fof(t8_bvfunc23,theorem,( ! [A,B,C,D,E,F,G] : ( ( v1_relat_1(G) & v1_funct_1(G) ) => ! [H,I,J,K,L,M] : ( G = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,I),k3_cqc_lang(C,J)),k3_cqc_lang(D,K)),k3_cqc_lang(E,L)),k3_cqc_lang(F,M)),k3_cqc_lang(A,H)) => k1_relat_1(G) = k4_enumset1(A,B,C,D,E,F) ) ) ), inference(mizar_proof,[status(thm)],[t30_bvfunc14,t47_enumset1,t50_enumset1,t5_cqc_lang,d1_funct_4,t51_enumset1]), [file(bvfunc23,t8_bvfunc23),interesting(1.00)]). fof(t5_bvfunc23,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ! [H] : ( m1_eqrel_1(H,A) => ( ( v2_bvfunc_2(B,A) & B = k4_enumset1(C,D,E,F,G,H) ) => ( C = D | C = E | C = F | C = G | C = H | D = E | D = F | D = G | D = H | E = F | E = G | E = H | F = G | F = H | G = H | k5_bvfunc_2(A,G,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),H) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t53_enumset1,t43_enumset1,t43_enumset1,t53_enumset1,t4_bvfunc23]), [file(bvfunc23,t5_bvfunc23),interesting(0.56)]). fof(t4_bvfunc23,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ! [H] : ( m1_eqrel_1(H,A) => ( ( v2_bvfunc_2(B,A) & B = k4_enumset1(C,D,E,F,G,H) ) => ( C = D | C = E | C = F | C = G | C = H | D = E | D = F | D = G | D = H | E = F | E = G | E = H | F = G | F = H | G = H | k5_bvfunc_2(A,F,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),G),H) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_enumset1,t45_enumset1,t45_enumset1,t52_enumset1,t3_bvfunc23]), [file(bvfunc23,t4_bvfunc23),interesting(0.52)]). fof(t3_bvfunc23,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ! [H] : ( m1_eqrel_1(H,A) => ( ( v2_bvfunc_2(B,A) & B = k4_enumset1(C,D,E,F,G,H) ) => ( C = D | C = E | C = F | C = G | C = H | D = E | D = F | D = G | D = H | E = F | E = G | E = H | F = G | F = H | G = H | k5_bvfunc_2(A,E,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),F),G),H) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t53_enumset1,t42_enumset1,t42_enumset1,t53_enumset1,t2_bvfunc23]), [file(bvfunc23,t3_bvfunc23),interesting(0.47)]). fof(t1_bvfunc23,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ! [H] : ( m1_eqrel_1(H,A) => ( B = k4_enumset1(C,D,E,F,G,H) => ( C = D | C = E | C = F | C = G | C = H | D = E | D = F | D = G | D = H | E = F | E = G | E = H | F = G | F = H | G = H | k5_bvfunc_2(A,C,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,D,E),F),G),H) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[d7_bvfunc_2,t51_enumset1,t42_xboole_1,d1_tarski,d1_tarski,d1_tarski,d1_tarski,d1_tarski,t47_enumset1,t42_xboole_1,t67_zfmisc_1,t44_enumset1,t42_xboole_1,t43_enumset1,t42_xboole_1,t72_zfmisc_1,t67_zfmisc_1,t67_zfmisc_1,t43_enumset1,t44_enumset1,t47_enumset1,d1_tarski,t68_zfmisc_1,d3_tarski,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,d4_partit1,d4_xboole_0,d5_setfam_1,t30_bvfunc14,t47_enumset1,t50_enumset1,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,t29_bvfunc14,d3_enumset1,d3_enumset1,d5_funct_1,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_tarski,d5_funct_1,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_tarski,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d3_enumset1,d10_xboole_0,d3_tarski,d3_enumset1,d10_setfam_1,d3_tarski,d3_enumset1,t29_bvfunc14,t16_xboole_1,t16_xboole_1,d3_xboole_0,t29_bvfunc14,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t29_bvfunc14,t16_xboole_1,t16_xboole_1,t16_xboole_1,d3_xboole_0,t29_bvfunc14,t16_xboole_1,d3_xboole_0,d3_xboole_0,d3_enumset1,d1_setfam_1,d10_setfam_1,d3_tarski,d3_enumset1,d1_setfam_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d10_xboole_0,d6_eqrel_1,d1_bvfunc_2,d3_tarski,d1_bvfunc_2,d3_enumset1,d5_funct_1,t12_funct_1,d10_setfam_1,d1_tarski,d3_tarski,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_tarski,d5_funct_1,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_enumset1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_enumset1,d1_setfam_1,d3_tarski,d1_setfam_1,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d10_xboole_0,d10_xboole_0,d1_tarski,d10_xboole_0,d1_tarski,d10_xboole_0,d1_tarski,d5_setfam_1,d4_xboole_0,d4_partit1,d5_setfam_1,d4_xboole_0,d4_partit1,d5_setfam_1,d4_xboole_0,d4_partit1,d5_setfam_1,d4_xboole_0,d4_partit1,d10_xboole_0]), [file(bvfunc23,t1_bvfunc23),interesting(0.46)]). fof(t7_bvfunc23,theorem,( ! [A,B,C,D,E,F,G] : ( ( v1_relat_1(G) & v1_funct_1(G) ) => ! [H,I,J,K,L,M] : ( G = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,I),k3_cqc_lang(C,J)),k3_cqc_lang(D,K)),k3_cqc_lang(E,L)),k3_cqc_lang(F,M)),k3_cqc_lang(A,H)) => ( A = B | A = C | A = D | A = E | A = F | B = C | B = D | B = E | B = F | C = D | C = E | C = F | D = E | D = F | E = F | ( k1_funct_1(G,A) = H & k1_funct_1(G,B) = I & k1_funct_1(G,C) = J & k1_funct_1(G,D) = K & k1_funct_1(G,E) = L & k1_funct_1(G,F) = M ) ) ) ) ), inference(mizar_proof,[status(thm)],[t5_cqc_lang,d1_tarski,t14_funct_4,t6_cqc_lang,d1_tarski,t12_funct_4,t29_bvfunc14,d1_tarski,t12_funct_4,t29_bvfunc14,d1_tarski,t12_funct_4,t29_bvfunc14,d1_tarski,t12_funct_4,t29_bvfunc14,d1_tarski,t12_funct_4,t29_bvfunc14]), [file(bvfunc23,t7_bvfunc23),interesting(0.43)]). fof(t2_bvfunc23,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ! [H] : ( m1_eqrel_1(H,A) => ( ( v2_bvfunc_2(B,A) & B = k4_enumset1(C,D,E,F,G,H) ) => ( C = D | C = E | C = F | C = G | C = H | D = E | D = F | D = G | D = H | E = F | E = G | E = H | F = G | F = H | G = H | k5_bvfunc_2(A,D,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,E),F),G),H) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t52_enumset1,t52_enumset1,t1_bvfunc23]), [file(bvfunc23,t2_bvfunc23),interesting(0.41)]). fof(t9_bvfunc23,theorem,( ! [A,B,C,D,E,F,G] : ( ( v1_relat_1(G) & v1_funct_1(G) ) => ! [H,I,J,K,L,M] : ( G = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,I),k3_cqc_lang(C,J)),k3_cqc_lang(D,K)),k3_cqc_lang(E,L)),k3_cqc_lang(F,M)),k3_cqc_lang(A,H)) => ( A = B | A = C | A = D | A = E | A = F | B = C | B = D | B = E | B = F | C = D | C = E | C = F | D = E | D = F | E = F | k2_relat_1(G) = k4_enumset1(k1_funct_1(G,A),k1_funct_1(G,B),k1_funct_1(G,C),k1_funct_1(G,D),k1_funct_1(G,E),k1_funct_1(G,F)) ) ) ) ), inference(mizar_proof,[status(thm)],[t8_bvfunc23,d4_enumset1,d4_enumset1,d4_enumset1,d4_enumset1,d4_enumset1,d4_enumset1,d3_tarski,d5_funct_1,d4_enumset1,d4_enumset1,d4_enumset1,d4_enumset1,d4_enumset1,d4_enumset1,d4_enumset1,d3_tarski,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d5_funct_1,d4_enumset1,d10_xboole_0]), [file(bvfunc23,t9_bvfunc23),interesting(0.38)]). fof(t6_bvfunc23,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ! [H] : ( m1_eqrel_1(H,A) => ( ( v2_bvfunc_2(B,A) & B = k4_enumset1(C,D,E,F,G,H) ) => ( C = D | C = E | C = F | C = G | C = H | D = E | D = F | D = G | D = H | E = F | E = G | E = H | F = G | F = H | G = H | k5_bvfunc_2(A,H,B) = k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,C,D),E),F),G) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t54_enumset1,t54_enumset1,t5_bvfunc23]), [file(bvfunc23,t6_bvfunc23),interesting(0.35)]). fof(t11_bvfunc23,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ! [H] : ( m1_eqrel_1(H,A) => ! [I] : ( m1_subset_1(I,A) => ! [J] : ( m1_subset_1(J,A) => ! [K] : ( ( v1_relat_1(K) & v1_funct_1(K) ) => ~ ( v2_bvfunc_2(B,A) & B = k4_enumset1(C,D,E,F,G,H) & C != D & C != E & C != F & C != G & C != H & D != E & D != F & D != G & D != H & E != F & E != G & E != H & F != G & F != H & G != H & k22_bvfunc_1(A,I,k2_partit1(A,k2_partit1(A,k2_partit1(A,E,F),G),H)) = k22_bvfunc_1(A,J,k2_partit1(A,k2_partit1(A,k2_partit1(A,E,F),G),H)) & r1_xboole_0(k22_bvfunc_1(A,J,k5_bvfunc_2(A,C,B)),k22_bvfunc_1(A,I,k5_bvfunc_2(A,D,B))) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t2_bvfunc23,t1_bvfunc23,t8_bvfunc23,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,d4_enumset1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,t9_bvfunc23,d3_tarski,d4_enumset1,d10_setfam_1,d5_bvfunc_2,d1_xboole_0,d1_setfam_1,t7_bvfunc23,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d1_xboole_0,d1_t_1topsp,d3_xboole_0,d3_xboole_0,d5_setfam_1,d1_tarski,d4_xboole_0,d4_partit1,t16_partit1,t16_partit1,t16_partit1,t3_bvfunc11,d3_xboole_0,d1_t_1topsp,t3_xboole_0,t9_t_1topsp,d1_t_1topsp,d1_t_1topsp,d3_xboole_0,d1_t_1topsp,t16_partit1,t16_partit1,t16_partit1,d6_eqrel_1,t3_xboole_0]), [file(bvfunc23,t11_bvfunc23),interesting(0.03)]). fof(t30_bvfunc14,theorem,( ! [A,B,C,D,E,F] : ( ( v1_relat_1(F) & v1_funct_1(F) ) => ! [G,H,I,J,K] : ( F = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,H),k3_cqc_lang(C,I)),k3_cqc_lang(D,J)),k3_cqc_lang(E,K)),k3_cqc_lang(A,G)) => k1_relat_1(F) = k3_enumset1(A,B,C,D,E) ) ) ), file(bvfunc14,t30_bvfunc14), [interesting(0.00)]). fof(t47_enumset1,theorem,( ! [A,B,C,D,E] : k3_enumset1(A,B,C,D,E) = k2_xboole_0(k1_tarski(A),k2_enumset1(B,C,D,E)) ), file(enumset1,t47_enumset1), [interesting(0.00)]). fof(t50_enumset1,theorem,( ! [A,B,C,D,E] : k3_enumset1(A,B,C,D,E) = k2_xboole_0(k2_enumset1(A,B,C,D),k1_tarski(E)) ), file(enumset1,t50_enumset1), [interesting(0.00)]). fof(t5_cqc_lang,theorem,( ! [A,B] : ( k1_relat_1(k3_cqc_lang(A,B)) = k1_tarski(A) & k2_relat_1(k3_cqc_lang(A,B)) = k1_tarski(B) ) ), file(cqc_lang,t5_cqc_lang), [interesting(0.00)]). fof(d1_funct_4,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( C = k1_funct_4(A,B) <=> ( k1_relat_1(C) = k2_xboole_0(k1_relat_1(A),k1_relat_1(B)) & ! [D] : ( r2_hidden(D,k2_xboole_0(k1_relat_1(A),k1_relat_1(B))) => ( ( r2_hidden(D,k1_relat_1(B)) => k1_funct_1(C,D) = k1_funct_1(B,D) ) & ( ~ r2_hidden(D,k1_relat_1(B)) => k1_funct_1(C,D) = k1_funct_1(A,D) ) ) ) ) ) ) ) ) ), file(funct_4,d1_funct_4), [interesting(0.00)]). fof(t51_enumset1,theorem,( ! [A,B,C,D,E,F] : k4_enumset1(A,B,C,D,E,F) = k2_xboole_0(k1_tarski(A),k3_enumset1(B,C,D,E,F)) ), file(enumset1,t51_enumset1), [interesting(0.00)]). fof(d1_tarski,definition,( ! [A,B] : ( B = k1_tarski(A) <=> ! [C] : ( r2_hidden(C,B) <=> C = A ) ) ), file(tarski,d1_tarski), [interesting(0.00)]). fof(t14_funct_4,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( r2_hidden(A,k1_relat_1(B)) => k1_funct_1(k1_funct_4(C,B),A) = k1_funct_1(B,A) ) ) ) ), file(funct_4,t14_funct_4), [interesting(0.00)]). fof(t6_cqc_lang,theorem,( ! [A,B] : k1_funct_1(k3_cqc_lang(A,B),A) = B ), file(cqc_lang,t6_cqc_lang), [interesting(0.00)]). fof(t12_funct_4,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ( ~ r2_hidden(A,k1_relat_1(B)) => k1_funct_1(k1_funct_4(C,B),A) = k1_funct_1(C,A) ) ) ) ), file(funct_4,t12_funct_4), [interesting(0.00)]). fof(t29_bvfunc14,theorem,( ! [A,B,C,D,E,F] : ( ( v1_relat_1(F) & v1_funct_1(F) ) => ! [G,H,I,J,K] : ( F = k1_funct_4(k1_funct_4(k1_funct_4(k1_funct_4(k3_cqc_lang(B,H),k3_cqc_lang(C,I)),k3_cqc_lang(D,J)),k3_cqc_lang(E,K)),k3_cqc_lang(A,G)) => ( A = B | A = C | A = D | A = E | B = C | B = D | B = E | C = D | C = E | D = E | ( k1_funct_1(F,A) = G & k1_funct_1(F,B) = H & k1_funct_1(F,C) = I & k1_funct_1(F,D) = J & k1_funct_1(F,E) = K ) ) ) ) ), file(bvfunc14,t29_bvfunc14), [interesting(0.00)]). fof(d4_enumset1,definition,( ! [A,B,C,D,E,F,G] : ( G = k4_enumset1(A,B,C,D,E,F) <=> ! [H] : ( r2_hidden(H,G) <=> ~ ( H != A & H != B & H != C & H != D & H != E & H != F ) ) ) ), file(enumset1,d4_enumset1), [interesting(0.00)]). fof(d5_funct_1,definition,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( B = k2_relat_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ? [D] : ( r2_hidden(D,k1_relat_1(A)) & C = k1_funct_1(A,D) ) ) ) ) ), file(funct_1,d5_funct_1), [interesting(0.00)]). fof(d3_tarski,definition,( ! [A,B] : ( r1_tarski(A,B) <=> ! [C] : ( r2_hidden(C,A) => r2_hidden(C,B) ) ) ), file(tarski,d3_tarski), [interesting(0.00)]). fof(d10_xboole_0,definition,( ! [A,B] : ( A = B <=> ( r1_tarski(A,B) & r1_tarski(B,A) ) ) ), file(xboole_0,d10_xboole_0), [interesting(0.00)]). fof(d10_setfam_1,definition,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) => ( ( B != k1_xboole_0 => k8_setfam_1(A,B) = k6_setfam_1(A,B) ) & ( B = k1_xboole_0 => k8_setfam_1(A,B) = A ) ) ) ), file(setfam_1,d10_setfam_1), [interesting(0.00)]). fof(d5_bvfunc_2,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ( v2_bvfunc_2(B,A) <=> ! [C] : ( ( v1_relat_1(C) & v1_funct_1(C) ) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(k1_zfmisc_1(A))) => ~ ( k1_relat_1(C) = B & k2_relat_1(C) = D & ! [E] : ( r2_hidden(E,B) => r2_hidden(k1_funct_1(C,E),E) ) & k8_setfam_1(A,D) = k1_xboole_0 ) ) ) ) ) ) ), file(bvfunc_2,d5_bvfunc_2), [interesting(0.00)]). fof(d1_xboole_0,definition,( ! [A] : ( A = k1_xboole_0 <=> ! [B] : ~ r2_hidden(B,A) ) ), file(xboole_0,d1_xboole_0), [interesting(0.00)]). fof(d1_setfam_1,definition,( ! [A,B] : ( ( A != k1_xboole_0 => ( B = k1_setfam_1(A) <=> ! [C] : ( r2_hidden(C,B) <=> ! [D] : ( r2_hidden(D,A) => r2_hidden(C,D) ) ) ) ) & ( A = k1_xboole_0 => ( B = k1_setfam_1(A) <=> B = k1_xboole_0 ) ) ) ), file(setfam_1,d1_setfam_1), [interesting(0.00)]). fof(t1_bvfunc14,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => k22_bvfunc_1(A,B,k2_partit1(A,C,D)) = k5_subset_1(A,k22_bvfunc_1(A,B,C),k22_bvfunc_1(A,B,D)) ) ) ) ) ), file(bvfunc14,t1_bvfunc14), [interesting(0.00)]). fof(d3_xboole_0,definition,( ! [A,B,C] : ( C = k3_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & r2_hidden(D,B) ) ) ) ), file(xboole_0,d3_xboole_0), [interesting(0.00)]). fof(d7_xboole_0,definition,( ! [A,B] : ( r1_xboole_0(A,B) <=> k3_xboole_0(A,B) = k1_xboole_0 ) ), file(xboole_0,d7_xboole_0), [interesting(0.00)]). fof(t10_bvfunc23,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => ! [E] : ( m1_eqrel_1(E,A) => ! [F] : ( m1_eqrel_1(F,A) => ! [G] : ( m1_eqrel_1(G,A) => ! [H] : ( m1_eqrel_1(H,A) => ! [I] : ( m1_subset_1(I,A) => ! [J] : ( m1_subset_1(J,A) => ! [K] : ( ( v1_relat_1(K) & v1_funct_1(K) ) => ~ ( v2_bvfunc_2(B,A) & B = k4_enumset1(C,D,E,F,G,H) & C != D & C != E & C != F & C != G & C != H & D != E & D != F & D != G & D != H & E != F & E != G & E != H & F != G & F != H & G != H & r1_xboole_0(k22_bvfunc_1(A,J,k2_partit1(A,k2_partit1(A,k2_partit1(A,k2_partit1(A,D,E),F),G),H)),k22_bvfunc_1(A,I,C)) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_proof,[status(thm)],[t8_bvfunc23,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,t7_bvfunc23,d4_enumset1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,d4_enumset1,d5_funct_1,t9_bvfunc23,d3_tarski,d4_enumset1,d10_setfam_1,d5_bvfunc_2,d1_xboole_0,d1_setfam_1,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,t1_bvfunc14,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d3_xboole_0,d7_xboole_0]), [file(bvfunc23,t10_bvfunc23),interesting(0.00)]). fof(t52_enumset1,theorem,( ! [A,B,C,D,E,F] : k4_enumset1(A,B,C,D,E,F) = k2_xboole_0(k2_tarski(A,B),k2_enumset1(C,D,E,F)) ), file(enumset1,t52_enumset1), [interesting(0.00)]). fof(d7_bvfunc_2,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_eqrel_1(B,A) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(k1_bvfunc_2(A))) => k5_bvfunc_2(A,B,C) = k2_bvfunc_2(A,k6_subset_1(k1_bvfunc_2(A),C,k4_bvfunc_2(A,B))) ) ) ) ), file(bvfunc_2,d7_bvfunc_2), [interesting(0.00)]). fof(t42_xboole_1,theorem,( ! [A,B,C] : k4_xboole_0(k2_xboole_0(A,B),C) = k2_xboole_0(k4_xboole_0(A,C),k4_xboole_0(B,C)) ), file(xboole_1,t42_xboole_1), [interesting(0.00)]). fof(t67_zfmisc_1,theorem,( ! [A,B] : ( k4_xboole_0(k1_tarski(A),B) = k1_tarski(A) <=> ~ r2_hidden(A,B) ) ), file(zfmisc_1,t67_zfmisc_1), [interesting(0.00)]). fof(t44_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_xboole_0(k1_tarski(A),k1_enumset1(B,C,D)) ), file(enumset1,t44_enumset1), [interesting(0.00)]). fof(t43_enumset1,theorem,( ! [A,B,C] : k1_enumset1(A,B,C) = k2_xboole_0(k2_tarski(A,B),k1_tarski(C)) ), file(enumset1,t43_enumset1), [interesting(0.00)]). fof(t72_zfmisc_1,theorem,( ! [A,B,C] : ( k4_xboole_0(k2_tarski(A,B),C) = k2_tarski(A,B) <=> ( ~ r2_hidden(A,C) & ~ r2_hidden(B,C) ) ) ), file(zfmisc_1,t72_zfmisc_1), [interesting(0.00)]). fof(t68_zfmisc_1,theorem,( ! [A,B] : ( k4_xboole_0(k1_tarski(A),B) = k1_xboole_0 <=> r2_hidden(A,B) ) ), file(zfmisc_1,t68_zfmisc_1), [interesting(0.00)]). fof(d4_partit1,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_eqrel_1(B,A) => ! [C] : ( m1_eqrel_1(C,A) => k2_partit1(A,B,C) = k4_xboole_0(k3_setfam_1(B,C),k1_tarski(k1_xboole_0)) ) ) ) ), file(partit1,d4_partit1), [interesting(0.00)]). fof(d4_xboole_0,definition,( ! [A,B,C] : ( C = k4_xboole_0(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ( r2_hidden(D,A) & ~ r2_hidden(D,B) ) ) ) ), file(xboole_0,d4_xboole_0), [interesting(0.00)]). fof(d5_setfam_1,definition,( ! [A,B,C] : ( C = k3_setfam_1(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E,F] : ( r2_hidden(E,A) & r2_hidden(F,B) & D = k3_xboole_0(E,F) ) ) ) ), file(setfam_1,d5_setfam_1), [interesting(0.00)]). fof(d3_enumset1,definition,( ! [A,B,C,D,E,F] : ( F = k3_enumset1(A,B,C,D,E) <=> ! [G] : ( r2_hidden(G,F) <=> ~ ( G != A & G != B & G != C & G != D & G != E ) ) ) ), file(enumset1,d3_enumset1), [interesting(0.00)]). fof(t16_xboole_1,theorem,( ! [A,B,C] : k3_xboole_0(k3_xboole_0(A,B),C) = k3_xboole_0(A,k3_xboole_0(B,C)) ), file(xboole_1,t16_xboole_1), [interesting(0.00)]). fof(d6_eqrel_1,definition,( ! [A,B] : ( m1_subset_1(B,k1_zfmisc_1(k1_zfmisc_1(A))) => ( ( A != k1_xboole_0 => ( m1_eqrel_1(B,A) <=> ( k5_setfam_1(A,B) = A & ! [C] : ( m1_subset_1(C,k1_zfmisc_1(A)) => ( r2_hidden(C,B) => ( C != k1_xboole_0 & ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ~ ( r2_hidden(D,B) & C != D & ~ r1_xboole_0(C,D) ) ) ) ) ) ) ) ) & ( A = k1_xboole_0 => ( m1_eqrel_1(B,A) <=> B = k1_xboole_0 ) ) ) ) ), file(eqrel_1,d6_eqrel_1), [interesting(0.00)]). fof(d1_bvfunc_2,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(k1_bvfunc_2(A))) => ! [C] : ( m1_eqrel_1(C,A) => ( C = k2_bvfunc_2(A,B) <=> ! [D] : ( r2_hidden(D,C) <=> ? [E] : ( v1_relat_1(E) & v1_funct_1(E) & ? [F] : ( m1_subset_1(F,k1_zfmisc_1(k1_zfmisc_1(A))) & k1_relat_1(E) = B & k2_relat_1(E) = F & ! [G] : ( r2_hidden(G,B) => r2_hidden(k1_funct_1(E,G),G) ) & D = k8_setfam_1(A,F) & D != k1_xboole_0 ) ) ) ) ) ) ) ), file(bvfunc_2,d1_bvfunc_2), [interesting(0.00)]). fof(t12_funct_1,theorem,( ! [A,B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( r2_hidden(A,k1_relat_1(B)) => r2_hidden(k1_funct_1(B,A),k2_relat_1(B)) ) ) ), file(funct_1,t12_funct_1), [interesting(0.00)]). fof(d1_t_1topsp,definition,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(A)) => ( D = k1_t_1topsp(A,B,C) <=> ( r2_hidden(B,D) & r2_hidden(D,C) ) ) ) ) ) ) ), file(t_1topsp,d1_t_1topsp), [interesting(0.00)]). fof(t16_partit1,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_eqrel_1(B,A) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => k2_partit1(A,k2_partit1(A,B,C),D) = k2_partit1(A,B,k2_partit1(A,C,D)) ) ) ) ) ), file(partit1,t16_partit1), [interesting(0.00)]). fof(t3_bvfunc11,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_subset_1(B,A) => ! [C] : ( m1_eqrel_1(C,A) => ! [D] : ( m1_eqrel_1(D,A) => r1_tarski(k22_bvfunc_1(A,B,k2_partit1(A,C,D)),k22_bvfunc_1(A,B,C)) ) ) ) ) ), file(bvfunc11,t3_bvfunc11), [interesting(0.00)]). fof(t3_xboole_0,theorem,( ! [A,B] : ( ~ ( ~ r1_xboole_0(A,B) & ! [C] : ~ ( r2_hidden(C,A) & r2_hidden(C,B) ) ) & ~ ( ? [C] : ( r2_hidden(C,A) & r2_hidden(C,B) ) & r1_xboole_0(A,B) ) ) ), file(xboole_0,t3_xboole_0), [interesting(0.00)]). fof(t9_t_1topsp,theorem,( ! [A] : ( ~ v1_xboole_0(A) => ! [B] : ( m1_eqrel_1(B,A) => ! [C] : ( m1_subset_1(C,A) => ! [D] : ( m1_subset_1(D,A) => ( ~ r1_xboole_0(k1_t_1topsp(A,C,B),k1_t_1topsp(A,D,B)) => k1_t_1topsp(A,C,B) = k1_t_1topsp(A,D,B) ) ) ) ) ) ), file(t_1topsp,t9_t_1topsp), [interesting(0.00)]). fof(t54_enumset1,theorem,( ! [A,B,C,D,E,F] : k4_enumset1(A,B,C,D,E,F) = k2_xboole_0(k2_enumset1(A,B,C,D),k2_tarski(E,F)) ), file(enumset1,t54_enumset1), [interesting(0.00)]). fof(t53_enumset1,theorem,( ! [A,B,C,D,E,F] : k4_enumset1(A,B,C,D,E,F) = k2_xboole_0(k1_enumset1(A,B,C),k1_enumset1(D,E,F)) ), file(enumset1,t53_enumset1), [interesting(0.00)]). fof(t45_enumset1,theorem,( ! [A,B,C,D] : k2_enumset1(A,B,C,D) = k2_xboole_0(k2_tarski(A,B),k2_tarski(C,D)) ), file(enumset1,t45_enumset1), [interesting(0.00)]). fof(t42_enumset1,theorem,( ! [A,B,C] : k1_enumset1(A,B,C) = k2_xboole_0(k1_tarski(A),k2_tarski(B,C)) ), file(enumset1,t42_enumset1), [interesting(0.00)]).