Step |
Hyp |
Ref |
Expression |
1 |
|
simplll |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> J e. ( TopOn ` X ) ) |
2 |
|
simprl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> f e. ( Fil ` X ) ) |
3 |
|
simplr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> J C_ K ) |
4 |
|
flimss1 |
|- ( ( J e. ( TopOn ` X ) /\ f e. ( Fil ` X ) /\ J C_ K ) -> ( K fLim f ) C_ ( J fLim f ) ) |
5 |
1 2 3 4
|
syl3anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> ( K fLim f ) C_ ( J fLim f ) ) |
6 |
|
simprr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> x e. ( K fLim f ) ) |
7 |
5 6
|
sseldd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ ( f e. ( Fil ` X ) /\ x e. ( K fLim f ) ) ) -> x e. ( J fLim f ) ) |
8 |
7
|
expr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ f e. ( Fil ` X ) ) -> ( x e. ( K fLim f ) -> x e. ( J fLim f ) ) ) |
9 |
8
|
ssrdv |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) /\ f e. ( Fil ` X ) ) -> ( K fLim f ) C_ ( J fLim f ) ) |
10 |
9
|
ralrimiva |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ J C_ K ) -> A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) |
11 |
|
oveq2 |
|- ( f = ( ( nei ` K ) ` { y } ) -> ( K fLim f ) = ( K fLim ( ( nei ` K ) ` { y } ) ) ) |
12 |
|
oveq2 |
|- ( f = ( ( nei ` K ) ` { y } ) -> ( J fLim f ) = ( J fLim ( ( nei ` K ) ` { y } ) ) ) |
13 |
11 12
|
sseq12d |
|- ( f = ( ( nei ` K ) ` { y } ) -> ( ( K fLim f ) C_ ( J fLim f ) <-> ( K fLim ( ( nei ` K ) ` { y } ) ) C_ ( J fLim ( ( nei ` K ) ` { y } ) ) ) ) |
14 |
|
simplr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) |
15 |
|
simpllr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> K e. ( TopOn ` X ) ) |
16 |
|
simplll |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> J e. ( TopOn ` X ) ) |
17 |
|
simprl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> x e. J ) |
18 |
|
toponss |
|- ( ( J e. ( TopOn ` X ) /\ x e. J ) -> x C_ X ) |
19 |
16 17 18
|
syl2anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> x C_ X ) |
20 |
|
simprr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> y e. x ) |
21 |
19 20
|
sseldd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> y e. X ) |
22 |
21
|
snssd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> { y } C_ X ) |
23 |
20
|
snn0d |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> { y } =/= (/) ) |
24 |
|
neifil |
|- ( ( K e. ( TopOn ` X ) /\ { y } C_ X /\ { y } =/= (/) ) -> ( ( nei ` K ) ` { y } ) e. ( Fil ` X ) ) |
25 |
15 22 23 24
|
syl3anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> ( ( nei ` K ) ` { y } ) e. ( Fil ` X ) ) |
26 |
13 14 25
|
rspcdva |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> ( K fLim ( ( nei ` K ) ` { y } ) ) C_ ( J fLim ( ( nei ` K ) ` { y } ) ) ) |
27 |
|
neiflim |
|- ( ( K e. ( TopOn ` X ) /\ y e. X ) -> y e. ( K fLim ( ( nei ` K ) ` { y } ) ) ) |
28 |
15 21 27
|
syl2anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> y e. ( K fLim ( ( nei ` K ) ` { y } ) ) ) |
29 |
26 28
|
sseldd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> y e. ( J fLim ( ( nei ` K ) ` { y } ) ) ) |
30 |
|
flimneiss |
|- ( y e. ( J fLim ( ( nei ` K ) ` { y } ) ) -> ( ( nei ` J ) ` { y } ) C_ ( ( nei ` K ) ` { y } ) ) |
31 |
29 30
|
syl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> ( ( nei ` J ) ` { y } ) C_ ( ( nei ` K ) ` { y } ) ) |
32 |
|
topontop |
|- ( J e. ( TopOn ` X ) -> J e. Top ) |
33 |
16 32
|
syl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> J e. Top ) |
34 |
|
opnneip |
|- ( ( J e. Top /\ x e. J /\ y e. x ) -> x e. ( ( nei ` J ) ` { y } ) ) |
35 |
33 17 20 34
|
syl3anc |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> x e. ( ( nei ` J ) ` { y } ) ) |
36 |
31 35
|
sseldd |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ ( x e. J /\ y e. x ) ) -> x e. ( ( nei ` K ) ` { y } ) ) |
37 |
36
|
anassrs |
|- ( ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ x e. J ) /\ y e. x ) -> x e. ( ( nei ` K ) ` { y } ) ) |
38 |
37
|
ralrimiva |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ x e. J ) -> A. y e. x x e. ( ( nei ` K ) ` { y } ) ) |
39 |
|
simpllr |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ x e. J ) -> K e. ( TopOn ` X ) ) |
40 |
|
topontop |
|- ( K e. ( TopOn ` X ) -> K e. Top ) |
41 |
|
opnnei |
|- ( K e. Top -> ( x e. K <-> A. y e. x x e. ( ( nei ` K ) ` { y } ) ) ) |
42 |
39 40 41
|
3syl |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ x e. J ) -> ( x e. K <-> A. y e. x x e. ( ( nei ` K ) ` { y } ) ) ) |
43 |
38 42
|
mpbird |
|- ( ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) /\ x e. J ) -> x e. K ) |
44 |
43
|
ex |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) -> ( x e. J -> x e. K ) ) |
45 |
44
|
ssrdv |
|- ( ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) /\ A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) -> J C_ K ) |
46 |
10 45
|
impbida |
|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` X ) ) -> ( J C_ K <-> A. f e. ( Fil ` X ) ( K fLim f ) C_ ( J fLim f ) ) ) |