MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  en2top Unicode version

Theorem en2top 16723
Description: If a topology has two elements it is the indiscrete topology. (Contributed by FL, 11-Aug-2008.) (Revised by Mario Carneiro, 10-Sep-2015.)
Assertion
Ref Expression
en2top  |-  ( J  e.  (TopOn `  X
)  ->  ( J  ~~  2o  <->  ( J  =  { (/) ,  X }  /\  X  =/=  (/) ) ) )

Proof of Theorem en2top
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 simpr 447 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  ->  J  ~~  2o )
2 toponss 16667 . . . . . . . . . . . . . . . . . 18  |-  ( ( J  e.  (TopOn `  X )  /\  x  e.  J )  ->  x  C_  X )
32ad2ant2rl 729 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  ( X  =  (/)  /\  x  e.  J ) )  ->  x  C_  X )
4 simprl 732 . . . . . . . . . . . . . . . . 17  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  ( X  =  (/)  /\  x  e.  J ) )  ->  X  =  (/) )
5 sseq0 3486 . . . . . . . . . . . . . . . . 17  |-  ( ( x  C_  X  /\  X  =  (/) )  ->  x  =  (/) )
63, 4, 5syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  ( X  =  (/)  /\  x  e.  J ) )  ->  x  =  (/) )
7 elsn 3655 . . . . . . . . . . . . . . . 16  |-  ( x  e.  { (/) }  <->  x  =  (/) )
86, 7sylibr 203 . . . . . . . . . . . . . . 15  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  ( X  =  (/)  /\  x  e.  J ) )  ->  x  e.  { (/) } )
98expr 598 . . . . . . . . . . . . . 14  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  X  =  (/) )  ->  (
x  e.  J  ->  x  e.  { (/) } ) )
109ssrdv 3185 . . . . . . . . . . . . 13  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  X  =  (/) )  ->  J  C_ 
{ (/) } )
11 topontop 16664 . . . . . . . . . . . . . . . 16  |-  ( J  e.  (TopOn `  X
)  ->  J  e.  Top )
12 0opn 16650 . . . . . . . . . . . . . . . 16  |-  ( J  e.  Top  ->  (/)  e.  J
)
1311, 12syl 15 . . . . . . . . . . . . . . 15  |-  ( J  e.  (TopOn `  X
)  ->  (/)  e.  J
)
1413ad2antrr 706 . . . . . . . . . . . . . 14  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  X  =  (/) )  ->  (/)  e.  J
)
1514snssd 3760 . . . . . . . . . . . . 13  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  X  =  (/) )  ->  { (/) } 
C_  J )
1610, 15eqssd 3196 . . . . . . . . . . . 12  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  X  =  (/) )  ->  J  =  { (/) } )
17 0ex 4150 . . . . . . . . . . . . 13  |-  (/)  e.  _V
1817ensn1 6925 . . . . . . . . . . . 12  |-  { (/) } 
~~  1o
1916, 18syl6eqbr 4060 . . . . . . . . . . 11  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  X  =  (/) )  ->  J  ~~  1o )
2019olcd 382 . . . . . . . . . 10  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  X  =  (/) )  ->  ( J  =  (/)  \/  J  ~~  1o ) )
21 sdom2en01 7928 . . . . . . . . . 10  |-  ( J 
~<  2o  <->  ( J  =  (/)  \/  J  ~~  1o ) )
2220, 21sylibr 203 . . . . . . . . 9  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  X  =  (/) )  ->  J  ~<  2o )
23 sdomnen 6890 . . . . . . . . 9  |-  ( J 
~<  2o  ->  -.  J  ~~  2o )
2422, 23syl 15 . . . . . . . 8  |-  ( ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  /\  X  =  (/) )  ->  -.  J  ~~  2o )
2524ex 423 . . . . . . 7  |-  ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  ->  ( X  =  (/)  ->  -.  J  ~~  2o ) )
2625necon2ad 2494 . . . . . 6  |-  ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  ->  ( J  ~~  2o  ->  X  =/=  (/) ) )
271, 26mpd 14 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  ->  X  =/=  (/) )
2827necomd 2529 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  ->  (/)  =/=  X
)
2913adantr 451 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  ->  (/)  e.  J
)
30 toponmax 16666 . . . . . 6  |-  ( J  e.  (TopOn `  X
)  ->  X  e.  J )
3130adantr 451 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  ->  X  e.  J )
32 en2eqpr 7637 . . . . 5  |-  ( ( J  ~~  2o  /\  (/) 
e.  J  /\  X  e.  J )  ->  ( (/) 
=/=  X  ->  J  =  { (/) ,  X }
) )
331, 29, 31, 32syl3anc 1182 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  ->  ( (/) 
=/=  X  ->  J  =  { (/) ,  X }
) )
3428, 33mpd 14 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  ->  J  =  { (/) ,  X }
)
3534, 27jca 518 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  J  ~~  2o )  ->  ( J  =  { (/) ,  X }  /\  X  =/=  (/) ) )
36 simprl 732 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  ( J  =  { (/) ,  X }  /\  X  =/=  (/) ) )  ->  J  =  { (/)
,  X } )
3717a1i 10 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  ( J  =  { (/) ,  X }  /\  X  =/=  (/) ) )  ->  (/)  e.  _V )
3830adantr 451 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  ( J  =  { (/) ,  X }  /\  X  =/=  (/) ) )  ->  X  e.  J
)
39 simprr 733 . . . . 5  |-  ( ( J  e.  (TopOn `  X )  /\  ( J  =  { (/) ,  X }  /\  X  =/=  (/) ) )  ->  X  =/=  (/) )
4039necomd 2529 . . . 4  |-  ( ( J  e.  (TopOn `  X )  /\  ( J  =  { (/) ,  X }  /\  X  =/=  (/) ) )  ->  (/)  =/=  X )
41 pr2nelem 7634 . . . 4  |-  ( (
(/)  e.  _V  /\  X  e.  J  /\  (/)  =/=  X
)  ->  { (/) ,  X }  ~~  2o )
4237, 38, 40, 41syl3anc 1182 . . 3  |-  ( ( J  e.  (TopOn `  X )  /\  ( J  =  { (/) ,  X }  /\  X  =/=  (/) ) )  ->  { (/) ,  X }  ~~  2o )
4336, 42eqbrtrd 4043 . 2  |-  ( ( J  e.  (TopOn `  X )  /\  ( J  =  { (/) ,  X }  /\  X  =/=  (/) ) )  ->  J  ~~  2o )
4435, 43impbida 805 1  |-  ( J  e.  (TopOn `  X
)  ->  ( J  ~~  2o  <->  ( J  =  { (/) ,  X }  /\  X  =/=  (/) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    \/ wo 357    /\ wa 358    = wceq 1623    e. wcel 1684    =/= wne 2446   _Vcvv 2788    C_ wss 3152   (/)c0 3455   {csn 3640   {cpr 3641   class class class wbr 4023   ` cfv 5255   1oc1o 6472   2oc2o 6473    ~~ cen 6860    ~< csdm 6862   Topctop 16631  TopOnctopon 16632
This theorem is referenced by:  hmphindis  17488
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-int 3863  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-1o 6479  df-2o 6480  df-er 6660  df-en 6864  df-dom 6865  df-sdom 6866  df-fin 6867  df-card 7572  df-top 16636  df-topon 16639
  Copyright terms: Public domain W3C validator