% Mizar problem: t16_projred2,projred2,296,65 fof(t16_projred2,conjecture,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u1_incsp_1(A)) => ! [F] : ( m1_subset_1(F,u1_incsp_1(A)) => ! [G] : ( m1_subset_1(G,u1_incsp_1(A)) => ! [H] : ( m1_subset_1(H,u1_incsp_1(A)) => ! [I] : ( m1_subset_1(I,u1_incsp_1(A)) => ! [J] : ( m1_subset_1(J,u1_incsp_1(A)) => ! [K] : ( m1_subset_1(K,u2_incsp_1(A)) => ! [L] : ( m1_subset_1(L,u2_incsp_1(A)) => ! [M] : ( m1_subset_1(M,u2_incsp_1(A)) => ! [N] : ( m1_subset_1(N,u2_incsp_1(A)) => ! [O] : ( m1_subset_1(O,u2_incsp_1(A)) => ! [P] : ( m1_subset_1(P,u2_incsp_1(A)) => ! [Q] : ( m1_subset_1(Q,u2_incsp_1(A)) => ! [R] : ( m1_subset_1(R,u2_incsp_1(A)) => ( ( r3_incproj(A,E,F,K) & r4_incproj(A,F,G,M,H) & r4_incproj(A,E,H,L,I) & r4_incproj(A,B,C,O,H) & r3_incproj(A,E,J,N) & r4_incproj(A,B,F,P,I) & r4_incproj(A,C,I,Q,J) & r4_incproj(A,F,J,R,D) & r1_incsp_1(A,D,O) ) => ( r1_incsp_1(A,B,K) | r1_incsp_1(A,B,L) | r1_incsp_1(A,C,M) | r1_incsp_1(A,C,L) | r1_incsp_1(A,C,N) | r1_projred2(A,K,M,L) | B = C | C = D | K = N | k5_relat_1(k1_projred1(A,K,L,B),k1_projred1(A,L,M,C)) = k5_relat_1(k1_projred1(A,K,N,D),k1_projred1(A,N,M,C)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), inference(mizar_bg_added,[status(thm)],[antisymmetry_r2_hidden,cc1_funct_1,cc1_relset_1,cc2_funct_1,d10_incproj,d14_incproj,d1_projred1,d1_projred2,d2_projred2,d5_incproj,d7_incproj,d8_incproj,d9_incproj,dt_k1_funct_1,dt_k1_projred1,dt_k1_projred2,dt_k1_relat_1,dt_k1_xboole_0,dt_k1_zfmisc_1,dt_k2_relat_1,dt_k2_zfmisc_1,dt_k4_relset_1,dt_k5_relat_1,dt_l1_incsp_1,dt_m1_relset_1,dt_m1_subset_1,dt_m2_relset_1,dt_u1_incsp_1,dt_u2_incsp_1,existence_l1_incsp_1,existence_m1_relset_1,existence_m1_subset_1,existence_m2_relset_1,fc1_funct_1,fraenkel_a_2_0_projred2,rc1_funct_1,rc2_funct_1,rc3_funct_1,redefinition_k4_relset_1,redefinition_m2_relset_1,reflexivity_r1_tarski,t14_projred1,t1_subset,t23_funct_1,t25_projred1,t2_subset,t2_tarski,t3_subset,t4_subset,t5_projred2,t5_subset,t6_boole,t7_boole,t8_boole,t9_funct_1]), [file(projred2,t16_projred2)]). fof(antisymmetry_r2_hidden,axiom,( ! [A,B] : ( r2_hidden(A,B) => ~ r2_hidden(B,A) ) ), file(hidden,r2_hidden), []). fof(cc1_funct_1,axiom,( ! [A] : ( v1_xboole_0(A) => v1_funct_1(A) ) ), file(funct_1,cc1_funct_1), []). fof(cc1_relset_1,axiom,( ! [A,B,C] : ( m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) => v1_relat_1(C) ) ), file(relset_1,cc1_relset_1), []). fof(cc2_funct_1,axiom,( ! [A] : ( ( v1_relat_1(A) & v1_xboole_0(A) & v1_funct_1(A) ) => ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) ) ) ), file(funct_1,cc2_funct_1), []). fof(d10_incproj,axiom,( ! [A] : ( l1_incsp_1(A) => ( v2_incproj(A) <=> ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ? [D] : ( m1_subset_1(D,u2_incsp_1(A)) & r1_incsp_1(A,B,D) & r1_incsp_1(A,C,D) ) ) ) ) ) ), file(incproj,d10_incproj), []). fof(d14_incproj,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & l1_incsp_1(A) ) => ( v6_incproj(A) <=> ! [B] : ( m1_subset_1(B,u2_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u2_incsp_1(A)) => ? [D] : ( m1_subset_1(D,u1_incsp_1(A)) & r1_incsp_1(A,D,B) & r1_incsp_1(A,D,C) ) ) ) ) ) ), file(incproj,d14_incproj), []). fof(d1_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u2_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u2_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ~ ( ~ r1_incsp_1(A,D,B) & ~ r1_incsp_1(A,D,C) & ~ ! [E] : ( ( v1_funct_1(E) & m2_relset_1(E,u1_incsp_1(A),u1_incsp_1(A)) ) => ( E = k1_projred1(A,B,C,D) <=> ( r1_tarski(k4_relset_1(u1_incsp_1(A),u1_incsp_1(A),E),u1_incsp_1(A)) & ! [F] : ( m1_subset_1(F,u1_incsp_1(A)) => ( r2_hidden(F,k4_relset_1(u1_incsp_1(A),u1_incsp_1(A),E)) <=> r1_incsp_1(A,F,B) ) ) & ! [F] : ( m1_subset_1(F,u1_incsp_1(A)) => ! [G] : ( m1_subset_1(G,u1_incsp_1(A)) => ( ( r1_incsp_1(A,F,B) & r1_incsp_1(A,G,C) ) => ( k1_funct_1(E,F) = G <=> ? [H] : ( m1_subset_1(H,u2_incsp_1(A)) & r1_incsp_1(A,D,H) & r1_incsp_1(A,F,H) & r1_incsp_1(A,G,H) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(projred1,d1_projred1), []). fof(d1_projred2,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u2_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u2_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ( r1_projred2(A,B,C,D) <=> ? [E] : ( m1_subset_1(E,u1_incsp_1(A)) & r1_incsp_1(A,E,B) & r1_incsp_1(A,E,C) & r1_incsp_1(A,E,D) ) ) ) ) ) ) ), file(projred2,d1_projred2), []). fof(d2_projred2,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u2_incsp_1(A)) => k1_projred2(A,B) = a_2_0_projred2(A,B) ) ) ), file(projred2,d2_projred2), []). fof(d5_incproj,axiom,( ! [A,B,C] : ( r1_incproj(A,B,C) <=> ( A != B & B != C & C != A ) ) ), file(incproj,d5_incproj), []). fof(d7_incproj,axiom,( ! [A] : ( l1_incsp_1(A) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ( r3_incproj(A,B,C,D) <=> ( r1_incsp_1(A,B,D) & r1_incsp_1(A,C,D) ) ) ) ) ) ) ), file(incproj,d7_incproj), []). fof(d8_incproj,axiom,( ! [A] : ( l1_incsp_1(A) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u1_incsp_1(A)) => ( r4_incproj(A,B,C,D,E) <=> ( r1_incsp_1(A,B,D) & r1_incsp_1(A,C,D) & r1_incsp_1(A,E,D) ) ) ) ) ) ) ) ), file(incproj,d8_incproj), []). fof(d9_incproj,axiom,( ! [A] : ( l1_incsp_1(A) => ( v1_incproj(A) <=> ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u2_incsp_1(A)) => ~ ( r1_incsp_1(A,B,D) & r1_incsp_1(A,C,D) & r1_incsp_1(A,B,E) & r1_incsp_1(A,C,E) & B != C & D != E ) ) ) ) ) ) ) ), file(incproj,d9_incproj), []). fof(dt_k1_funct_1,axiom,( $true ), file(funct_1,k1_funct_1), []). fof(dt_k1_projred1,axiom,( ! [A,B,C,D] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) & m1_subset_1(B,u2_incsp_1(A)) & m1_subset_1(C,u2_incsp_1(A)) & m1_subset_1(D,u1_incsp_1(A)) ) => ( v1_funct_1(k1_projred1(A,B,C,D)) & m2_relset_1(k1_projred1(A,B,C,D),u1_incsp_1(A),u1_incsp_1(A)) ) ) ), file(projred1,k1_projred1), []). fof(dt_k1_projred2,axiom,( ! [A,B] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & l1_incsp_1(A) & m1_subset_1(B,u2_incsp_1(A)) ) => m1_subset_1(k1_projred2(A,B),k1_zfmisc_1(u1_incsp_1(A))) ) ), file(projred2,k1_projred2), []). fof(dt_k1_relat_1,axiom,( $true ), file(relat_1,k1_relat_1), []). fof(dt_k1_xboole_0,axiom,( $true ), file(xboole_0,k1_xboole_0), []). fof(dt_k1_zfmisc_1,axiom,( $true ), file(zfmisc_1,k1_zfmisc_1), []). fof(dt_k2_relat_1,axiom,( $true ), file(relat_1,k2_relat_1), []). fof(dt_k2_zfmisc_1,axiom,( $true ), file(zfmisc_1,k2_zfmisc_1), []). fof(dt_k4_relset_1,axiom,( ! [A,B,C] : ( m1_relset_1(C,A,B) => m1_subset_1(k4_relset_1(A,B,C),k1_zfmisc_1(A)) ) ), file(relset_1,k4_relset_1), []). fof(dt_k5_relat_1,axiom,( ! [A,B] : ( ( v1_relat_1(A) & v1_relat_1(B) ) => v1_relat_1(k5_relat_1(A,B)) ) ), file(relat_1,k5_relat_1), []). fof(dt_l1_incsp_1,axiom,( $true ), file(incsp_1,l1_incsp_1), []). fof(dt_m1_relset_1,axiom,( $true ), file(relset_1,m1_relset_1), []). fof(dt_m1_subset_1,axiom,( $true ), file(subset_1,m1_subset_1), []). fof(dt_m2_relset_1,axiom,( ! [A,B,C] : ( m2_relset_1(C,A,B) => m1_subset_1(C,k1_zfmisc_1(k2_zfmisc_1(A,B))) ) ), file(relset_1,m2_relset_1), []). fof(dt_u1_incsp_1,axiom,( ! [A] : ( l1_incsp_1(A) => ~ v1_xboole_0(u1_incsp_1(A)) ) ), file(incsp_1,u1_incsp_1), []). fof(dt_u2_incsp_1,axiom,( ! [A] : ( l1_incsp_1(A) => ~ v1_xboole_0(u2_incsp_1(A)) ) ), file(incsp_1,u2_incsp_1), []). fof(existence_l1_incsp_1,axiom,( ? [A] : l1_incsp_1(A) ), file(incsp_1,l1_incsp_1), []). fof(existence_m1_relset_1,axiom,( ! [A,B] : ? [C] : m1_relset_1(C,A,B) ), file(relset_1,m1_relset_1), []). fof(existence_m1_subset_1,axiom,( ! [A] : ? [B] : m1_subset_1(B,A) ), file(subset_1,m1_subset_1), []). fof(existence_m2_relset_1,axiom,( ! [A,B] : ? [C] : m2_relset_1(C,A,B) ), file(relset_1,m2_relset_1), []). fof(fc1_funct_1,axiom,( ! [A,B] : ( ( v1_relat_1(A) & v1_funct_1(A) & v1_relat_1(B) & v1_funct_1(B) ) => ( v1_relat_1(k5_relat_1(A,B)) & v1_funct_1(k5_relat_1(A,B)) ) ) ), file(funct_1,fc1_funct_1), []). fof(fraenkel_a_2_0_projred2,axiom,( ! [A,B,C] : ( ( v1_incproj(B) & v2_incproj(B) & v3_incproj(B) & v4_incproj(B) & v5_incproj(B) & l1_incsp_1(B) & m1_subset_1(C,u2_incsp_1(B)) ) => ( r2_hidden(A,a_2_0_projred2(B,C)) <=> ? [D] : ( m1_subset_1(D,u1_incsp_1(B)) & A = D & r1_incsp_1(B,D,C) ) ) ) ), file(projred2,a_2_0_projred2), []). fof(rc1_funct_1,axiom,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) ) ), file(funct_1,rc1_funct_1), []). fof(rc2_funct_1,axiom,( ? [A] : ( v1_relat_1(A) & v1_xboole_0(A) & v1_funct_1(A) ) ), file(funct_1,rc2_funct_1), []). fof(rc3_funct_1,axiom,( ? [A] : ( v1_relat_1(A) & v1_funct_1(A) & v2_funct_1(A) ) ), file(funct_1,rc3_funct_1), []). fof(redefinition_k4_relset_1,axiom,( ! [A,B,C] : ( m1_relset_1(C,A,B) => k4_relset_1(A,B,C) = k1_relat_1(C) ) ), file(relset_1,k4_relset_1), []). fof(redefinition_m2_relset_1,axiom,( ! [A,B,C] : ( m2_relset_1(C,A,B) <=> m1_relset_1(C,A,B) ) ), file(relset_1,m2_relset_1), []). fof(reflexivity_r1_tarski,axiom,( ! [A,B] : r1_tarski(A,A) ), file(tarski,r1_tarski), []). fof(t14_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u1_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u1_incsp_1(A)) => ! [F] : ( m1_subset_1(F,u1_incsp_1(A)) => ! [G] : ( m1_subset_1(G,u1_incsp_1(A)) => ! [H] : ( m1_subset_1(H,u1_incsp_1(A)) => ! [I] : ( m1_subset_1(I,u1_incsp_1(A)) => ! [J] : ( m1_subset_1(J,u1_incsp_1(A)) => ! [K] : ( m1_subset_1(K,u1_incsp_1(A)) => ! [L] : ( m1_subset_1(L,u2_incsp_1(A)) => ! [M] : ( m1_subset_1(M,u2_incsp_1(A)) => ! [N] : ( m1_subset_1(N,u2_incsp_1(A)) => ! [O] : ( m1_subset_1(O,u2_incsp_1(A)) => ! [P] : ( m1_subset_1(P,u2_incsp_1(A)) => ! [Q] : ( m1_subset_1(Q,u2_incsp_1(A)) => ! [R] : ( m1_subset_1(R,u2_incsp_1(A)) => ! [S] : ( m1_subset_1(S,u2_incsp_1(A)) => ! [T] : ( m1_subset_1(T,u2_incsp_1(A)) => ~ ( r4_incproj(A,B,C,L,D) & r4_incproj(A,B,F,M,E) & r4_incproj(A,B,H,N,G) & r4_incproj(A,H,F,O,K) & r4_incproj(A,H,I,P,D) & r4_incproj(A,F,J,Q,D) & r4_incproj(A,K,E,R,G) & r4_incproj(A,C,I,S,G) & r4_incproj(A,C,J,T,E) & r1_incproj(L,M,N) & B != H & B != C & B != E & F != E & ! [U] : ( m1_subset_1(U,u2_incsp_1(A)) => ~ r4_incproj(A,I,J,U,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(projred1,t14_projred1), []). fof(t1_subset,axiom,( ! [A,B] : ( r2_hidden(A,B) => m1_subset_1(A,B) ) ), file(subset,t1_subset), []). fof(t23_funct_1,axiom,( ! [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(k5_relat_1(B,C),A) = k1_funct_1(C,k1_funct_1(B,A)) ) ) ) ), file(funct_1,t23_funct_1), []). fof(t25_projred1,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u1_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ! [E] : ( m1_subset_1(E,u2_incsp_1(A)) => ! [F] : ( m1_subset_1(F,u2_incsp_1(A)) => ~ ( ~ r1_incsp_1(A,B,D) & ~ r1_incsp_1(A,B,E) & ~ r1_incsp_1(A,C,E) & ~ r1_incsp_1(A,C,F) & ~ ( k1_relat_1(k5_relat_1(k1_projred1(A,D,E,B),k1_projred1(A,E,F,C))) = k4_relset_1(u1_incsp_1(A),u1_incsp_1(A),k1_projred1(A,D,E,B)) & k2_relat_1(k5_relat_1(k1_projred1(A,D,E,B),k1_projred1(A,E,F,C))) = k2_relat_1(k1_projred1(A,E,F,C)) ) ) ) ) ) ) ) ) ), file(projred1,t25_projred1), []). fof(t2_subset,axiom,( ! [A,B] : ( m1_subset_1(A,B) => ( v1_xboole_0(B) | r2_hidden(A,B) ) ) ), file(subset,t2_subset), []). fof(t2_tarski,axiom,( ! [A,B] : ( ! [C] : ( r2_hidden(C,A) <=> r2_hidden(C,B) ) => A = B ) ), file(tarski,t2_tarski), []). fof(t3_subset,axiom,( ! [A,B] : ( m1_subset_1(A,k1_zfmisc_1(B)) <=> r1_tarski(A,B) ) ), file(subset,t3_subset), []). fof(t4_subset,axiom,( ! [A,B,C] : ( ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) ) => m1_subset_1(A,C) ) ), file(subset,t4_subset), []). fof(t5_projred2,axiom,( ! [A] : ( ( v1_incproj(A) & v2_incproj(A) & v3_incproj(A) & v4_incproj(A) & v5_incproj(A) & v6_incproj(A) & v10_incproj(A) & l1_incsp_1(A) ) => ! [B] : ( m1_subset_1(B,u1_incsp_1(A)) => ! [C] : ( m1_subset_1(C,u2_incsp_1(A)) => ! [D] : ( m1_subset_1(D,u2_incsp_1(A)) => ~ ( ~ r1_incsp_1(A,B,C) & ~ r1_incsp_1(A,B,D) & k4_relset_1(u1_incsp_1(A),u1_incsp_1(A),k1_projred1(A,C,D,B)) != k1_projred2(A,C) ) ) ) ) ) ), file(projred2,t5_projred2), []). fof(t5_subset,axiom,( ! [A,B,C] : ~ ( r2_hidden(A,B) & m1_subset_1(B,k1_zfmisc_1(C)) & v1_xboole_0(C) ) ), file(subset,t5_subset), []). fof(t6_boole,axiom,( ! [A] : ( v1_xboole_0(A) => A = k1_xboole_0 ) ), file(boole,t6_boole), []). fof(t7_boole,axiom,( ! [A,B] : ~ ( r2_hidden(A,B) & v1_xboole_0(B) ) ), file(boole,t7_boole), []). fof(t8_boole,axiom,( ! [A,B] : ~ ( v1_xboole_0(A) & A != B & v1_xboole_0(B) ) ), file(boole,t8_boole), []). fof(t9_funct_1,axiom,( ! [A] : ( ( v1_relat_1(A) & v1_funct_1(A) ) => ! [B] : ( ( v1_relat_1(B) & v1_funct_1(B) ) => ( ( k1_relat_1(A) = k1_relat_1(B) & ! [C] : ( r2_hidden(C,k1_relat_1(A)) => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) => A = B ) ) ) ), file(funct_1,t9_funct_1), []).