Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  altopthsn Structured version   Unicode version

Theorem altopthsn 29816
Description: Two alternate ordered pairs are equal iff the singletons of their respective elements are equal. Note that this holds regardless of sethood of any of the elements. (Contributed by Scott Fenton, 16-Apr-2012.)
Assertion
Ref Expression
altopthsn  |-  ( << A ,  B >>  =  << C ,  D >>  <->  ( { A }  =  { C }  /\  { B }  =  { D } ) )

Proof of Theorem altopthsn
StepHypRef Expression
1 df-altop 29813 . . 3  |-  << A ,  B >>  =  { { A } ,  { A ,  { B } } }
2 df-altop 29813 . . 3  |-  << C ,  D >>  =  { { C } ,  { C ,  { D } } }
31, 2eqeq12i 2477 . 2  |-  ( << A ,  B >>  =  << C ,  D >>  <->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4 snex 4697 . . . . . 6  |-  { A }  e.  _V
5 prex 4698 . . . . . 6  |-  { A ,  { B } }  e.  _V
6 snex 4697 . . . . . 6  |-  { C }  e.  _V
7 prex 4698 . . . . . 6  |-  { C ,  { D } }  e.  _V
84, 5, 6, 7preq12b 4208 . . . . 5  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  <->  ( ( { A }  =  { C }  /\  { A ,  { B } }  =  { C ,  { D } } )  \/  ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } ) ) )
9 simpl 457 . . . . . 6  |-  ( ( { A }  =  { C }  /\  { A ,  { B } }  =  { C ,  { D } } )  ->  { A }  =  { C } )
10 snsspr1 4181 . . . . . . . . 9  |-  { A }  C_  { A ,  { B } }
11 sseq2 3521 . . . . . . . . 9  |-  ( { A ,  { B } }  =  { C }  ->  ( { A }  C_  { A ,  { B } }  <->  { A }  C_  { C } ) )
1210, 11mpbii 211 . . . . . . . 8  |-  ( { A ,  { B } }  =  { C }  ->  { A }  C_  { C }
)
1312adantl 466 . . . . . . 7  |-  ( ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } )  ->  { A }  C_ 
{ C } )
14 snsspr1 4181 . . . . . . . . 9  |-  { C }  C_  { C ,  { D } }
15 sseq2 3521 . . . . . . . . 9  |-  ( { A }  =  { C ,  { D } }  ->  ( { C }  C_  { A } 
<->  { C }  C_  { C ,  { D } } ) )
1614, 15mpbiri 233 . . . . . . . 8  |-  ( { A }  =  { C ,  { D } }  ->  { C }  C_  { A }
)
1716adantr 465 . . . . . . 7  |-  ( ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } )  ->  { C }  C_ 
{ A } )
1813, 17eqssd 3516 . . . . . 6  |-  ( ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } )  ->  { A }  =  { C } )
199, 18jaoi 379 . . . . 5  |-  ( ( ( { A }  =  { C }  /\  { A ,  { B } }  =  { C ,  { D } } )  \/  ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } ) )  ->  { A }  =  { C } )
208, 19sylbi 195 . . . 4  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { A }  =  { C } )
21 uneq1 3647 . . . . . . . . . 10  |-  ( { A }  =  { C }  ->  ( { A }  u.  { { B } } )  =  ( { C }  u.  { { B } } ) )
22 df-pr 4035 . . . . . . . . . 10  |-  { A ,  { B } }  =  ( { A }  u.  { { B } } )
23 df-pr 4035 . . . . . . . . . 10  |-  { C ,  { B } }  =  ( { C }  u.  { { B } } )
2421, 22, 233eqtr4g 2523 . . . . . . . . 9  |-  ( { A }  =  { C }  ->  { A ,  { B } }  =  { C ,  { B } } )
2524preq2d 4118 . . . . . . . 8  |-  ( { A }  =  { C }  ->  { { A } ,  { A ,  { B } } }  =  { { A } ,  { C ,  { B } } } )
26 preq1 4111 . . . . . . . 8  |-  ( { A }  =  { C }  ->  { { A } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { B } } } )
2725, 26eqtrd 2498 . . . . . . 7  |-  ( { A }  =  { C }  ->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { B } } } )
2827eqeq1d 2459 . . . . . 6  |-  ( { A }  =  { C }  ->  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  <->  { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } } ) )
2928biimpd 207 . . . . 5  |-  ( { A }  =  { C }  ->  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } } ) )
30 prex 4698 . . . . . . 7  |-  { C ,  { B } }  e.  _V
3130, 7preqr2 4207 . . . . . 6  |-  ( { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { C ,  { B } }  =  { C ,  { D } } )
32 snex 4697 . . . . . . 7  |-  { B }  e.  _V
33 snex 4697 . . . . . . 7  |-  { D }  e.  _V
3432, 33preqr2 4207 . . . . . 6  |-  ( { C ,  { B } }  =  { C ,  { D } }  ->  { B }  =  { D } )
3531, 34syl 16 . . . . 5  |-  ( { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { B }  =  { D } )
3629, 35syl6com 35 . . . 4  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  ( { A }  =  { C }  ->  { B }  =  { D } ) )
3720, 36jcai 536 . . 3  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  ( { A }  =  { C }  /\  { B }  =  { D } ) )
38 preq2 4112 . . . . 5  |-  ( { B }  =  { D }  ->  { C ,  { B } }  =  { C ,  { D } } )
3938preq2d 4118 . . . 4  |-  ( { B }  =  { D }  ->  { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4027, 39sylan9eq 2518 . . 3  |-  ( ( { A }  =  { C }  /\  { B }  =  { D } )  ->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4137, 40impbii 188 . 2  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  <->  ( { A }  =  { C }  /\  { B }  =  { D } ) )
423, 41bitri 249 1  |-  ( << A ,  B >>  =  << C ,  D >>  <->  ( { A }  =  { C }  /\  { B }  =  { D } ) )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    \/ wo 368    /\ wa 369    = wceq 1395    u. cun 3469    C_ wss 3471   {csn 4032   {cpr 4034   <<caltop 29811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1619  ax-4 1632  ax-5 1705  ax-6 1748  ax-7 1791  ax-9 1823  ax-10 1838  ax-11 1843  ax-12 1855  ax-13 2000  ax-ext 2435  ax-sep 4578  ax-nul 4586  ax-pr 4695
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1614  df-nf 1618  df-sb 1741  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-nul 3794  df-sn 4033  df-pr 4035  df-altop 29813
This theorem is referenced by:  altopeq12  29817  altopth1  29820  altopth2  29821  altopthg  29822  altopthbg  29823
  Copyright terms: Public domain W3C validator