This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimpi 
 |-  ( D = A -> A = D )
92 91 adantl 
 |-  ( ( C = D /\ D = A ) -> A = D )
93 92 adantr 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> A = D )
94 93 adantr 
 |-  ( ( ( ( C = D /\ D = A ) /\ A = B ) /\ F = { C } ) -> A = D )
95 simpr 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> A = B )
96 64 eqeq1d 
 |-  ( ( C = D /\ D = A ) -> ( A = B <-> C = B ) )
97 96 biimpa 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> C = B )
98 97 eqcomd 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> B = C )
99 1 2 preqsn 
 |-  ( { A , B } = { C } <-> ( A = B /\ B = C ) )
100 95 98 99 sylanbrc 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> { A , B } = { C } )
101 100 eqcomd 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> { C } = { A , B } )
102 101 eqeq2d 
 |-  ( ( ( C = D /\ D = A ) /\ A = B ) -> ( F = { C } <-> F = { A , B } ) )
103 102 biimpa 
 |-  ( ( ( ( C = D /\ D = A ) /\ A = B ) /\ F = { C } ) -> F = { A , B } )
104 94 103 jca 
 |-  ( ( ( ( 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 ex 
 |-  ( ( C = D /\ D = A ) -> ( A = B -> ( F = { C } -> ( A = D /\ F = { A , B } ) ) ) )
107 106 com23 
 |-  ( ( C = D /\ D = A ) -> ( F = { C } -> ( A = B -> ( A = D /\ F = { A , B } ) ) ) )
108 62 107 sylbi 
 |-  ( { C , D } = { A } -> ( F = { C } -> ( A = B -> ( A = D /\ F = { A , B } ) ) ) )
109 61 108 biimtrdi 
 |-  ( E = { C , D } -> ( E = { A } -> ( F = { C } -> ( A = B -> ( A = D /\ F = { A , B } ) ) ) ) )
110 109 com23 
 |-  ( E = { C , D } -> ( F = { C } -> ( E = { A } -> ( A = B -> ( A = D /\ F = { A , B } ) ) ) ) )
111 110 imp 
 |-  ( ( E = { C , D } /\ F = { C } ) -> ( E = { A } -> ( A = B -> ( A = D /\ F = { A , B } ) ) ) )
112 111 com13 
 |-  ( A = B -> ( E = { A } -> ( ( E = { C , D } /\ F = { C } ) -> ( A = D /\ F = { A , B } ) ) ) )
113 112 imp 
 |-  ( ( A = B /\ E = { A } ) -> ( ( E = { C , D } /\ F = { C } ) -> ( A = D /\ F = { A , B } ) ) )
114 89 113 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 } ) ) ) )
115 114 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 } ) ) )
116 74 115 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 } ) ) ) )
117 116 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 } ) ) ) )
118 eqeq1 
 |-  ( E = { C } -> ( E = { A , B } <-> { C } = { A , B } ) )
119 eqcom 
 |-  ( { C } = { A , B } <-> { A , B } = { C } )
120 119 99 bitri 
 |-  ( { C } = { A , B } <-> ( A = B /\ B = C ) )
121 eqtr 
 |-  ( ( A = B /\ B = C ) -> A = C )
122 121 adantr 
 |-  ( ( ( A = B /\ B = C ) /\ E = { C } ) -> A = C )
123 121 eqcomd 
 |-  ( ( A = B /\ B = C ) -> C = A )
124 sneq 
 |-  ( C = A -> { C } = { A } )
125 123 124 syl 
 |-  ( ( A = B /\ B = C ) -> { C } = { A } )
126 125 eqeq2d 
 |-  ( ( A = B /\ B = C ) -> ( E = { C } <-> E = { A } ) )
127 126 biimpa 
 |-  ( ( ( A = B /\ B = C ) /\ E = { C } ) -> E = { A } )
128 122 127 jca 
 |-  ( ( ( A = B /\ B = C ) /\ E = { C } ) -> ( A = C /\ E = { A } ) )
129 128 ex 
 |-  ( ( A = B /\ B = C ) -> ( E = { C } -> ( A = C /\ E = { A } ) ) )
130 129 a1i13 
 |-  ( C = D -> ( ( A = B /\ B = C ) -> ( F = { A } -> ( E = { C } -> ( A = C /\ E = { A } ) ) ) ) )
131 130 com14 
 |-  ( E = { C } -> ( ( A = B /\ B = C ) -> ( F = { A } -> ( C = D -> ( A = C /\ E = { A } ) ) ) ) )
132 120 131 biimtrid 
 |-  ( E = { C } -> ( { C } = { A , B } -> ( F = { A } -> ( C = D -> ( A = C /\ E = { A } ) ) ) ) )
133 118 132 sylbid 
 |-  ( E = { C } -> ( E = { A , B } -> ( F = { A } -> ( C = D -> ( A = C /\ E = { A } ) ) ) ) )
134 133 com24 
 |-  ( E = { C } -> ( C = D -> ( F = { A } -> ( E = { A , B } -> ( A = C /\ E = { A } ) ) ) ) )
135 134 impcom 
 |-  ( ( C = D /\ E = { C } ) -> ( F = { A } -> ( E = { A , B } -> ( A = C /\ E = { A } ) ) ) )
136 135 com13 
 |-  ( E = { A , B } -> ( F = { A } -> ( ( C = D /\ E = { C } ) -> ( A = C /\ E = { A } ) ) ) )
137 136 imp 
 |-  ( ( E = { A , B } /\ F = { A } ) -> ( ( C = D /\ E = { C } ) -> ( A = C /\ E = { A } ) ) )
138 59 adantl 
 |-  ( ( C = D /\ E = { C } ) -> ( E = { A } -> A = C ) )
139 138 com12 
 |-  ( E = { A } -> ( ( C = D /\ E = { C } ) -> A = C ) )
140 139 adantr 
 |-  ( ( E = { A } /\ F = { A , B } ) -> ( ( C = D /\ E = { C } ) -> A = C ) )
141 140 imp 
 |-  ( ( ( E = { A } /\ F = { A , B } ) /\ ( C = D /\ E = { C } ) ) -> A = C )
142 simpl 
 |-  ( ( E = { A } /\ F = { A , B } ) -> E = { A } )
143 142 adantr 
 |-  ( ( ( E = { A } /\ F = { A , B } ) /\ ( C = D /\ E = { C } ) ) -> E = { A } )
144 141 143 jca 
 |-  ( ( ( E = { A } /\ F = { A , B } ) /\ ( C = D /\ E = { C } ) ) -> ( A = C /\ E = { A } ) )
145 144 ex 
 |-  ( ( E = { A } /\ F = { A , B } ) -> ( ( C = D /\ E = { C } ) -> ( A = C /\ E = { A } ) ) )
146 137 145 jaoi 
 |-  ( ( ( E = { A , B } /\ F = { A } ) \/ ( E = { A } /\ F = { A , B } ) ) -> ( ( C = D /\ E = { C } ) -> ( A = C /\ E = { A } ) ) )
147 146 impcom 
 |-  ( ( ( C = D /\ E = { C } ) /\ ( ( E = { A , B } /\ F = { A } ) \/ ( E = { A } /\ F = { A , B } ) ) ) -> ( A = C /\ E = { A } ) )
148 eqeq1 
 |-  ( E = { A , B } -> ( E = { C } <-> { A , B } = { C } ) )
149 simpl 
 |-  ( ( A = B /\ B = C ) -> A = B )
150 149 adantr 
 |-  ( ( ( A = B /\ B = C ) /\ C = D ) -> A = B )
151 150 adantr 
 |-  ( ( ( ( A = B /\ B = C ) /\ C = D ) /\ F = { A } ) -> A = B )
152 eqtr 
 |-  ( ( A = C /\ C = D ) -> A = D )
153 dfsn2 
 |-  { A } = { A , A }
154 preq2 
 |-  ( A = D -> { A , A } = { A , D } )
155 153 154 eqtrid 
 |-  ( A = D -> { A } = { A , D } )
156 152 155 syl 
 |-  ( ( A = C /\ C = D ) -> { A } = { A , D } )
157 156 ex 
 |-  ( A = C -> ( C = D -> { A } = { A , D } ) )
158 121 157 syl 
 |-  ( ( A = B /\ B = C ) -> ( C = D -> { A } = { A , D } ) )
159 158 imp 
 |-  ( ( ( A = B /\ B = C ) /\ C = D ) -> { A } = { A , D } )
160 159 eqeq2d 
 |-  ( ( ( A = B /\ B = C ) /\ C = D ) -> ( F = { A } <-> F = { A , D } ) )
161 160 biimpa 
 |-  ( ( ( ( A = B /\ B = C ) /\ C = D ) /\ F = { A } ) -> F = { A , D } )
162 151 161 jca 
 |-  ( ( ( ( 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 ex 
 |-  ( ( A = B /\ B = C ) -> ( C = D -> ( F = { A } -> ( A = B /\ F = { A , D } ) ) ) )
165 164 com23 
 |-  ( ( A = B /\ B = C ) -> ( F = { A } -> ( C = D -> ( A = B /\ F = { A , D } ) ) ) )
166 99 165 sylbi 
 |-  ( { A , B } = { C } -> ( F = { A } -> ( C = D -> ( A = B /\ F = { A , D } ) ) ) )
167 148 166 biimtrdi 
 |-  ( E = { A , B } -> ( E = { C } -> ( F = { A } -> ( C = D -> ( A = B /\ F = { A , D } ) ) ) ) )
168 167 com23 
 |-  ( E = { A , B } -> ( F = { A } -> ( E = { C } -> ( C = D -> ( A = B /\ F = { A , D } ) ) ) ) )
169 168 imp 
 |-  ( ( E = { A , B } /\ F = { A } ) -> ( E = { C } -> ( C = D -> ( A = B /\ F = { A , D } ) ) ) )
170 169 com13 
 |-  ( C = D -> ( E = { C } -> ( ( E = { A , B } /\ F = { A } ) -> ( A = B /\ F = { A , D } ) ) ) )
171 170 imp 
 |-  ( ( C = D /\ E = { C } ) -> ( ( E = { A , B } /\ F = { A } ) -> ( A = B /\ F = { A , D } ) ) )
172 80 imp 
 |-  ( ( E = { A } /\ E = { C } ) -> C = A )
173 172 eqeq1d 
 |-  ( ( E = { A } /\ E = { C } ) -> ( C = D <-> A = D ) )
174 173 biimpd 
 |-  ( ( E = { A } /\ E = { C } ) -> ( C = D -> A = D ) )
175 174 ex 
 |-  ( E = { A } -> ( E = { C } -> ( C = D -> A = D ) ) )
176 175 com13 
 |-  ( C = D -> ( E = { C } -> ( E = { A } -> A = D ) ) )
177 176 imp 
 |-  ( ( C = D /\ E = { C } ) -> ( E = { A } -> A = D ) )
178 177 anim1d 
 |-  ( ( C = D /\ E = { C } ) -> ( ( E = { A } /\ F = { A , B } ) -> ( A = D /\ F = { A , B } ) ) )
179 171 178 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 } ) ) ) )
180 179 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 } ) ) )
181 147 180 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 } ) ) ) )
182 181 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 } ) ) ) ) )
183 182 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 } ) ) ) ) )
184 183 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 } ) ) ) ) )
185 184 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 } ) ) ) )
186 117 185 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 } ) ) ) )
187 55 186 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 } ) ) ) )
188 13 18 187 3bitr4i 
 |-  ( { <. A , B >. , <. C , D >. } = <. E , F >. <-> ( ( A = C /\ E = { A } ) /\ ( ( A = B /\ F = { A , D } ) \/ ( A = D /\ F = { A , B } ) ) ) )