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

Theorem altopthsn 25806
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 25803 . . 3  |-  << A ,  B >>  =  { { A } ,  { A ,  { B } } }
2 df-altop 25803 . . 3  |-  << C ,  D >>  =  { { C } ,  { C ,  { D } } }
31, 2eqeq12i 2449 . 2  |-  ( << A ,  B >>  =  << C ,  D >>  <->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4 snex 4405 . . . . . 6  |-  { A }  e.  _V
5 prex 4406 . . . . . 6  |-  { A ,  { B } }  e.  _V
6 snex 4405 . . . . . 6  |-  { C }  e.  _V
7 prex 4406 . . . . . 6  |-  { C ,  { D } }  e.  _V
84, 5, 6, 7preq12b 3974 . . . . 5  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  <->  ( ( { A }  =  { C }  /\  { A ,  { B } }  =  { C ,  { D } } )  \/  ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } ) ) )
9 simpl 444 . . . . . 6  |-  ( ( { A }  =  { C }  /\  { A ,  { B } }  =  { C ,  { D } } )  ->  { A }  =  { C } )
10 snsspr1 3947 . . . . . . . . 9  |-  { A }  C_  { A ,  { B } }
11 sseq2 3370 . . . . . . . . 9  |-  ( { A ,  { B } }  =  { C }  ->  ( { A }  C_  { A ,  { B } }  <->  { A }  C_  { C } ) )
1210, 11mpbii 203 . . . . . . . 8  |-  ( { A ,  { B } }  =  { C }  ->  { A }  C_  { C }
)
1312adantl 453 . . . . . . 7  |-  ( ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } )  ->  { A }  C_ 
{ C } )
14 snsspr1 3947 . . . . . . . . 9  |-  { C }  C_  { C ,  { D } }
15 sseq2 3370 . . . . . . . . 9  |-  ( { A }  =  { C ,  { D } }  ->  ( { C }  C_  { A } 
<->  { C }  C_  { C ,  { D } } ) )
1614, 15mpbiri 225 . . . . . . . 8  |-  ( { A }  =  { C ,  { D } }  ->  { C }  C_  { A }
)
1716adantr 452 . . . . . . 7  |-  ( ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } )  ->  { C }  C_ 
{ A } )
1813, 17eqssd 3365 . . . . . 6  |-  ( ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } )  ->  { A }  =  { C } )
199, 18jaoi 369 . . . . 5  |-  ( ( ( { A }  =  { C }  /\  { A ,  { B } }  =  { C ,  { D } } )  \/  ( { A }  =  { C ,  { D } }  /\  { A ,  { B } }  =  { C } ) )  ->  { A }  =  { C } )
208, 19sylbi 188 . . . 4  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { A }  =  { C } )
21 uneq1 3494 . . . . . . . . . 10  |-  ( { A }  =  { C }  ->  ( { A }  u.  { { B } } )  =  ( { C }  u.  { { B } } ) )
22 df-pr 3821 . . . . . . . . . 10  |-  { A ,  { B } }  =  ( { A }  u.  { { B } } )
23 df-pr 3821 . . . . . . . . . 10  |-  { C ,  { B } }  =  ( { C }  u.  { { B } } )
2421, 22, 233eqtr4g 2493 . . . . . . . . 9  |-  ( { A }  =  { C }  ->  { A ,  { B } }  =  { C ,  { B } } )
2524preq2d 3890 . . . . . . . 8  |-  ( { A }  =  { C }  ->  { { A } ,  { A ,  { B } } }  =  { { A } ,  { C ,  { B } } } )
26 preq1 3883 . . . . . . . 8  |-  ( { A }  =  { C }  ->  { { A } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { B } } } )
2725, 26eqtrd 2468 . . . . . . 7  |-  ( { A }  =  { C }  ->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { B } } } )
2827eqeq1d 2444 . . . . . 6  |-  ( { A }  =  { C }  ->  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  <->  { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } } ) )
2928biimpd 199 . . . . 5  |-  ( { A }  =  { C }  ->  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } } ) )
30 prex 4406 . . . . . . 7  |-  { C ,  { B } }  e.  _V
3130, 7preqr2 3973 . . . . . 6  |-  ( { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { C ,  { B } }  =  { C ,  { D } } )
32 snex 4405 . . . . . . 7  |-  { B }  e.  _V
33 snex 4405 . . . . . . 7  |-  { D }  e.  _V
3432, 33preqr2 3973 . . . . . 6  |-  ( { C ,  { B } }  =  { C ,  { D } }  ->  { B }  =  { D } )
3531, 34syl 16 . . . . 5  |-  ( { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { B }  =  { D } )
3629, 35syl6com 33 . . . 4  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  ( { A }  =  { C }  ->  { B }  =  { D } ) )
3720, 36jcai 523 . . 3  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  ( { A }  =  { C }  /\  { B }  =  { D } ) )
38 preq2 3884 . . . . 5  |-  ( { B }  =  { D }  ->  { C ,  { B } }  =  { C ,  { D } } )
3938preq2d 3890 . . . 4  |-  ( { B }  =  { D }  ->  { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4027, 39sylan9eq 2488 . . 3  |-  ( ( { A }  =  { C }  /\  { B }  =  { D } )  ->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4137, 40impbii 181 . 2  |-  ( { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } }  <->  ( { A }  =  { C }  /\  { B }  =  { D } ) )
423, 41bitri 241 1  |-  ( << A ,  B >>  =  << C ,  D >>  <->  ( { A }  =  { C }  /\  { B }  =  { D } ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    \/ wo 358    /\ wa 359    = wceq 1652    u. cun 3318    C_ wss 3320   {csn 3814   {cpr 3815   <<caltop 25801
This theorem is referenced by:  altopeq12  25807  altopth1  25810  altopth2  25811  altopthg  25812  altopthbg  25813
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417  ax-sep 4330  ax-nul 4338  ax-pr 4403
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ne 2601  df-v 2958  df-dif 3323  df-un 3325  df-in 3327  df-ss 3334  df-nul 3629  df-sn 3820  df-pr 3821  df-altop 25803
  Copyright terms: Public domain W3C validator