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

Theorem altopthsn 24567
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 24564 . . 3  |-  << A ,  B >>  =  { { A } ,  { A ,  { B } } }
2 df-altop 24564 . . 3  |-  << C ,  D >>  =  { { C } ,  { C ,  { D } } }
31, 2eqeq12i 2309 . 2  |-  ( << A ,  B >>  =  << C ,  D >>  <->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4 snex 4232 . . . . . 6  |-  { A }  e.  _V
5 prex 4233 . . . . . 6  |-  { A ,  { B } }  e.  _V
6 snex 4232 . . . . . 6  |-  { C }  e.  _V
7 prex 4233 . . . . . 6  |-  { C ,  { D } }  e.  _V
84, 5, 6, 7preq12b 3804 . . . . 5  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  <->  ( ( { A }  =  { C }  /\  { A ,  { B } }  =  { C ,  { D } } )  \/  ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } ) ) )
9 simpl 443 . . . . . 6  |-  ( ( { A }  =  { C }  /\  { A ,  { B } }  =  { C ,  { D } } )  ->  { A }  =  { C } )
10 snsspr1 3780 . . . . . . . . 9  |-  { A }  C_  { A ,  { B } }
11 sseq2 3213 . . . . . . . . 9  |-  ( { A ,  { B } }  =  { C }  ->  ( { A }  C_  { A ,  { B } }  <->  { A }  C_  { C } ) )
1210, 11mpbii 202 . . . . . . . 8  |-  ( { A ,  { B } }  =  { C }  ->  { A }  C_  { C }
)
1312adantl 452 . . . . . . 7  |-  ( ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } )  ->  { A }  C_ 
{ C } )
14 snsspr1 3780 . . . . . . . . 9  |-  { C }  C_  { C ,  { D } }
15 sseq2 3213 . . . . . . . . 9  |-  ( { A }  =  { C ,  { D } }  ->  ( { C }  C_  { A } 
<->  { C }  C_  { C ,  { D } } ) )
1614, 15mpbiri 224 . . . . . . . 8  |-  ( { A }  =  { C ,  { D } }  ->  { C }  C_  { A }
)
1716adantr 451 . . . . . . 7  |-  ( ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } )  ->  { C }  C_ 
{ A } )
1813, 17eqssd 3209 . . . . . 6  |-  ( ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } )  ->  { A }  =  { C } )
199, 18jaoi 368 . . . . 5  |-  ( ( ( { A }  =  { C }  /\  { A ,  { B } }  =  { C ,  { D } } )  \/  ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } ) )  ->  { A }  =  { C } )
208, 19sylbi 187 . . . 4  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { A }  =  { C } )
21 uneq1 3335 . . . . . . . . . 10  |-  ( { A }  =  { C }  ->  ( { A }  u.  { { B } } )  =  ( { C }  u.  { { B } } ) )
22 df-pr 3660 . . . . . . . . . 10  |-  { A ,  { B } }  =  ( { A }  u.  { { B } } )
23 df-pr 3660 . . . . . . . . . 10  |-  { C ,  { B } }  =  ( { C }  u.  { { B } } )
2421, 22, 233eqtr4g 2353 . . . . . . . . 9  |-  ( { A }  =  { C }  ->  { A ,  { B } }  =  { C ,  { B } } )
2524preq2d 3726 . . . . . . . 8  |-  ( { A }  =  { C }  ->  { { A } ,  { A ,  { B } } }  =  { { A } ,  { C ,  { B } } } )
26 preq1 3719 . . . . . . . 8  |-  ( { A }  =  { C }  ->  { { A } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { B } } } )
2725, 26eqtrd 2328 . . . . . . 7  |-  ( { A }  =  { C }  ->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { B } } } )
2827eqeq1d 2304 . . . . . 6  |-  ( { A }  =  { C }  ->  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  <->  { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } } ) )
2928biimpd 198 . . . . 5  |-  ( { A }  =  { C }  ->  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } } ) )
30 prex 4233 . . . . . . 7  |-  { C ,  { B } }  e.  _V
3130, 7preqr2 3803 . . . . . 6  |-  ( { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { C ,  { B } }  =  { C ,  { D } } )
32 snex 4232 . . . . . . 7  |-  { B }  e.  _V
33 snex 4232 . . . . . . 7  |-  { D }  e.  _V
3432, 33preqr2 3803 . . . . . 6  |-  ( { C ,  { B } }  =  { C ,  { D } }  ->  { B }  =  { D } )
3531, 34syl 15 . . . . 5  |-  ( { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { B }  =  { D } )
3629, 35syl6com 31 . . . 4  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  ( { A }  =  { C }  ->  { B }  =  { D } ) )
3720, 36jcai 522 . . 3  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  ( { A }  =  { C }  /\  { B }  =  { D } ) )
38 preq2 3720 . . . . 5  |-  ( { B }  =  { D }  ->  { C ,  { B } }  =  { C ,  { D } } )
3938preq2d 3726 . . . 4  |-  ( { B }  =  { D }  ->  { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4027, 39sylan9eq 2348 . . 3  |-  ( ( { A }  =  { C }  /\  { B }  =  { D } )  ->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4137, 40impbii 180 . 2  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  <->  ( { A }  =  { C }  /\  { B }  =  { D } ) )
423, 41bitri 240 1  |-  ( << A ,  B >>  =  << C ,  D >>  <->  ( { A }  =  { C }  /\  { B }  =  { D } ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    \/ wo 357    /\ wa 358    = wceq 1632    u. cun 3163    C_ wss 3165   {csn 3653   {cpr 3654   <<caltop 24562
This theorem is referenced by:  altopeq12  24568  altopth1  24571  altopth2  24572  altopthg  24573  altopthbg  24574
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pr 4230
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-v 2803  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-nul 3469  df-sn 3659  df-pr 3660  df-altop 24564
  Copyright terms: Public domain W3C validator