Step |
Hyp |
Ref |
Expression |
1 |
|
simplll |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
2 |
|
simprl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → 𝑓 ∈ ( Fil ‘ 𝑋 ) ) |
3 |
|
simplr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → 𝐽 ⊆ 𝐾 ) |
4 |
|
flimss1 |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝐽 ⊆ 𝐾 ) → ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) |
5 |
1 2 3 4
|
syl3anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) |
6 |
|
simprr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) |
7 |
5 6
|
sseldd |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) ∧ ( 𝑓 ∈ ( Fil ‘ 𝑋 ) ∧ 𝑥 ∈ ( 𝐾 fLim 𝑓 ) ) ) → 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) |
8 |
7
|
expr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝑥 ∈ ( 𝐾 fLim 𝑓 ) → 𝑥 ∈ ( 𝐽 fLim 𝑓 ) ) ) |
9 |
8
|
ssrdv |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) ∧ 𝑓 ∈ ( Fil ‘ 𝑋 ) ) → ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) |
10 |
9
|
ralrimiva |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ 𝐽 ⊆ 𝐾 ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) |
11 |
|
oveq2 |
⊢ ( 𝑓 = ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) → ( 𝐾 fLim 𝑓 ) = ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ) |
12 |
|
oveq2 |
⊢ ( 𝑓 = ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) → ( 𝐽 fLim 𝑓 ) = ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ) |
13 |
11 12
|
sseq12d |
⊢ ( 𝑓 = ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) → ( ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ↔ ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ⊆ ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ) ) |
14 |
|
simplr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) |
15 |
|
simpllr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) |
16 |
|
simplll |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) ) |
17 |
|
simprl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ∈ 𝐽 ) |
18 |
|
toponss |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ⊆ 𝑋 ) |
19 |
16 17 18
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ⊆ 𝑋 ) |
20 |
|
simprr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ 𝑥 ) |
21 |
19 20
|
sseldd |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ 𝑋 ) |
22 |
21
|
snssd |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → { 𝑦 } ⊆ 𝑋 ) |
23 |
20
|
snn0d |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → { 𝑦 } ≠ ∅ ) |
24 |
|
neifil |
⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ { 𝑦 } ⊆ 𝑋 ∧ { 𝑦 } ≠ ∅ ) → ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ∈ ( Fil ‘ 𝑋 ) ) |
25 |
15 22 23 24
|
syl3anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ∈ ( Fil ‘ 𝑋 ) ) |
26 |
13 14 25
|
rspcdva |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ⊆ ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ) |
27 |
|
neiflim |
⊢ ( ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑦 ∈ 𝑋 ) → 𝑦 ∈ ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ) |
28 |
15 21 27
|
syl2anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ ( 𝐾 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ) |
29 |
26 28
|
sseldd |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑦 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ) |
30 |
|
flimneiss |
⊢ ( 𝑦 ∈ ( 𝐽 fLim ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ⊆ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) |
31 |
29 30
|
syl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ⊆ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) |
32 |
|
topontop |
⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top ) |
33 |
16 32
|
syl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝐽 ∈ Top ) |
34 |
|
opnneip |
⊢ ( ( 𝐽 ∈ Top ∧ 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) |
35 |
33 17 20 34
|
syl3anc |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐽 ) ‘ { 𝑦 } ) ) |
36 |
31 35
|
sseldd |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ ( 𝑥 ∈ 𝐽 ∧ 𝑦 ∈ 𝑥 ) ) → 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) |
37 |
36
|
anassrs |
⊢ ( ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) |
38 |
37
|
ralrimiva |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → ∀ 𝑦 ∈ 𝑥 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) |
39 |
|
simpllr |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) |
40 |
|
topontop |
⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑋 ) → 𝐾 ∈ Top ) |
41 |
|
opnnei |
⊢ ( 𝐾 ∈ Top → ( 𝑥 ∈ 𝐾 ↔ ∀ 𝑦 ∈ 𝑥 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ) |
42 |
39 40 41
|
3syl |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → ( 𝑥 ∈ 𝐾 ↔ ∀ 𝑦 ∈ 𝑥 𝑥 ∈ ( ( nei ‘ 𝐾 ) ‘ { 𝑦 } ) ) ) |
43 |
38 42
|
mpbird |
⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐾 ) |
44 |
43
|
ex |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) → ( 𝑥 ∈ 𝐽 → 𝑥 ∈ 𝐾 ) ) |
45 |
44
|
ssrdv |
⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) ∧ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) → 𝐽 ⊆ 𝐾 ) |
46 |
10 45
|
impbida |
⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑋 ) ) → ( 𝐽 ⊆ 𝐾 ↔ ∀ 𝑓 ∈ ( Fil ‘ 𝑋 ) ( 𝐾 fLim 𝑓 ) ⊆ ( 𝐽 fLim 𝑓 ) ) ) |