% Mizar problem: t7_conmetr1,conmetr1,463,54 fof(t7_conmetr1,conjecture,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v4_aff_2(A) => v2_conmetr1(A) ) ) ), inference(mizar_bg_added,[status(thm)],[antisymmetry_r2_hidden,d1_aff_1,d2_conmetr1,d4_aff_2,dt_k1_zfmisc_1,dt_l1_analoaf,dt_l1_struct_0,dt_m1_subset_1,dt_u1_struct_0,existence_l1_analoaf,existence_l1_struct_0,existence_m1_subset_1,redefinition_r4_aff_1,reflexivity_r1_tarski,symmetry_r4_aff_1,t11_aff_1,t13_aff_1,t14_aff_1,t15_aff_1,t16_aff_1,t1_subset,t23_aff_1,t2_translac,t33_aff_1,t39_aff_1,t3_subset,t4_subset,t52_aff_1,t53_aff_1,t55_aff_1,t58_aff_1,t59_aff_1,t74_aff_1]), [file(conmetr1,t7_conmetr1)]). fof(antisymmetry_r2_hidden,axiom,( ! [A,B] : ( r2_hidden(A,B) => ~ r2_hidden(B,A) ) ), file(hidden,r2_hidden), []). fof(d1_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_aff_1(A,B,C,D) <=> r2_analoaf(A,B,C,B,D) ) ) ) ) ) ), file(aff_1,d1_aff_1), []). fof(d2_conmetr1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ( v2_conmetr1(A) <=> ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,k1_zfmisc_1(u1_struct_0(A))) => ! [L] : ( m1_subset_1(L,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(K,A) & v1_aff_1(L,A) & r2_hidden(B,K) & r2_hidden(B,L) & r2_hidden(C,K) & r2_hidden(E,K) & r2_hidden(G,K) & r2_hidden(I,K) & r2_hidden(D,L) & r2_hidden(F,L) & r2_hidden(H,L) & r2_hidden(J,L) & r2_analoaf(A,E,D,I,H) & r2_analoaf(A,D,C,H,G) & r2_analoaf(A,C,F,G,J) ) => ( r2_hidden(F,K) | r2_hidden(D,K) | r2_hidden(H,K) | r2_hidden(J,K) | r2_hidden(C,L) | r2_hidden(E,L) | r2_hidden(G,L) | r2_hidden(I,L) | r2_analoaf(A,E,F,I,J) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(conmetr1,d2_conmetr1), []). fof(d4_aff_2,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ( v4_aff_2(A) <=> ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ! [H] : ( m1_subset_1(H,u1_struct_0(A)) => ! [I] : ( m1_subset_1(I,u1_struct_0(A)) => ! [J] : ( m1_subset_1(J,u1_struct_0(A)) => ! [K] : ( m1_subset_1(K,u1_struct_0(A)) => ( ( r2_hidden(E,B) & r2_hidden(E,C) & r2_hidden(E,D) & r2_hidden(F,B) & r2_hidden(I,B) & r2_hidden(G,C) & r2_hidden(J,C) & r2_hidden(H,D) & r2_hidden(K,D) & v1_aff_1(B,A) & v1_aff_1(C,A) & v1_aff_1(D,A) & r2_analoaf(A,F,G,I,J) & r2_analoaf(A,F,H,I,K) ) => ( E = F | E = G | E = H | B = C | B = D | r2_analoaf(A,G,H,J,K) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ), file(aff_2,d4_aff_2), []). fof(dt_k1_zfmisc_1,axiom,( $true ), file(zfmisc_1,k1_zfmisc_1), []). fof(dt_l1_analoaf,axiom,( ! [A] : ( l1_analoaf(A) => l1_struct_0(A) ) ), file(analoaf,l1_analoaf), []). fof(dt_l1_struct_0,axiom,( $true ), file(struct_0,l1_struct_0), []). fof(dt_m1_subset_1,axiom,( $true ), file(subset_1,m1_subset_1), []). fof(dt_u1_struct_0,axiom,( $true ), file(struct_0,u1_struct_0), []). fof(existence_l1_analoaf,axiom,( ? [A] : l1_analoaf(A) ), file(analoaf,l1_analoaf), []). fof(existence_l1_struct_0,axiom,( ? [A] : l1_struct_0(A) ), file(struct_0,l1_struct_0), []). fof(existence_m1_subset_1,axiom,( ! [A] : ? [B] : m1_subset_1(B,A) ), file(subset_1,m1_subset_1), []). fof(redefinition_r4_aff_1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) => ( r4_aff_1(A,B,C) <=> r3_aff_1(A,B,C) ) ) ), file(aff_1,r4_aff_1), []). fof(reflexivity_r1_tarski,axiom,( ! [A,B] : r1_tarski(A,A) ), file(tarski,r1_tarski), []). fof(symmetry_r4_aff_1,axiom,( ! [A,B,C] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) & m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) & m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) ) => ( r4_aff_1(A,B,C) => r4_aff_1(A,C,B) ) ) ), file(aff_1,r4_aff_1), []). fof(t11_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r2_analoaf(A,B,C,C,B) & r2_analoaf(A,B,C,B,C) ) ) ) ) ), file(aff_1,t11_aff_1), []). fof(t13_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( r2_analoaf(A,B,C,D,E) => ( r2_analoaf(A,B,C,E,D) & r2_analoaf(A,C,B,D,E) & r2_analoaf(A,C,B,E,D) & r2_analoaf(A,D,E,B,C) & r2_analoaf(A,D,E,C,B) & r2_analoaf(A,E,D,B,C) & r2_analoaf(A,E,D,C,B) ) ) ) ) ) ) ) ), file(aff_1,t13_aff_1), []). fof(t14_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ! [G] : ( m1_subset_1(G,u1_struct_0(A)) => ~ ( B != C & ~ ( ~ ( r2_analoaf(A,B,C,D,E) & r2_analoaf(A,B,C,F,G) ) & ~ ( r2_analoaf(A,B,C,D,E) & r2_analoaf(A,F,G,B,C) ) & ~ ( r2_analoaf(A,D,E,B,C) & r2_analoaf(A,F,G,B,C) ) & ~ ( r2_analoaf(A,D,E,B,C) & r2_analoaf(A,B,C,F,G) ) ) & ~ r2_analoaf(A,D,E,F,G) ) ) ) ) ) ) ) ) ), file(aff_1,t14_aff_1), []). fof(t15_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_aff_1(A,B,C,D) => ( r1_aff_1(A,B,D,C) & r1_aff_1(A,C,B,D) & r1_aff_1(A,C,D,B) & r1_aff_1(A,D,B,C) & r1_aff_1(A,D,C,B) ) ) ) ) ) ) ), file(aff_1,t15_aff_1), []). fof(t16_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ( r1_aff_1(A,B,B,C) & r1_aff_1(A,B,C,C) & r1_aff_1(A,B,C,B) ) ) ) ) ), file(aff_1,t16_aff_1), []). fof(t1_subset,axiom,( ! [A,B] : ( r2_hidden(A,B) => m1_subset_1(A,B) ) ), file(subset,t1_subset), []). fof(t23_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ( ( r1_aff_1(A,B,D,E) & r2_analoaf(A,C,D,C,E) ) => ( r1_aff_1(A,B,C,D) | D = E ) ) ) ) ) ) ) ), file(aff_1,t23_aff_1), []). fof(t2_translac,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ( ? [B] : ( m1_subset_1(B,u1_struct_0(A)) & ? [C] : ( m1_subset_1(C,u1_struct_0(A)) & ? [D] : ( m1_subset_1(D,u1_struct_0(A)) & r1_aff_1(A,B,C,D) & B != C & B != D & C != D ) ) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ~ ( B != C & ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ~ ( r1_aff_1(A,B,C,D) & B != D & C != D ) ) ) ) ) ) ) ), file(translac,t2_translac), []). fof(t33_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ( r1_aff_1(A,B,C,D) <=> ? [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) & v1_aff_1(E,A) & r2_hidden(B,E) & r2_hidden(C,E) & r2_hidden(D,E) ) ) ) ) ) ) ), file(aff_1,t33_aff_1), []). fof(t39_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(E,A) & r2_hidden(B,E) & r2_hidden(C,E) & r1_aff_1(A,B,C,D) ) => ( B = C | r2_hidden(D,E) ) ) ) ) ) ) ) ), file(aff_1,t39_aff_1), []). 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(t52_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ! [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(A))) => ( ( v1_aff_1(F,A) & v1_aff_1(G,A) & r2_hidden(B,F) & r2_hidden(C,F) & r2_hidden(D,G) & r2_hidden(E,G) ) => ( B = C | D = E | ( r3_aff_1(A,F,G) <=> r2_analoaf(A,B,C,D,E) ) ) ) ) ) ) ) ) ) ) ), file(aff_1,t52_aff_1), []). fof(t53_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ! [F] : ( m1_subset_1(F,k1_zfmisc_1(u1_struct_0(A))) => ! [G] : ( m1_subset_1(G,k1_zfmisc_1(u1_struct_0(A))) => ( ( r2_hidden(B,F) & r2_hidden(C,F) & r2_hidden(D,G) & r2_hidden(E,G) & r3_aff_1(A,F,G) ) => r2_analoaf(A,B,C,D,E) ) ) ) ) ) ) ) ) ), file(aff_1,t53_aff_1), []). fof(t55_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ( v1_aff_1(B,A) => r3_aff_1(A,B,B) ) ) ) ), file(aff_1,t55_aff_1), []). fof(t58_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A))) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ~ ( ~ ( r4_aff_1(A,B,C) & r4_aff_1(A,C,D) ) & ~ ( r4_aff_1(A,B,C) & r4_aff_1(A,D,C) ) & ~ ( r4_aff_1(A,C,B) & r4_aff_1(A,C,D) ) & ~ ( r4_aff_1(A,C,B) & r4_aff_1(A,D,C) ) ) => r4_aff_1(A,B,D) ) ) ) ) ) ), file(aff_1,t58_aff_1), []). fof(t59_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,k1_zfmisc_1(u1_struct_0(A))) => ! [D] : ( m1_subset_1(D,k1_zfmisc_1(u1_struct_0(A))) => ( ( r4_aff_1(A,C,D) & r2_hidden(B,C) & r2_hidden(B,D) ) => C = D ) ) ) ) ) ), file(aff_1,t59_aff_1), []). fof(t74_aff_1,axiom,( ! [A] : ( ( ~ v3_struct_0(A) & ~ v3_realset2(A) & v1_diraf(A) & v2_diraf(A) & l1_analoaf(A) ) => ! [B] : ( m1_subset_1(B,u1_struct_0(A)) => ! [C] : ( m1_subset_1(C,u1_struct_0(A)) => ! [D] : ( m1_subset_1(D,u1_struct_0(A)) => ! [E] : ( m1_subset_1(E,u1_struct_0(A)) => ~ ( ~ r2_analoaf(A,B,C,D,E) & ! [F] : ( m1_subset_1(F,u1_struct_0(A)) => ~ ( r1_aff_1(A,B,C,F) & r1_aff_1(A,D,E,F) ) ) ) ) ) ) ) ) ), file(aff_1,t74_aff_1), []).