Step |
Hyp |
Ref |
Expression |
1 |
|
simpr |
|- ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> J ~~ 2o ) |
2 |
|
toponss |
|- ( ( J e. ( TopOn ` X ) /\ x e. J ) -> x C_ X ) |
3 |
2
|
ad2ant2rl |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ ( X = (/) /\ x e. J ) ) -> x C_ X ) |
4 |
|
simprl |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ ( X = (/) /\ x e. J ) ) -> X = (/) ) |
5 |
|
sseq0 |
|- ( ( x C_ X /\ X = (/) ) -> x = (/) ) |
6 |
3 4 5
|
syl2anc |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ ( X = (/) /\ x e. J ) ) -> x = (/) ) |
7 |
|
velsn |
|- ( x e. { (/) } <-> x = (/) ) |
8 |
6 7
|
sylibr |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ ( X = (/) /\ x e. J ) ) -> x e. { (/) } ) |
9 |
8
|
expr |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> ( x e. J -> x e. { (/) } ) ) |
10 |
9
|
ssrdv |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> J C_ { (/) } ) |
11 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
12 |
|
0opn |
|- ( J e. Top -> (/) e. J ) |
13 |
11 12
|
syl |
|- ( J e. ( TopOn ` X ) -> (/) e. J ) |
14 |
13
|
ad2antrr |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> (/) e. J ) |
15 |
14
|
snssd |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> { (/) } C_ J ) |
16 |
10 15
|
eqssd |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> J = { (/) } ) |
17 |
|
0ex |
|- (/) e. _V |
18 |
17
|
ensn1 |
|- { (/) } ~~ 1o |
19 |
16 18
|
eqbrtrdi |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> J ~~ 1o ) |
20 |
19
|
olcd |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> ( J = (/) \/ J ~~ 1o ) ) |
21 |
|
sdom2en01 |
|- ( J ~< 2o <-> ( J = (/) \/ J ~~ 1o ) ) |
22 |
20 21
|
sylibr |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> J ~< 2o ) |
23 |
|
sdomnen |
|- ( J ~< 2o -> -. J ~~ 2o ) |
24 |
22 23
|
syl |
|- ( ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) /\ X = (/) ) -> -. J ~~ 2o ) |
25 |
24
|
ex |
|- ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> ( X = (/) -> -. J ~~ 2o ) ) |
26 |
25
|
necon2ad |
|- ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> ( J ~~ 2o -> X =/= (/) ) ) |
27 |
1 26
|
mpd |
|- ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> X =/= (/) ) |
28 |
27
|
necomd |
|- ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> (/) =/= X ) |
29 |
13
|
adantr |
|- ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> (/) e. J ) |
30 |
|
toponmax |
|- ( J e. ( TopOn ` X ) -> X e. J ) |
31 |
30
|
adantr |
|- ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> X e. J ) |
32 |
|
en2eqpr |
|- ( ( J ~~ 2o /\ (/) e. J /\ X e. J ) -> ( (/) =/= X -> J = { (/) , X } ) ) |
33 |
1 29 31 32
|
syl3anc |
|- ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> ( (/) =/= X -> J = { (/) , X } ) ) |
34 |
28 33
|
mpd |
|- ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> J = { (/) , X } ) |
35 |
34 27
|
jca |
|- ( ( J e. ( TopOn ` X ) /\ J ~~ 2o ) -> ( J = { (/) , X } /\ X =/= (/) ) ) |
36 |
|
simprl |
|- ( ( J e. ( TopOn ` X ) /\ ( J = { (/) , X } /\ X =/= (/) ) ) -> J = { (/) , X } ) |
37 |
|
simprr |
|- ( ( J e. ( TopOn ` X ) /\ ( J = { (/) , X } /\ X =/= (/) ) ) -> X =/= (/) ) |
38 |
37
|
necomd |
|- ( ( J e. ( TopOn ` X ) /\ ( J = { (/) , X } /\ X =/= (/) ) ) -> (/) =/= X ) |
39 |
|
pr2nelem |
|- ( ( (/) e. _V /\ X e. J /\ (/) =/= X ) -> { (/) , X } ~~ 2o ) |
40 |
17 30 38 39
|
mp3an2ani |
|- ( ( J e. ( TopOn ` X ) /\ ( J = { (/) , X } /\ X =/= (/) ) ) -> { (/) , X } ~~ 2o ) |
41 |
36 40
|
eqbrtrd |
|- ( ( J e. ( TopOn ` X ) /\ ( J = { (/) , X } /\ X =/= (/) ) ) -> J ~~ 2o ) |
42 |
35 41
|
impbida |
|- ( J e. ( TopOn ` X ) -> ( J ~~ 2o <-> ( J = { (/) , X } /\ X =/= (/) ) ) ) |