Metamath Proof Explorer

Theorem propeqop

Description: Equivalence for an ordered pair equal to a pair of ordered pairs. (Contributed by AV, 18-Sep-2020) (Proof shortened by AV, 16-Jun-2022) (Avoid depending on this detail.)

Ref Expression
Hypotheses snopeqop.a 
|- A e. _V
snopeqop.b 
|- B e. _V
propeqop.c 
|- C e. _V
propeqop.d 
|- D e. _V
propeqop.e 
|- E e. _V
propeqop.f 
|- F e. _V
Assertion propeqop 
|- ( { <. A , B >. , <. C , D >. } = <. E , F >. <-> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )

Proof

Step Hyp Ref Expression
1 snopeqop.a 
 |-  A e. _V
2 snopeqop.b 
 |-  B e. _V
3 propeqop.c 
 |-  C e. _V
4 propeqop.d 
 |-  D e. _V
5 propeqop.e 
 |-  E e. _V
6 propeqop.f 
 |-  F e. _V
7 1 2 opeqsn 
 |-  ( <. A , B >. = { E } <-> ( A = B /\ E = { A } ) )
8 3 4 5 6 opeqpr 
 |-  ( <. C , D >. = { E , F } <-> ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) )
9 7 8 anbi12i 
 |-  ( ( <. A , B >. = { E } /\ <. C , D >. = { E , F } ) <-> ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) )
10 1 2 5 6 opeqpr 
 |-  ( <. A , B >. = { E , F } <-> ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) )
11 3 4 opeqsn 
 |-  ( <. C , D >. = { E } <-> ( C = D /\ E = { C } ) )
12 10 11 anbi12i 
 |-  ( ( <. A , B >. = { E , F } /\ <. C , D >. = { E } ) <-> ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) )
13 9 12 orbi12i 
 |-  ( ( ( <. A , B >. = { E } /\ <. C , D >. = { E , F } ) \/ ( <. A , B >. = { E , F } /\ <. C , D >. = { E } ) ) <-> ( ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) \/ ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) ) )
14 eqcom 
 |-  ( { <. A , B >. , <. C , D >. } = <. E , F >. <-> <. E , F >. = { <. A , B >. , <. C , D >. } )
15 opex 
 |-  <. A , B >. e. _V
16 opex 
 |-  <. C , D >. e. _V
17 5 6 15 16 opeqpr 
 |-  ( <. E , F >. = { <. A , B >. , <. C , D >. } <-> ( ( <. A , B >. = { E } /\ <. C , D >. = { E , F } ) \/ ( <. A , B >. = { E , F } /\ <. C , D >. = { E } ) ) )
18 14 17 bitri 
 |-  ( { <. A , B >. , <. C , D >. } = <. E , F >. <-> ( ( <. A , B >. = { E } /\ <. C , D >. = { E , F } ) \/ ( <. A , B >. = { E , F } /\ <. C , D >. = { E } ) ) )
19 simpl 
 |-  ( ( A = B /\ F = { A , D } ) -> A = B )
20 simpr 
 |-  ( ( A = C /\ E = { A } ) -> E = { A } )
21 19 20 anim12i 
 |-  ( ( ( A = B /\ F = { A , D } ) /\ ( A = C /\ E = { A } ) ) -> ( A = B /\ E = { A } ) )
22 sneq 
 |-  ( A = C -> { A } = { C } )
23 22 eqeq2d 
 |-  ( A = C -> ( E = { A } <-> E = { C } ) )
24 23 biimpa 
 |-  ( ( A = C /\ E = { A } ) -> E = { C } )
25 24 adantl 
 |-  ( ( ( A = B /\ F = { A , D } ) /\ ( A = C /\ E = { A } ) ) -> E = { C } )
26 preq1 
 |-  ( A = C -> { A , D } = { C , D } )
27 26 adantr 
 |-  ( ( A = C /\ E = { A } ) -> { A , D } = { C , D } )
28 27 eqeq2d 
 |-  ( ( A = C /\ E = { A } ) -> ( F = { A , D } <-> F = { C , D } ) )
29 28 biimpcd 
 |-  ( F = { A , D } -> ( ( A = C /\ E = { A } ) -> F = { C , D } ) )
30 29 adantl 
 |-  ( ( A = B /\ F = { A , D } ) -> ( ( A = C /\ E = { A } ) -> F = { C , D } ) )
31 30 imp 
 |-  ( ( ( A = B /\ F = { A , D } ) /\ ( A = C /\ E = { A } ) ) -> F = { C , D } )
32 25 31 jca 
 |-  ( ( ( A = B /\ F = { A , D } ) /\ ( A = C /\ E = { A } ) ) -> ( E = { C } /\ F = { C , D } ) )
33 32 orcd 
 |-  ( ( ( A = B /\ F = { A , D } ) /\ ( A = C /\ E = { A } ) ) -> ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) )
34 21 33 jca 
 |-  ( ( ( A = B /\ F = { A , D } ) /\ ( A = C /\ E = { A } ) ) -> ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) )
35 34 orcd 
 |-  ( ( ( A = B /\ F = { A , D } ) /\ ( A = C /\ E = { A } ) ) -> ( ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) \/ ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) ) )
36 35 ex 
 |-  ( ( A = B /\ F = { A , D } ) -> ( ( A = C /\ E = { A } ) -> ( ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) \/ ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) ) ) )
37 simpr 
 |-  ( ( A = D /\ F = { A , B } ) -> F = { A , B } )
38 20 37 anim12i 
 |-  ( ( ( A = C /\ E = { A } ) /\ ( A = D /\ F = { A , B } ) ) -> ( E = { A } /\ F = { A , B } ) )
39 38 ancoms 
 |-  ( ( ( A = D /\ F = { A , B } ) /\ ( A = C /\ E = { A } ) ) -> ( E = { A } /\ F = { A , B } ) )
40 39 orcd 
 |-  ( ( ( A = D /\ F = { A , B } ) /\ ( A = C /\ E = { A } ) ) -> ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) )
41 simpl 
 |-  ( ( A = C /\ E = { A } ) -> A = C )
42 41 eqeq1d 
 |-  ( ( A = C /\ E = { A } ) -> ( A = D <-> C = D ) )
43 42 biimpcd 
 |-  ( A = D -> ( ( A = C /\ E = { A } ) -> C = D ) )
44 43 adantr 
 |-  ( ( A = D /\ F = { A , B } ) -> ( ( A = C /\ E = { A } ) -> C = D ) )
45 44 imp 
 |-  ( ( ( A = D /\ F = { A , B } ) /\ ( A = C /\ E = { A } ) ) -> C = D )
46 23 biimpd 
 |-  ( A = C -> ( E = { A } -> E = { C } ) )
47 46 a1dd 
 |-  ( A = C -> ( E = { A } -> ( ( A = D /\ F = { A , B } ) -> E = { C } ) ) )
48 47 imp 
 |-  ( ( A = C /\ E = { A } ) -> ( ( A = D /\ F = { A , B } ) -> E = { C } ) )
49 48 impcom 
 |-  ( ( ( A = D /\ F = { A , B } ) /\ ( A = C /\ E = { A } ) ) -> E = { C } )
50 45 49 jca 
 |-  ( ( ( A = D /\ F = { A , B } ) /\ ( A = C /\ E = { A } ) ) -> ( C = D /\ E = { C } ) )
51 40 50 jca 
 |-  ( ( ( A = D /\ F = { A , B } ) /\ ( A = C /\ E = { A } ) ) -> ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) )
52 51 olcd 
 |-  ( ( ( A = D /\ F = { A , B } ) /\ ( A = C /\ E = { A } ) ) -> ( ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) \/ ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) ) )
53 52 ex 
 |-  ( ( A = D /\ F = { A , B } ) -> ( ( A = C /\ E = { A } ) -> ( ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) \/ ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) ) ) )
54 36 53 jaoi 
 |-  ( ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) -> ( ( A = C /\ E = { A } ) -> ( ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) \/ ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) ) ) )
55 54 impcom 
 |-  ( ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) -> ( ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) \/ ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) ) )
56 eqeq1 
 |-  ( E = { C } -> ( E = { A } <-> { C } = { A } ) )
57 3 sneqr 
 |-  ( { C } = { A } -> C = A )
58 57 eqcomd 
 |-  ( { C } = { A } -> A = C )
59 56 58 biimtrdi 
 |-  ( E = { C } -> ( E = { A } -> A = C ) )
60 59 adantr 
 |-  ( ( E = { C } /\ F = { C , D } ) -> ( E = { A } -> A = C ) )
61 eqeq1 
 |-  ( E = { C , D } -> ( E = { A } <-> { C , D } = { A } ) )
62 3 4 preqsn 
 |-  ( { C , D } = { A } <-> ( C = D /\ D = A ) )
63 eqtr 
 |-  ( ( C = D /\ D = A ) -> C = A )
64 63 eqcomd 
 |-  ( ( C = D /\ D = A ) -> A = C )
65 62 64 sylbi 
 |-  ( { C , D } = { A } -> A = C )
66 61 65 biimtrdi 
 |-  ( E = { C , D } -> ( E = { A } -> A = C ) )
67 66 adantr 
 |-  ( ( E = { C , D } /\ F = { C } ) -> ( E = { A } -> A = C ) )
68 60 67 jaoi 
 |-  ( ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) -> ( E = { A } -> A = C ) )
69 68 com12 
 |-  ( E = { A } -> ( ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) -> A = C ) )
70 69 adantl 
 |-  ( ( A = B /\ E = { A } ) -> ( ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) -> A = C ) )
71 70 impcom 
 |-  ( ( ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) /\ ( A = B /\ E = { A } ) ) -> A = C )
72 simpr 
 |-  ( ( A = B /\ E = { A } ) -> E = { A } )
73 72 adantl 
 |-  ( ( ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) /\ ( A = B /\ E = { A } ) ) -> E = { A } )
74 71 73 jca 
 |-  ( ( ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) /\ ( A = B /\ E = { A } ) ) -> ( A = C /\ E = { A } ) )
75 simpl 
 |-  ( ( A = B /\ E = { A } ) -> A = B )
76 75 adantr 
 |-  ( ( ( A = B /\ E = { A } ) /\ ( E = { C } /\ F = { C , D } ) ) -> A = B )
77 eqeq1 
 |-  ( E = { A } -> ( E = { C } <-> { A } = { C } ) )
78 1 sneqr 
 |-  ( { A } = { C } -> A = C )
79 78 eqcomd 
 |-  ( { A } = { C } -> C = A )
80 77 79 biimtrdi 
 |-  ( E = { A } -> ( E = { C } -> C = A ) )
81 80 adantl 
 |-  ( ( A = B /\ E = { A } ) -> ( E = { C } -> C = A ) )
82 81 impcom 
 |-  ( ( E = { C } /\ ( A = B /\ E = { A } ) ) -> C = A )
83 82 preq1d 
 |-  ( ( E = { C } /\ ( A = B /\ E = { A } ) ) -> { C , D } = { A , D } )
84 83 eqeq2d 
 |-  ( ( E = { C } /\ ( A = B /\ E = { A } ) ) -> ( F = { C , D } <-> F = { A , D } ) )
85 84 biimpd 
 |-  ( ( E = { C } /\ ( A = B /\ E = { A } ) ) -> ( F = { C , D } -> F = { A , D } ) )
86 85 impancom 
 |-  ( ( E = { C } /\ F = { C , D } ) -> ( ( A = B /\ E = { A } ) -> F = { A , D } ) )
87 86 impcom 
 |-  ( ( ( A = B /\ E = { A } ) /\ ( E = { C } /\ F = { C , D } ) ) -> F = { A , D } )
88 76 87 jca 
 |-  ( ( ( A = B /\ E = { A } ) /\ ( E = { C } /\ F = { C , D } ) ) -> ( A = B /\ F = { A , D } ) )
89 88 ex 
 |-  ( ( A = B /\ E = { A } ) -> ( ( E = { C } /\ F = { C , D } ) -> ( A = B /\ F = { A , D } ) ) )
90 eqcom 
 |-  ( D = A <-> A = D )
91 90 bilani 
 |-  ( ( C = D /\ D = A ) -> A = D )
92 91 adantr 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> A = D )
93 92 adantr 
 |-  ( ( ( ( C = D /\ D = A ) /\ A = B ) /\ F = { C } ) -> A = D )
94 simpr 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> A = B )
95 64 eqeq1d 
 |-  ( ( C = D /\ D = A ) -> ( A = B <-> C = B ) )
96 95 biimpa 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> C = B )
97 96 eqcomd 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> B = C )
98 1 2 preqsn 
 |-  ( { A , B } = { C } <-> ( A = B /\ B = C ) )
99 94 97 98 sylanbrc 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> { A , B } = { C } )
100 99 eqcomd 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> { C } = { A , B } )
101 100 eqeq2d 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> ( F = { C } <-> F = { A , B } ) )
102 101 biimpa 
 |-  ( ( ( ( C = D /\ D = A ) /\ A = B ) /\ F = { C } ) -> F = { A , B } )
103 93 102 jca 
 |-  ( ( ( ( C = D /\ D = A ) /\ A = B ) /\ F = { C } ) -> ( A = D /\ F = { A , B } ) )
104 103 ex 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> ( F = { C } -> ( A = D /\ F = { A , B } ) ) )
105 104 ex 
 |-  ( ( C = D /\ D = A ) -> ( A = B -> ( F = { C } -> ( A = D /\ F = { A , B } ) ) ) )
106 105 com23 
 |-  ( ( C = D /\ D = A ) -> ( F = { C } -> ( A = B -> ( A = D /\ F = { A , B } ) ) ) )
107 62 106 sylbi 
 |-  ( { C , D } = { A } -> ( F = { C } -> ( A = B -> ( A = D /\ F = { A , B } ) ) ) )
108 61 107 biimtrdi 
 |-  ( E = { C , D } -> ( E = { A } -> ( F = { C } -> ( A = B -> ( A = D /\ F = { A , B } ) ) ) ) )
109 108 com23 
 |-  ( E = { C , D } -> ( F = { C } -> ( E = { A } -> ( A = B -> ( A = D /\ F = { A , B } ) ) ) ) )
110 109 imp 
 |-  ( ( E = { C , D } /\ F = { C } ) -> ( E = { A } -> ( A = B -> ( A = D /\ F = { A , B } ) ) ) )
111 110 com13 
 |-  ( A = B -> ( E = { A } -> ( ( E = { C , D } /\ F = { C } ) -> ( A = D /\ F = { A , B } ) ) ) )
112 111 imp 
 |-  ( ( A = B /\ E = { A } ) -> ( ( E = { C , D } /\ F = { C } ) -> ( A = D /\ F = { A , B } ) ) )
113 89 112 orim12d 
 |-  ( ( A = B /\ E = { A } ) -> ( ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) -> ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
114 113 impcom 
 |-  ( ( ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) /\ ( A = B /\ E = { A } ) ) -> ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) )
115 74 114 jca 
 |-  ( ( ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) /\ ( A = B /\ E = { A } ) ) -> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
116 115 ancoms 
 |-  ( ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) -> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
117 eqeq1 
 |-  ( E = { C } -> ( E = { A , B } <-> { C } = { A , B } ) )
118 eqcom 
 |-  ( { C } = { A , B } <-> { A , B } = { C } )
119 118 98 bitri 
 |-  ( { C } = { A , B } <-> ( A = B /\ B = C ) )
120 eqtr 
 |-  ( ( A = B /\ B = C ) -> A = C )
121 120 adantr 
 |-  ( ( ( A = B /\ B = C ) /\ E = { C } ) -> A = C )
122 120 eqcomd 
 |-  ( ( A = B /\ B = C ) -> C = A )
123 sneq 
 |-  ( C = A -> { C } = { A } )
124 122 123 syl 
 |-  ( ( A = B /\ B = C ) -> { C } = { A } )
125 124 eqeq2d 
 |-  ( ( A = B /\ B = C ) -> ( E = { C } <-> E = { A } ) )
126 125 biimpa 
 |-  ( ( ( A = B /\ B = C ) /\ E = { C } ) -> E = { A } )
127 121 126 jca 
 |-  ( ( ( A = B /\ B = C ) /\ E = { C } ) -> ( A = C /\ E = { A } ) )
128 127 ex 
 |-  ( ( A = B /\ B = C ) -> ( E = { C } -> ( A = C /\ E = { A } ) ) )
129 128 a1i13 
 |-  ( C = D -> ( ( A = B /\ B = C ) -> ( F = { A } -> ( E = { C } -> ( A = C /\ E = { A } ) ) ) ) )
130 129 com14 
 |-  ( E = { C } -> ( ( A = B /\ B = C ) -> ( F = { A } -> ( C = D -> ( A = C /\ E = { A } ) ) ) ) )
131 119 130 biimtrid 
 |-  ( E = { C } -> ( { C } = { A , B } -> ( F = { A } -> ( C = D -> ( A = C /\ E = { A } ) ) ) ) )
132 117 131 sylbid 
 |-  ( E = { C } -> ( E = { A , B } -> ( F = { A } -> ( C = D -> ( A = C /\ E = { A } ) ) ) ) )
133 132 com24 
 |-  ( E = { C } -> ( C = D -> ( F = { A } -> ( E = { A , B } -> ( A = C /\ E = { A } ) ) ) ) )
134 133 impcom 
 |-  ( ( C = D /\ E = { C } ) -> ( F = { A } -> ( E = { A , B } -> ( A = C /\ E = { A } ) ) ) )
135 134 com13 
 |-  ( E = { A , B } -> ( F = { A } -> ( ( C = D /\ E = { C } ) -> ( A = C /\ E = { A } ) ) ) )
136 135 imp 
 |-  ( ( E = { A , B } /\ F = { A } ) -> ( ( C = D /\ E = { C } ) -> ( A = C /\ E = { A } ) ) )
137 59 adantl 
 |-  ( ( C = D /\ E = { C } ) -> ( E = { A } -> A = C ) )
138 137 com12 
 |-  ( E = { A } -> ( ( C = D /\ E = { C } ) -> A = C ) )
139 138 adantr 
 |-  ( ( E = { A } /\ F = { A , B } ) -> ( ( C = D /\ E = { C } ) -> A = C ) )
140 139 imp 
 |-  ( ( ( E = { A } /\ F = { A , B } ) /\ ( C = D /\ E = { C } ) ) -> A = C )
141 simpl 
 |-  ( ( E = { A } /\ F = { A , B } ) -> E = { A } )
142 141 adantr 
 |-  ( ( ( E = { A } /\ F = { A , B } ) /\ ( C = D /\ E = { C } ) ) -> E = { A } )
143 140 142 jca 
 |-  ( ( ( E = { A } /\ F = { A , B } ) /\ ( C = D /\ E = { C } ) ) -> ( A = C /\ E = { A } ) )
144 143 ex 
 |-  ( ( E = { A } /\ F = { A , B } ) -> ( ( C = D /\ E = { C } ) -> ( A = C /\ E = { A } ) ) )
145 136 144 jaoi 
 |-  ( ( ( E = { A , B } /\ F = { A } ) \/ ( E = { A } /\ F = { A , B } ) ) -> ( ( C = D /\ E = { C } ) -> ( A = C /\ E = { A } ) ) )
146 145 impcom 
 |-  ( ( ( C = D /\ E = { C } ) /\ ( ( E = { A , B } /\ F = { A } ) \/ ( E = { A } /\ F = { A , B } ) ) ) -> ( A = C /\ E = { A } ) )
147 eqeq1 
 |-  ( E = { A , B } -> ( E = { C } <-> { A , B } = { C } ) )
148 simpl 
 |-  ( ( A = B /\ B = C ) -> A = B )
149 148 adantr 
 |-  ( ( ( A = B /\ B = C ) /\ C = D ) -> A = B )
150 149 adantr 
 |-  ( ( ( ( A = B /\ B = C ) /\ C = D ) /\ F = { A } ) -> A = B )
151 eqtr 
 |-  ( ( A = C /\ C = D ) -> A = D )
152 dfsn2 
 |-  { A } = { A , A }
153 preq2 
 |-  ( A = D -> { A , A } = { A , D } )
154 152 153 eqtrid 
 |-  ( A = D -> { A } = { A , D } )
155 151 154 syl 
 |-  ( ( A = C /\ C = D ) -> { A } = { A , D } )
156 155 ex 
 |-  ( A = C -> ( C = D -> { A } = { A , D } ) )
157 120 156 syl 
 |-  ( ( A = B /\ B = C ) -> ( C = D -> { A } = { A , D } ) )
158 157 imp 
 |-  ( ( ( A = B /\ B = C ) /\ C = D ) -> { A } = { A , D } )
159 158 eqeq2d 
 |-  ( ( ( A = B /\ B = C ) /\ C = D ) -> ( F = { A } <-> F = { A , D } ) )
160 159 biimpa 
 |-  ( ( ( ( A = B /\ B = C ) /\ C = D ) /\ F = { A } ) -> F = { A , D } )
161 150 160 jca 
 |-  ( ( ( ( A = B /\ B = C ) /\ C = D ) /\ F = { A } ) -> ( A = B /\ F = { A , D } ) )
162 161 ex 
 |-  ( ( ( A = B /\ B = C ) /\ C = D ) -> ( F = { A } -> ( A = B /\ F = { A , D } ) ) )
163 162 ex 
 |-  ( ( A = B /\ B = C ) -> ( C = D -> ( F = { A } -> ( A = B /\ F = { A , D } ) ) ) )
164 163 com23 
 |-  ( ( A = B /\ B = C ) -> ( F = { A } -> ( C = D -> ( A = B /\ F = { A , D } ) ) ) )
165 98 164 sylbi 
 |-  ( { A , B } = { C } -> ( F = { A } -> ( C = D -> ( A = B /\ F = { A , D } ) ) ) )
166 147 165 biimtrdi 
 |-  ( E = { A , B } -> ( E = { C } -> ( F = { A } -> ( C = D -> ( A = B /\ F = { A , D } ) ) ) ) )
167 166 com23 
 |-  ( E = { A , B } -> ( F = { A } -> ( E = { C } -> ( C = D -> ( A = B /\ F = { A , D } ) ) ) ) )
168 167 imp 
 |-  ( ( E = { A , B } /\ F = { A } ) -> ( E = { C } -> ( C = D -> ( A = B /\ F = { A , D } ) ) ) )
169 168 com13 
 |-  ( C = D -> ( E = { C } -> ( ( E = { A , B } /\ F = { A } ) -> ( A = B /\ F = { A , D } ) ) ) )
170 169 imp 
 |-  ( ( C = D /\ E = { C } ) -> ( ( E = { A , B } /\ F = { A } ) -> ( A = B /\ F = { A , D } ) ) )
171 80 imp 
 |-  ( ( E = { A } /\ E = { C } ) -> C = A )
172 171 eqeq1d 
 |-  ( ( E = { A } /\ E = { C } ) -> ( C = D <-> A = D ) )
173 172 biimpd 
 |-  ( ( E = { A } /\ E = { C } ) -> ( C = D -> A = D ) )
174 173 ex 
 |-  ( E = { A } -> ( E = { C } -> ( C = D -> A = D ) ) )
175 174 com13 
 |-  ( C = D -> ( E = { C } -> ( E = { A } -> A = D ) ) )
176 175 imp 
 |-  ( ( C = D /\ E = { C } ) -> ( E = { A } -> A = D ) )
177 176 anim1d 
 |-  ( ( C = D /\ E = { C } ) -> ( ( E = { A } /\ F = { A , B } ) -> ( A = D /\ F = { A , B } ) ) )
178 170 177 orim12d 
 |-  ( ( C = D /\ E = { C } ) -> ( ( ( E = { A , B } /\ F = { A } ) \/ ( E = { A } /\ F = { A , B } ) ) -> ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
179 178 imp 
 |-  ( ( ( C = D /\ E = { C } ) /\ ( ( E = { A , B } /\ F = { A } ) \/ ( E = { A } /\ F = { A , B } ) ) ) -> ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) )
180 146 179 jca 
 |-  ( ( ( C = D /\ E = { C } ) /\ ( ( E = { A , B } /\ F = { A } ) \/ ( E = { A } /\ F = { A , B } ) ) ) -> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
181 180 ex 
 |-  ( ( C = D /\ E = { C } ) -> ( ( ( E = { A , B } /\ F = { A } ) \/ ( E = { A } /\ F = { A , B } ) ) -> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) ) )
182 181 com12 
 |-  ( ( ( E = { A , B } /\ F = { A } ) \/ ( E = { A } /\ F = { A , B } ) ) -> ( ( C = D /\ E = { C } ) -> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) ) )
183 182 orcoms 
 |-  ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) -> ( ( C = D /\ E = { C } ) -> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) ) )
184 183 imp 
 |-  ( ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) -> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
185 116 184 jaoi 
 |-  ( ( ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) \/ ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) ) -> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )
186 55 185 impbii 
 |-  ( ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) <-> ( ( ( A = B /\ E = { A } ) /\ ( ( E = { C } /\ F = { C , D } ) \/ ( E = { C , D } /\ F = { C } ) ) ) \/ ( ( ( E = { A } /\ F = { A , B } ) \/ ( E = { A , B } /\ F = { A } ) ) /\ ( C = D /\ E = { C } ) ) ) )
187 13 18 186 3bitr4i 
 |-  ( { <. A , B >. , <. C , D >. } = <. E , F >. <-> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )