Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  propeqop Structured version   Visualization version   Unicode version

Theorem propeqop 39009
Description: Equivalence for an ordered pair equal to a pair of ordered pairs. (Contributed by AV, 18-Sep-2020.)
Hypotheses
Ref Expression
snopeqop.a  |-  A  e. 
_V
snopeqop.b  |-  B  e. 
_V
snopeqop.c  |-  C  e. 
_V
snopeqop.d  |-  D  e. 
_V
propeqop.e  |-  E  e. 
_V
propeqop.f  |-  F  e. 
_V
Assertion
Ref Expression
propeqop  |-  ( {
<. A ,  B >. , 
<. C ,  D >. }  =  <. E ,  F >.  <-> 
( ( A  =  C  /\  E  =  { A } )  /\  ( ( A  =  B  /\  F  =  { A ,  D } )  \/  ( A  =  D  /\  F  =  { A ,  B } ) ) ) )

Proof of Theorem propeqop
StepHypRef Expression
1 snopeqop.a . . . . 5  |-  A  e. 
_V
2 snopeqop.b . . . . 5  |-  B  e. 
_V
3 propeqop.e . . . . 5  |-  E  e. 
_V
41, 2, 3opeqsn 4700 . . . 4  |-  ( <. A ,  B >.  =  { E }  <->  ( A  =  B  /\  E  =  { A } ) )
5 snopeqop.c . . . . 5  |-  C  e. 
_V
6 snopeqop.d . . . . 5  |-  D  e. 
_V
7 propeqop.f . . . . 5  |-  F  e. 
_V
85, 6, 3, 7opeqpr 4701 . . . 4  |-  ( <. C ,  D >.  =  { E ,  F } 
<->  ( ( E  =  { C }  /\  F  =  { C ,  D } )  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) ) )
94, 8anbi12i 704 . . 3  |-  ( (
<. A ,  B >.  =  { E }  /\  <. C ,  D >.  =  { E ,  F } )  <->  ( ( A  =  B  /\  E  =  { A } )  /\  (
( E  =  { C }  /\  F  =  { C ,  D } )  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) ) ) )
101, 2, 3, 7opeqpr 4701 . . . 4  |-  ( <. A ,  B >.  =  { E ,  F } 
<->  ( ( E  =  { A }  /\  F  =  { A ,  B } )  \/  ( E  =  { A ,  B }  /\  F  =  { A } ) ) )
115, 6, 3opeqsn 4700 . . . 4  |-  ( <. C ,  D >.  =  { E }  <->  ( C  =  D  /\  E  =  { C } ) )
1210, 11anbi12i 704 . . 3  |-  ( (
<. A ,  B >.  =  { E ,  F }  /\  <. C ,  D >.  =  { E }
)  <->  ( ( ( E  =  { A }  /\  F  =  { A ,  B }
)  \/  ( E  =  { A ,  B }  /\  F  =  { A } ) )  /\  ( C  =  D  /\  E  =  { C } ) ) )
139, 12orbi12i 524 . 2  |-  ( ( ( <. 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 2460 . . 3  |-  ( {
<. A ,  B >. , 
<. C ,  D >. }  =  <. E ,  F >.  <->  <. E ,  F >.  =  { <. A ,  B >. ,  <. C ,  D >. } )
15 opex 4667 . . . 4  |-  <. A ,  B >.  e.  _V
16 opex 4667 . . . 4  |-  <. C ,  D >.  e.  _V
173, 7, 15, 16opeqpr 4701 . . 3  |-  ( <. E ,  F >.  =  { <. A ,  B >. ,  <. C ,  D >. }  <->  ( ( <. A ,  B >.  =  { E }  /\  <. C ,  D >.  =  { E ,  F } )  \/  ( <. A ,  B >.  =  { E ,  F }  /\  <. C ,  D >.  =  { E }
) ) )
1814, 17bitri 253 . 2  |-  ( {
<. A ,  B >. , 
<. C ,  D >. }  =  <. E ,  F >.  <-> 
( ( <. A ,  B >.  =  { E }  /\  <. C ,  D >.  =  { E ,  F } )  \/  ( <. A ,  B >.  =  { E ,  F }  /\  <. C ,  D >.  =  { E }
) ) )
19 simpl 459 . . . . . . . . 9  |-  ( ( A  =  B  /\  F  =  { A ,  D } )  ->  A  =  B )
20 simpr 463 . . . . . . . . 9  |-  ( ( A  =  C  /\  E  =  { A } )  ->  E  =  { A } )
2119, 20anim12i 570 . . . . . . . 8  |-  ( ( ( A  =  B  /\  F  =  { A ,  D }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  ( A  =  B  /\  E  =  { A } ) )
22 sneq 3980 . . . . . . . . . . . . 13  |-  ( A  =  C  ->  { A }  =  { C } )
2322eqeq2d 2463 . . . . . . . . . . . 12  |-  ( A  =  C  ->  ( E  =  { A } 
<->  E  =  { C } ) )
2423biimpa 487 . . . . . . . . . . 11  |-  ( ( A  =  C  /\  E  =  { A } )  ->  E  =  { C } )
2524adantl 468 . . . . . . . . . 10  |-  ( ( ( A  =  B  /\  F  =  { A ,  D }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  E  =  { C } )
26 preq1 4054 . . . . . . . . . . . . . . 15  |-  ( A  =  C  ->  { A ,  D }  =  { C ,  D }
)
2726adantr 467 . . . . . . . . . . . . . 14  |-  ( ( A  =  C  /\  E  =  { A } )  ->  { A ,  D }  =  { C ,  D }
)
2827eqeq2d 2463 . . . . . . . . . . . . 13  |-  ( ( A  =  C  /\  E  =  { A } )  ->  ( F  =  { A ,  D }  <->  F  =  { C ,  D }
) )
2928biimpcd 228 . . . . . . . . . . . 12  |-  ( F  =  { A ,  D }  ->  ( ( A  =  C  /\  E  =  { A } )  ->  F  =  { C ,  D } ) )
3029adantl 468 . . . . . . . . . . 11  |-  ( ( A  =  B  /\  F  =  { A ,  D } )  -> 
( ( A  =  C  /\  E  =  { A } )  ->  F  =  { C ,  D }
) )
3130imp 431 . . . . . . . . . 10  |-  ( ( ( A  =  B  /\  F  =  { A ,  D }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  F  =  { C ,  D }
)
3225, 31jca 535 . . . . . . . . 9  |-  ( ( ( A  =  B  /\  F  =  { A ,  D }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  ( E  =  { C }  /\  F  =  { C ,  D } ) )
3332orcd 394 . . . . . . . 8  |-  ( ( ( A  =  B  /\  F  =  { A ,  D }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  ( ( E  =  { C }  /\  F  =  { C ,  D }
)  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) ) )
3421, 33jca 535 . . . . . . 7  |-  ( ( ( A  =  B  /\  F  =  { A ,  D }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  ( ( A  =  B  /\  E  =  { A } )  /\  (
( E  =  { C }  /\  F  =  { C ,  D } )  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) ) ) )
3534orcd 394 . . . . . 6  |-  ( ( ( 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 } ) ) ) )
3635ex 436 . . . . 5  |-  ( ( 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 463 . . . . . . . . . . 11  |-  ( ( A  =  D  /\  F  =  { A ,  B } )  ->  F  =  { A ,  B } )
3820, 37anim12i 570 . . . . . . . . . 10  |-  ( ( ( A  =  C  /\  E  =  { A } )  /\  ( A  =  D  /\  F  =  { A ,  B } ) )  ->  ( E  =  { A }  /\  F  =  { A ,  B } ) )
3938ancoms 455 . . . . . . . . 9  |-  ( ( ( A  =  D  /\  F  =  { A ,  B }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  ( E  =  { A }  /\  F  =  { A ,  B } ) )
4039orcd 394 . . . . . . . 8  |-  ( ( ( A  =  D  /\  F  =  { A ,  B }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  ( ( E  =  { A }  /\  F  =  { A ,  B }
)  \/  ( E  =  { A ,  B }  /\  F  =  { A } ) ) )
41 simpl 459 . . . . . . . . . . . . 13  |-  ( ( A  =  C  /\  E  =  { A } )  ->  A  =  C )
4241eqeq1d 2455 . . . . . . . . . . . 12  |-  ( ( A  =  C  /\  E  =  { A } )  ->  ( A  =  D  <->  C  =  D ) )
4342biimpcd 228 . . . . . . . . . . 11  |-  ( A  =  D  ->  (
( A  =  C  /\  E  =  { A } )  ->  C  =  D ) )
4443adantr 467 . . . . . . . . . 10  |-  ( ( A  =  D  /\  F  =  { A ,  B } )  -> 
( ( A  =  C  /\  E  =  { A } )  ->  C  =  D ) )
4544imp 431 . . . . . . . . 9  |-  ( ( ( A  =  D  /\  F  =  { A ,  B }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  C  =  D )
4623biimpd 211 . . . . . . . . . . . 12  |-  ( A  =  C  ->  ( E  =  { A }  ->  E  =  { C } ) )
4746a1dd 47 . . . . . . . . . . 11  |-  ( A  =  C  ->  ( E  =  { A }  ->  ( ( A  =  D  /\  F  =  { A ,  B } )  ->  E  =  { C } ) ) )
4847imp 431 . . . . . . . . . 10  |-  ( ( A  =  C  /\  E  =  { A } )  ->  (
( A  =  D  /\  F  =  { A ,  B }
)  ->  E  =  { C } ) )
4948impcom 432 . . . . . . . . 9  |-  ( ( ( A  =  D  /\  F  =  { A ,  B }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  E  =  { C } )
5045, 49jca 535 . . . . . . . 8  |-  ( ( ( A  =  D  /\  F  =  { A ,  B }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  ( C  =  D  /\  E  =  { C } ) )
5140, 50jca 535 . . . . . . 7  |-  ( ( ( A  =  D  /\  F  =  { A ,  B }
)  /\  ( A  =  C  /\  E  =  { A } ) )  ->  ( (
( E  =  { A }  /\  F  =  { A ,  B } )  \/  ( E  =  { A ,  B }  /\  F  =  { A } ) )  /\  ( C  =  D  /\  E  =  { C } ) ) )
5251olcd 395 . . . . . 6  |-  ( ( ( 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 } ) ) ) )
5352ex 436 . . . . 5  |-  ( ( 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 } ) ) ) ) )
5436, 53jaoi 381 . . . 4  |-  ( ( ( 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 } ) ) ) ) )
5554impcom 432 . . 3  |-  ( ( ( 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 2457 . . . . . . . . . . . . 13  |-  ( E  =  { C }  ->  ( E  =  { A }  <->  { C }  =  { A } ) )
575sneqr 4142 . . . . . . . . . . . . . 14  |-  ( { C }  =  { A }  ->  C  =  A )
5857eqcomd 2459 . . . . . . . . . . . . 13  |-  ( { C }  =  { A }  ->  A  =  C )
5956, 58syl6bi 232 . . . . . . . . . . . 12  |-  ( E  =  { C }  ->  ( E  =  { A }  ->  A  =  C ) )
6059adantr 467 . . . . . . . . . . 11  |-  ( ( E  =  { C }  /\  F  =  { C ,  D }
)  ->  ( E  =  { A }  ->  A  =  C ) )
61 eqeq1 2457 . . . . . . . . . . . . 13  |-  ( E  =  { C ,  D }  ->  ( E  =  { A }  <->  { C ,  D }  =  { A } ) )
625, 6, 1preqsn 4162 . . . . . . . . . . . . . 14  |-  ( { C ,  D }  =  { A }  <->  ( C  =  D  /\  D  =  A ) )
63 eqtr 2472 . . . . . . . . . . . . . . 15  |-  ( ( C  =  D  /\  D  =  A )  ->  C  =  A )
6463eqcomd 2459 . . . . . . . . . . . . . 14  |-  ( ( C  =  D  /\  D  =  A )  ->  A  =  C )
6562, 64sylbi 199 . . . . . . . . . . . . 13  |-  ( { C ,  D }  =  { A }  ->  A  =  C )
6661, 65syl6bi 232 . . . . . . . . . . . 12  |-  ( E  =  { C ,  D }  ->  ( E  =  { A }  ->  A  =  C ) )
6766adantr 467 . . . . . . . . . . 11  |-  ( ( E  =  { C ,  D }  /\  F  =  { C } )  ->  ( E  =  { A }  ->  A  =  C ) )
6860, 67jaoi 381 . . . . . . . . . 10  |-  ( ( ( E  =  { C }  /\  F  =  { C ,  D } )  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) )  ->  ( E  =  { A }  ->  A  =  C ) )
6968com12 32 . . . . . . . . 9  |-  ( E  =  { A }  ->  ( ( ( E  =  { C }  /\  F  =  { C ,  D }
)  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) )  ->  A  =  C ) )
7069adantl 468 . . . . . . . 8  |-  ( ( A  =  B  /\  E  =  { A } )  ->  (
( ( E  =  { C }  /\  F  =  { C ,  D } )  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) )  ->  A  =  C )
)
7170impcom 432 . . . . . . 7  |-  ( ( ( ( E  =  { C }  /\  F  =  { C ,  D } )  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) )  /\  ( A  =  B  /\  E  =  { A } ) )  ->  A  =  C )
72 simpr 463 . . . . . . . 8  |-  ( ( A  =  B  /\  E  =  { A } )  ->  E  =  { A } )
7372adantl 468 . . . . . . 7  |-  ( ( ( ( E  =  { C }  /\  F  =  { C ,  D } )  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) )  /\  ( A  =  B  /\  E  =  { A } ) )  ->  E  =  { A } )
7471, 73jca 535 . . . . . 6  |-  ( ( ( ( E  =  { C }  /\  F  =  { C ,  D } )  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) )  /\  ( A  =  B  /\  E  =  { A } ) )  -> 
( A  =  C  /\  E  =  { A } ) )
75 simpl 459 . . . . . . . . . . 11  |-  ( ( A  =  B  /\  E  =  { A } )  ->  A  =  B )
7675adantr 467 . . . . . . . . . 10  |-  ( ( ( A  =  B  /\  E  =  { A } )  /\  ( E  =  { C }  /\  F  =  { C ,  D }
) )  ->  A  =  B )
77 eqeq1 2457 . . . . . . . . . . . . . . . . . 18  |-  ( E  =  { A }  ->  ( E  =  { C }  <->  { A }  =  { C } ) )
781sneqr 4142 . . . . . . . . . . . . . . . . . . 19  |-  ( { A }  =  { C }  ->  A  =  C )
7978eqcomd 2459 . . . . . . . . . . . . . . . . . 18  |-  ( { A }  =  { C }  ->  C  =  A )
8077, 79syl6bi 232 . . . . . . . . . . . . . . . . 17  |-  ( E  =  { A }  ->  ( E  =  { C }  ->  C  =  A ) )
8180adantl 468 . . . . . . . . . . . . . . . 16  |-  ( ( A  =  B  /\  E  =  { A } )  ->  ( E  =  { C }  ->  C  =  A ) )
8281impcom 432 . . . . . . . . . . . . . . 15  |-  ( ( E  =  { C }  /\  ( A  =  B  /\  E  =  { A } ) )  ->  C  =  A )
8382preq1d 4060 . . . . . . . . . . . . . 14  |-  ( ( E  =  { C }  /\  ( A  =  B  /\  E  =  { A } ) )  ->  { C ,  D }  =  { A ,  D }
)
8483eqeq2d 2463 . . . . . . . . . . . . 13  |-  ( ( E  =  { C }  /\  ( A  =  B  /\  E  =  { A } ) )  ->  ( F  =  { C ,  D } 
<->  F  =  { A ,  D } ) )
8584biimpd 211 . . . . . . . . . . . 12  |-  ( ( E  =  { C }  /\  ( A  =  B  /\  E  =  { A } ) )  ->  ( F  =  { C ,  D }  ->  F  =  { A ,  D }
) )
8685impancom 442 . . . . . . . . . . 11  |-  ( ( E  =  { C }  /\  F  =  { C ,  D }
)  ->  ( ( A  =  B  /\  E  =  { A } )  ->  F  =  { A ,  D } ) )
8786impcom 432 . . . . . . . . . 10  |-  ( ( ( A  =  B  /\  E  =  { A } )  /\  ( E  =  { C }  /\  F  =  { C ,  D }
) )  ->  F  =  { A ,  D } )
8876, 87jca 535 . . . . . . . . 9  |-  ( ( ( A  =  B  /\  E  =  { A } )  /\  ( E  =  { C }  /\  F  =  { C ,  D }
) )  ->  ( A  =  B  /\  F  =  { A ,  D } ) )
8988ex 436 . . . . . . . 8  |-  ( ( A  =  B  /\  E  =  { A } )  ->  (
( E  =  { C }  /\  F  =  { C ,  D } )  ->  ( A  =  B  /\  F  =  { A ,  D } ) ) )
90 eqcom 2460 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( D  =  A  <->  A  =  D )
9190biimpi 198 . . . . . . . . . . . . . . . . . . . . 21  |-  ( D  =  A  ->  A  =  D )
9291adantl 468 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( C  =  D  /\  D  =  A )  ->  A  =  D )
9392adantr 467 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( C  =  D  /\  D  =  A )  /\  A  =  B )  ->  A  =  D )
9493adantr 467 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( C  =  D  /\  D  =  A )  /\  A  =  B )  /\  F  =  { C } )  ->  A  =  D )
95 simpr 463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( C  =  D  /\  D  =  A )  /\  A  =  B )  ->  A  =  B )
9664eqeq1d 2455 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( C  =  D  /\  D  =  A )  ->  ( A  =  B  <-> 
C  =  B ) )
9796biimpa 487 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( C  =  D  /\  D  =  A )  /\  A  =  B )  ->  C  =  B )
9897eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( C  =  D  /\  D  =  A )  /\  A  =  B )  ->  B  =  C )
991, 2, 5preqsn 4162 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( { A ,  B }  =  { C }  <->  ( A  =  B  /\  B  =  C ) )
10095, 98, 99sylanbrc 671 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( C  =  D  /\  D  =  A )  /\  A  =  B )  ->  { A ,  B }  =  { C } )
101100eqcomd 2459 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( C  =  D  /\  D  =  A )  /\  A  =  B )  ->  { C }  =  { A ,  B } )
102101eqeq2d 2463 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( C  =  D  /\  D  =  A )  /\  A  =  B )  ->  ( F  =  { C } 
<->  F  =  { A ,  B } ) )
103102biimpa 487 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( C  =  D  /\  D  =  A )  /\  A  =  B )  /\  F  =  { C } )  ->  F  =  { A ,  B }
)
10494, 103jca 535 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( C  =  D  /\  D  =  A )  /\  A  =  B )  /\  F  =  { C } )  ->  ( A  =  D  /\  F  =  { A ,  B } ) )
105104ex 436 . . . . . . . . . . . . . . . 16  |-  ( ( ( C  =  D  /\  D  =  A )  /\  A  =  B )  ->  ( F  =  { C }  ->  ( A  =  D  /\  F  =  { A ,  B } ) ) )
106105ex 436 . . . . . . . . . . . . . . 15  |-  ( ( C  =  D  /\  D  =  A )  ->  ( A  =  B  ->  ( F  =  { C }  ->  ( A  =  D  /\  F  =  { A ,  B } ) ) ) )
107106com23 81 . . . . . . . . . . . . . 14  |-  ( ( C  =  D  /\  D  =  A )  ->  ( F  =  { C }  ->  ( A  =  B  ->  ( A  =  D  /\  F  =  { A ,  B } ) ) ) )
10862, 107sylbi 199 . . . . . . . . . . . . 13  |-  ( { C ,  D }  =  { A }  ->  ( F  =  { C }  ->  ( A  =  B  ->  ( A  =  D  /\  F  =  { A ,  B } ) ) ) )
10961, 108syl6bi 232 . . . . . . . . . . . 12  |-  ( E  =  { C ,  D }  ->  ( E  =  { A }  ->  ( F  =  { C }  ->  ( A  =  B  ->  ( A  =  D  /\  F  =  { A ,  B } ) ) ) ) )
110109com23 81 . . . . . . . . . . 11  |-  ( E  =  { C ,  D }  ->  ( F  =  { C }  ->  ( E  =  { A }  ->  ( A  =  B  ->  ( A  =  D  /\  F  =  { A ,  B } ) ) ) ) )
111110imp 431 . . . . . . . . . 10  |-  ( ( E  =  { C ,  D }  /\  F  =  { C } )  ->  ( E  =  { A }  ->  ( A  =  B  -> 
( A  =  D  /\  F  =  { A ,  B }
) ) ) )
112111com13 83 . . . . . . . . 9  |-  ( A  =  B  ->  ( E  =  { A }  ->  ( ( E  =  { C ,  D }  /\  F  =  { C } )  ->  ( A  =  D  /\  F  =  { A ,  B } ) ) ) )
113112imp 431 . . . . . . . 8  |-  ( ( A  =  B  /\  E  =  { A } )  ->  (
( E  =  { C ,  D }  /\  F  =  { C } )  ->  ( A  =  D  /\  F  =  { A ,  B } ) ) )
11489, 113orim12d 850 . . . . . . 7  |-  ( ( A  =  B  /\  E  =  { A } )  ->  (
( ( E  =  { C }  /\  F  =  { C ,  D } )  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) )  -> 
( ( A  =  B  /\  F  =  { A ,  D } )  \/  ( A  =  D  /\  F  =  { A ,  B } ) ) ) )
115114impcom 432 . . . . . 6  |-  ( ( ( ( E  =  { C }  /\  F  =  { C ,  D } )  \/  ( E  =  { C ,  D }  /\  F  =  { C } ) )  /\  ( A  =  B  /\  E  =  { A } ) )  -> 
( ( A  =  B  /\  F  =  { A ,  D } )  \/  ( A  =  D  /\  F  =  { A ,  B } ) ) )
11674, 115jca 535 . . . . 5  |-  ( ( ( ( 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 } ) ) ) )
117116ancoms 455 . . . 4  |-  ( ( ( 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 2457 . . . . . . . . . . . . . . . 16  |-  ( E  =  { C }  ->  ( E  =  { A ,  B }  <->  { C }  =  { A ,  B }
) )
119 eqcom 2460 . . . . . . . . . . . . . . . . . 18  |-  ( { C }  =  { A ,  B }  <->  { A ,  B }  =  { C } )
120119, 99bitri 253 . . . . . . . . . . . . . . . . 17  |-  ( { C }  =  { A ,  B }  <->  ( A  =  B  /\  B  =  C )
)
121 eqtr 2472 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  C )
122121adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  =  B  /\  B  =  C )  /\  E  =  { C } )  ->  A  =  C )
123121eqcomd 2459 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( A  =  B  /\  B  =  C )  ->  C  =  A )
124 sneq 3980 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( C  =  A  ->  { C }  =  { A } )
125123, 124syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  =  B  /\  B  =  C )  ->  { C }  =  { A } )
126125eqeq2d 2463 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  =  B  /\  B  =  C )  ->  ( E  =  { C }  <->  E  =  { A } ) )
127126biimpa 487 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  =  B  /\  B  =  C )  /\  E  =  { C } )  ->  E  =  { A } )
128122, 127jca 535 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( A  =  B  /\  B  =  C )  /\  E  =  { C } )  ->  ( A  =  C  /\  E  =  { A } ) )
129128ex 436 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( A  =  B  /\  B  =  C )  ->  ( E  =  { C }  ->  ( A  =  C  /\  E  =  { A } ) ) )
130129a1d 26 . . . . . . . . . . . . . . . . . . 19  |-  ( ( A  =  B  /\  B  =  C )  ->  ( F  =  { A }  ->  ( E  =  { C }  ->  ( A  =  C  /\  E  =  { A } ) ) ) )
131130a1i 11 . . . . . . . . . . . . . . . . . 18  |-  ( C  =  D  ->  (
( A  =  B  /\  B  =  C )  ->  ( F  =  { A }  ->  ( E  =  { C }  ->  ( A  =  C  /\  E  =  { A } ) ) ) ) )
132131com14 91 . . . . . . . . . . . . . . . . 17  |-  ( E  =  { C }  ->  ( ( A  =  B  /\  B  =  C )  ->  ( F  =  { A }  ->  ( C  =  D  ->  ( A  =  C  /\  E  =  { A } ) ) ) ) )
133120, 132syl5bi 221 . . . . . . . . . . . . . . . 16  |-  ( E  =  { C }  ->  ( { C }  =  { A ,  B }  ->  ( F  =  { A }  ->  ( C  =  D  -> 
( A  =  C  /\  E  =  { A } ) ) ) ) )
134118, 133sylbid 219 . . . . . . . . . . . . . . 15  |-  ( E  =  { C }  ->  ( E  =  { A ,  B }  ->  ( F  =  { A }  ->  ( C  =  D  ->  ( A  =  C  /\  E  =  { A } ) ) ) ) )
135134com24 90 . . . . . . . . . . . . . 14  |-  ( E  =  { C }  ->  ( C  =  D  ->  ( F  =  { A }  ->  ( E  =  { A ,  B }  ->  ( A  =  C  /\  E  =  { A } ) ) ) ) )
136135impcom 432 . . . . . . . . . . . . 13  |-  ( ( C  =  D  /\  E  =  { C } )  ->  ( F  =  { A }  ->  ( E  =  { A ,  B }  ->  ( A  =  C  /\  E  =  { A } ) ) ) )
137136com13 83 . . . . . . . . . . . 12  |-  ( E  =  { A ,  B }  ->  ( F  =  { A }  ->  ( ( C  =  D  /\  E  =  { C } )  ->  ( A  =  C  /\  E  =  { A } ) ) ) )
138137imp 431 . . . . . . . . . . 11  |-  ( ( E  =  { A ,  B }  /\  F  =  { A } )  ->  ( ( C  =  D  /\  E  =  { C } )  ->  ( A  =  C  /\  E  =  { A } ) ) )
13959adantl 468 . . . . . . . . . . . . . . . 16  |-  ( ( C  =  D  /\  E  =  { C } )  ->  ( E  =  { A }  ->  A  =  C ) )
140139com12 32 . . . . . . . . . . . . . . 15  |-  ( E  =  { A }  ->  ( ( C  =  D  /\  E  =  { C } )  ->  A  =  C ) )
141140adantr 467 . . . . . . . . . . . . . 14  |-  ( ( E  =  { A }  /\  F  =  { A ,  B }
)  ->  ( ( C  =  D  /\  E  =  { C } )  ->  A  =  C ) )
142141imp 431 . . . . . . . . . . . . 13  |-  ( ( ( E  =  { A }  /\  F  =  { A ,  B } )  /\  ( C  =  D  /\  E  =  { C } ) )  ->  A  =  C )
143 simpl 459 . . . . . . . . . . . . . 14  |-  ( ( E  =  { A }  /\  F  =  { A ,  B }
)  ->  E  =  { A } )
144143adantr 467 . . . . . . . . . . . . 13  |-  ( ( ( E  =  { A }  /\  F  =  { A ,  B } )  /\  ( C  =  D  /\  E  =  { C } ) )  ->  E  =  { A } )
145142, 144jca 535 . . . . . . . . . . . 12  |-  ( ( ( E  =  { A }  /\  F  =  { A ,  B } )  /\  ( C  =  D  /\  E  =  { C } ) )  -> 
( A  =  C  /\  E  =  { A } ) )
146145ex 436 . . . . . . . . . . 11  |-  ( ( E  =  { A }  /\  F  =  { A ,  B }
)  ->  ( ( C  =  D  /\  E  =  { C } )  ->  ( A  =  C  /\  E  =  { A } ) ) )
147138, 146jaoi 381 . . . . . . . . . 10  |-  ( ( ( E  =  { A ,  B }  /\  F  =  { A } )  \/  ( E  =  { A }  /\  F  =  { A ,  B }
) )  ->  (
( C  =  D  /\  E  =  { C } )  ->  ( A  =  C  /\  E  =  { A } ) ) )
148147impcom 432 . . . . . . . . 9  |-  ( ( ( C  =  D  /\  E  =  { C } )  /\  (
( E  =  { A ,  B }  /\  F  =  { A } )  \/  ( E  =  { A }  /\  F  =  { A ,  B }
) ) )  -> 
( A  =  C  /\  E  =  { A } ) )
149 eqeq1 2457 . . . . . . . . . . . . . . . 16  |-  ( E  =  { A ,  B }  ->  ( E  =  { C }  <->  { A ,  B }  =  { C } ) )
150 simpl 459 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  =  B  /\  B  =  C )  ->  A  =  B )
151150adantr 467 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  =  B  /\  B  =  C )  /\  C  =  D )  ->  A  =  B )
152151adantr 467 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  =  B  /\  B  =  C )  /\  C  =  D )  /\  F  =  { A } )  ->  A  =  B )
153 eqtr 2472 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( A  =  C  /\  C  =  D )  ->  A  =  D )
154 dfsn2 3983 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  { A }  =  { A ,  A }
155 preq2 4055 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( A  =  D  ->  { A ,  A }  =  { A ,  D }
)
156154, 155syl5eq 2499 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( A  =  D  ->  { A }  =  { A ,  D } )
157153, 156syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( A  =  C  /\  C  =  D )  ->  { A }  =  { A ,  D }
)
158157ex 436 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  =  C  ->  ( C  =  D  ->  { A }  =  { A ,  D }
) )
159121, 158syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  =  B  /\  B  =  C )  ->  ( C  =  D  ->  { A }  =  { A ,  D } ) )
160159imp 431 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( A  =  B  /\  B  =  C )  /\  C  =  D )  ->  { A }  =  { A ,  D } )
161160eqeq2d 2463 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( A  =  B  /\  B  =  C )  /\  C  =  D )  ->  ( F  =  { A } 
<->  F  =  { A ,  D } ) )
162161biimpa 487 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( A  =  B  /\  B  =  C )  /\  C  =  D )  /\  F  =  { A } )  ->  F  =  { A ,  D }
)
163152, 162jca 535 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( A  =  B  /\  B  =  C )  /\  C  =  D )  /\  F  =  { A } )  ->  ( A  =  B  /\  F  =  { A ,  D } ) )
164163ex 436 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( A  =  B  /\  B  =  C )  /\  C  =  D )  ->  ( F  =  { A }  ->  ( A  =  B  /\  F  =  { A ,  D } ) ) )
165164ex 436 . . . . . . . . . . . . . . . . . 18  |-  ( ( A  =  B  /\  B  =  C )  ->  ( C  =  D  ->  ( F  =  { A }  ->  ( A  =  B  /\  F  =  { A ,  D } ) ) ) )
166165com23 81 . . . . . . . . . . . . . . . . 17  |-  ( ( A  =  B  /\  B  =  C )  ->  ( F  =  { A }  ->  ( C  =  D  ->  ( A  =  B  /\  F  =  { A ,  D } ) ) ) )
16799, 166sylbi 199 . . . . . . . . . . . . . . . 16  |-  ( { A ,  B }  =  { C }  ->  ( F  =  { A }  ->  ( C  =  D  ->  ( A  =  B  /\  F  =  { A ,  D } ) ) ) )
168149, 167syl6bi 232 . . . . . . . . . . . . . . 15  |-  ( E  =  { A ,  B }  ->  ( E  =  { C }  ->  ( F  =  { A }  ->  ( C  =  D  ->  ( A  =  B  /\  F  =  { A ,  D } ) ) ) ) )
169168com23 81 . . . . . . . . . . . . . 14  |-  ( E  =  { A ,  B }  ->  ( F  =  { A }  ->  ( E  =  { C }  ->  ( C  =  D  ->  ( A  =  B  /\  F  =  { A ,  D } ) ) ) ) )
170169imp 431 . . . . . . . . . . . . 13  |-  ( ( E  =  { A ,  B }  /\  F  =  { A } )  ->  ( E  =  { C }  ->  ( C  =  D  -> 
( A  =  B  /\  F  =  { A ,  D }
) ) ) )
171170com13 83 . . . . . . . . . . . 12  |-  ( C  =  D  ->  ( E  =  { C }  ->  ( ( E  =  { A ,  B }  /\  F  =  { A } )  ->  ( A  =  B  /\  F  =  { A ,  D } ) ) ) )
172171imp 431 . . . . . . . . . . 11  |-  ( ( C  =  D  /\  E  =  { C } )  ->  (
( E  =  { A ,  B }  /\  F  =  { A } )  ->  ( A  =  B  /\  F  =  { A ,  D } ) ) )
17380imp 431 . . . . . . . . . . . . . . . . 17  |-  ( ( E  =  { A }  /\  E  =  { C } )  ->  C  =  A )
174173eqeq1d 2455 . . . . . . . . . . . . . . . 16  |-  ( ( E  =  { A }  /\  E  =  { C } )  ->  ( C  =  D  <->  A  =  D ) )
175174biimpd 211 . . . . . . . . . . . . . . 15  |-  ( ( E  =  { A }  /\  E  =  { C } )  ->  ( C  =  D  ->  A  =  D ) )
176175ex 436 . . . . . . . . . . . . . 14  |-  ( E  =  { A }  ->  ( E  =  { C }  ->  ( C  =  D  ->  A  =  D ) ) )
177176com13 83 . . . . . . . . . . . . 13  |-  ( C  =  D  ->  ( E  =  { C }  ->  ( E  =  { A }  ->  A  =  D ) ) )
178177imp 431 . . . . . . . . . . . 12  |-  ( ( C  =  D  /\  E  =  { C } )  ->  ( E  =  { A }  ->  A  =  D ) )
179178anim1d 568 . . . . . . . . . . 11  |-  ( ( C  =  D  /\  E  =  { C } )  ->  (
( E  =  { A }  /\  F  =  { A ,  B } )  ->  ( A  =  D  /\  F  =  { A ,  B } ) ) )
180172, 179orim12d 850 . . . . . . . . . 10  |-  ( ( C  =  D  /\  E  =  { C } )  ->  (
( ( E  =  { A ,  B }  /\  F  =  { A } )  \/  ( E  =  { A }  /\  F  =  { A ,  B }
) )  ->  (
( A  =  B  /\  F  =  { A ,  D }
)  \/  ( A  =  D  /\  F  =  { A ,  B } ) ) ) )
181180imp 431 . . . . . . . . 9  |-  ( ( ( C  =  D  /\  E  =  { C } )  /\  (
( E  =  { A ,  B }  /\  F  =  { A } )  \/  ( E  =  { A }  /\  F  =  { A ,  B }
) ) )  -> 
( ( A  =  B  /\  F  =  { A ,  D } )  \/  ( A  =  D  /\  F  =  { A ,  B } ) ) )
182148, 181jca 535 . . . . . . . 8  |-  ( ( ( 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 } ) ) ) )
183182ex 436 . . . . . . 7  |-  ( ( 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 } ) ) ) ) )
184183com12 32 . . . . . 6  |-  ( ( ( 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 } ) ) ) ) )
185184orcoms 391 . . . . 5  |-  ( ( ( 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 } ) ) ) ) )
186185imp 431 . . . 4  |-  ( ( ( ( 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 } ) ) ) )
187117, 186jaoi 381 . . 3  |-  ( ( ( ( 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 } ) ) ) )
18855, 187impbii 191 . 2  |-  ( ( ( 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 } ) ) ) )
18913, 18, 1883bitr4i 281 1  |-  ( {
<. A ,  B >. , 
<. C ,  D >. }  =  <. E ,  F >.  <-> 
( ( A  =  C  /\  E  =  { A } )  /\  ( ( A  =  B  /\  F  =  { A ,  D } )  \/  ( A  =  D  /\  F  =  { A ,  B } ) ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 188    \/ wo 370    /\ wa 371    = wceq 1446    e. wcel 1889   _Vcvv 3047   {csn 3970   {cpr 3972   <.cop 3976
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1671  ax-4 1684  ax-5 1760  ax-6 1807  ax-7 1853  ax-9 1898  ax-10 1917  ax-11 1922  ax-12 1935  ax-13 2093  ax-ext 2433  ax-sep 4528  ax-nul 4537  ax-pr 4642
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3an 988  df-tru 1449  df-ex 1666  df-nf 1670  df-sb 1800  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2583  df-ne 2626  df-v 3049  df-dif 3409  df-un 3411  df-in 3413  df-ss 3420  df-nul 3734  df-if 3884  df-sn 3971  df-pr 3973  df-op 3977
This theorem is referenced by:  propssopi  39010  fun2dmnopgexmpl  39038
  Copyright terms: Public domain W3C validator