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

Theorem altopthsn 29174
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 29171 . . 3  |-  << A ,  B >>  =  { { A } ,  { A ,  { B } } }
2 df-altop 29171 . . 3  |-  << C ,  D >>  =  { { C } ,  { C ,  { D } } }
31, 2eqeq12i 2480 . 2  |-  ( << A ,  B >>  =  << C ,  D >>  <->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4 snex 4681 . . . . . 6  |-  { A }  e.  _V
5 prex 4682 . . . . . 6  |-  { A ,  { B } }  e.  _V
6 snex 4681 . . . . . 6  |-  { C }  e.  _V
7 prex 4682 . . . . . 6  |-  { C ,  { D } }  e.  _V
84, 5, 6, 7preq12b 4195 . . . . 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 4169 . . . . . . . . 9  |-  { A }  C_  { A ,  { B } }
11 sseq2 3519 . . . . . . . . 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 4169 . . . . . . . . 9  |-  { C }  C_  { C ,  { D } }
15 sseq2 3519 . . . . . . . . 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 3514 . . . . . 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 3644 . . . . . . . . . 10  |-  ( { A }  =  { C }  ->  ( { A }  u.  { { B } } )  =  ( { C }  u.  { { B } } ) )
22 df-pr 4023 . . . . . . . . . 10  |-  { A ,  { B } }  =  ( { A }  u.  { { B } } )
23 df-pr 4023 . . . . . . . . . 10  |-  { C ,  { B } }  =  ( { C }  u.  { { B } } )
2421, 22, 233eqtr4g 2526 . . . . . . . . 9  |-  ( { A }  =  { C }  ->  { A ,  { B } }  =  { C ,  { B } } )
2524preq2d 4106 . . . . . . . 8  |-  ( { A }  =  { C }  ->  { { A } ,  { A ,  { B } } }  =  { { A } ,  { C ,  { B } } } )
26 preq1 4099 . . . . . . . 8  |-  ( { A }  =  { C }  ->  { { A } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { B } } } )
2725, 26eqtrd 2501 . . . . . . 7  |-  ( { A }  =  { C }  ->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { B } } } )
2827eqeq1d 2462 . . . . . 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 4682 . . . . . . 7  |-  { C ,  { B } }  e.  _V
3130, 7preqr2 4194 . . . . . 6  |-  ( { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { C ,  { B } }  =  { C ,  { D } } )
32 snex 4681 . . . . . . 7  |-  { B }  e.  _V
33 snex 4681 . . . . . . 7  |-  { D }  e.  _V
3432, 33preqr2 4194 . . . . . 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 4100 . . . . 5  |-  ( { B }  =  { D }  ->  { C ,  { B } }  =  { C ,  { D } } )
3938preq2d 4106 . . . 4  |-  ( { B }  =  { D }  ->  { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4027, 39sylan9eq 2521 . . 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 1374    u. cun 3467    C_ wss 3469   {csn 4020   {cpr 4022   <<caltop 29169
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438  ax-sep 4561  ax-nul 4569  ax-pr 4679
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-nfc 2610  df-ne 2657  df-v 3108  df-dif 3472  df-un 3474  df-in 3476  df-ss 3483  df-nul 3779  df-sn 4021  df-pr 4023  df-altop 29171
This theorem is referenced by:  altopeq12  29175  altopth1  29178  altopth2  29179  altopthg  29180  altopthbg  29181
  Copyright terms: Public domain W3C validator