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

Theorem altopthsn 25771
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 25768 . . 3  |-  << A ,  B >>  =  { { A } ,  { A ,  { B } } }
2 df-altop 25768 . . 3  |-  << C ,  D >>  =  { { C } ,  { C ,  { D } } }
31, 2eqeq12i 2448 . 2  |-  ( << A ,  B >>  =  << C ,  D >>  <->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4 snex 4397 . . . . . 6  |-  { A }  e.  _V
5 prex 4398 . . . . . 6  |-  { A ,  { B } }  e.  _V
6 snex 4397 . . . . . 6  |-  { C }  e.  _V
7 prex 4398 . . . . . 6  |-  { C ,  { D } }  e.  _V
84, 5, 6, 7preq12b 3966 . . . . 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 3939 . . . . . . . . 9  |-  { A }  C_  { A ,  { B } }
11 sseq2 3362 . . . . . . . . 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 3939 . . . . . . . . 9  |-  { C }  C_  { C ,  { D } }
15 sseq2 3362 . . . . . . . . 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 3357 . . . . . 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 3486 . . . . . . . . . 10  |-  ( { A }  =  { C }  ->  ( { A }  u.  { { B } } )  =  ( { C }  u.  { { B } } ) )
22 df-pr 3813 . . . . . . . . . 10  |-  { A ,  { B } }  =  ( { A }  u.  { { B } } )
23 df-pr 3813 . . . . . . . . . 10  |-  { C ,  { B } }  =  ( { C }  u.  { { B } } )
2421, 22, 233eqtr4g 2492 . . . . . . . . 9  |-  ( { A }  =  { C }  ->  { A ,  { B } }  =  { C ,  { B } } )
2524preq2d 3882 . . . . . . . 8  |-  ( { A }  =  { C }  ->  { { A } ,  { A ,  { B } } }  =  { { A } ,  { C ,  { B } } } )
26 preq1 3875 . . . . . . . 8  |-  ( { A }  =  { C }  ->  { { A } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { B } } } )
2725, 26eqtrd 2467 . . . . . . 7  |-  ( { A }  =  { C }  ->  { { A } ,  { A ,  { B } } }  =  { { C } ,  { C ,  { B } } } )
2827eqeq1d 2443 . . . . . 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 4398 . . . . . . 7  |-  { C ,  { B } }  e.  _V
3130, 7preqr2 3965 . . . . . 6  |-  ( { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } }  ->  { C ,  { B } }  =  { C ,  { D } } )
32 snex 4397 . . . . . . 7  |-  { B }  e.  _V
33 snex 4397 . . . . . . 7  |-  { D }  e.  _V
3432, 33preqr2 3965 . . . . . 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 3876 . . . . 5  |-  ( { B }  =  { D }  ->  { C ,  { B } }  =  { C ,  { D } } )
3938preq2d 3882 . . . 4  |-  ( { B }  =  { D }  ->  { { C } ,  { C ,  { B } } }  =  { { C } ,  { C ,  { D } } } )
4027, 39sylan9eq 2487 . . 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 3310    C_ wss 3312   {csn 3806   {cpr 3807   <<caltop 25766
This theorem is referenced by:  altopeq12  25772  altopth1  25775  altopth2  25776  altopthg  25777  altopthbg  25778
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 2416  ax-sep 4322  ax-nul 4330  ax-pr 4395
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-v 2950  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-sn 3812  df-pr 3813  df-altop 25768
  Copyright terms: Public domain W3C validator