Users' Mathboxes Mathbox for Chen-Pang He < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ssoninhaus Unicode version

Theorem ssoninhaus 26110
Description: The ordinal topologies  1o and  2o are Hausdorff. (Contributed by Chen-Pang He, 10-Nov-2015.)
Assertion
Ref Expression
ssoninhaus  |-  { 1o ,  2o }  C_  ( On  i^i  Haus )

Proof of Theorem ssoninhaus
StepHypRef Expression
1 1on 6698 . . 3  |-  1o  e.  On
2 2on 6699 . . 3  |-  2o  e.  On
3 prssi 3922 . . 3  |-  ( ( 1o  e.  On  /\  2o  e.  On )  ->  { 1o ,  2o }  C_  On )
41, 2, 3mp2an 654 . 2  |-  { 1o ,  2o }  C_  On
5 df1o2 6703 . . . . 5  |-  1o  =  { (/) }
6 pw0 3913 . . . . 5  |-  ~P (/)  =  { (/)
}
75, 6eqtr4i 2435 . . . 4  |-  1o  =  ~P (/)
8 0ex 4307 . . . . 5  |-  (/)  e.  _V
9 dishaus 17408 . . . . 5  |-  ( (/)  e.  _V  ->  ~P (/)  e.  Haus )
108, 9ax-mp 8 . . . 4  |-  ~P (/)  e.  Haus
117, 10eqeltri 2482 . . 3  |-  1o  e.  Haus
12 df2o2 6705 . . . . 5  |-  2o  =  { (/) ,  { (/) } }
13 pwpw0 3914 . . . . 5  |-  ~P { (/)
}  =  { (/) ,  { (/) } }
1412, 13eqtr4i 2435 . . . 4  |-  2o  =  ~P { (/) }
15 p0ex 4354 . . . . 5  |-  { (/) }  e.  _V
16 dishaus 17408 . . . . 5  |-  ( {
(/) }  e.  _V  ->  ~P { (/) }  e.  Haus )
1715, 16ax-mp 8 . . . 4  |-  ~P { (/)
}  e.  Haus
1814, 17eqeltri 2482 . . 3  |-  2o  e.  Haus
19 prssi 3922 . . 3  |-  ( ( 1o  e.  Haus  /\  2o  e.  Haus )  ->  { 1o ,  2o }  C_  Haus )
2011, 18, 19mp2an 654 . 2  |-  { 1o ,  2o }  C_  Haus
214, 20ssini 3532 1  |-  { 1o ,  2o }  C_  ( On  i^i  Haus )
Colors of variables: wff set class
Syntax hints:    e. wcel 1721   _Vcvv 2924    i^i cin 3287    C_ wss 3288   (/)c0 3596   ~Pcpw 3767   {csn 3782   {cpr 3783   Oncon0 4549   1oc1o 6684   2oc2o 6685   Hauscha 17334
This theorem is referenced by:  onint1  26111  oninhaus  26112
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-rab 2683  df-v 2926  df-sbc 3130  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-br 4181  df-opab 4235  df-tr 4271  df-eprel 4462  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-suc 4555  df-1o 6691  df-2o 6692  df-top 16926  df-haus 17341
  Copyright terms: Public domain W3C validator