Proof of Theorem flfnei
Step | Hyp | Ref
| Expression |
1 | | flfval 22734 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐽 fLimf 𝐿)‘𝐹) = (𝐽 fLim ((𝑋 FilMap 𝐹)‘𝐿))) |
2 | 1 | eleq2d 2818 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ 𝐴 ∈ (𝐽 fLim ((𝑋 FilMap 𝐹)‘𝐿)))) |
3 | | simp1 1137 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐽 ∈ (TopOn‘𝑋)) |
4 | | toponmax 21670 |
. . . . 5
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 ∈ 𝐽) |
5 | 4 | 3ad2ant1 1134 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 ∈ 𝐽) |
6 | | filfbas 22592 |
. . . . 5
⊢ (𝐿 ∈ (Fil‘𝑌) → 𝐿 ∈ (fBas‘𝑌)) |
7 | 6 | 3ad2ant2 1135 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐿 ∈ (fBas‘𝑌)) |
8 | | simp3 1139 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐹:𝑌⟶𝑋) |
9 | | fmfil 22688 |
. . . 4
⊢ ((𝑋 ∈ 𝐽 ∧ 𝐿 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐿) ∈ (Fil‘𝑋)) |
10 | 5, 7, 8, 9 | syl3anc 1372 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑋 FilMap 𝐹)‘𝐿) ∈ (Fil‘𝑋)) |
11 | | elflim 22715 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ ((𝑋 FilMap 𝐹)‘𝐿) ∈ (Fil‘𝑋)) → (𝐴 ∈ (𝐽 fLim ((𝑋 FilMap 𝐹)‘𝐿)) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ ((𝑋 FilMap 𝐹)‘𝐿)))) |
12 | 3, 10, 11 | syl2anc 587 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ (𝐽 fLim ((𝑋 FilMap 𝐹)‘𝐿)) ↔ (𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ ((𝑋 FilMap 𝐹)‘𝐿)))) |
13 | | dfss3 3863 |
. . . 4
⊢
(((nei‘𝐽)‘{𝐴}) ⊆ ((𝑋 FilMap 𝐹)‘𝐿) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})𝑛 ∈ ((𝑋 FilMap 𝐹)‘𝐿)) |
14 | | topontop 21657 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
15 | 14 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝐽 ∈ Top) |
16 | | eqid 2738 |
. . . . . . . . 9
⊢ ∪ 𝐽 =
∪ 𝐽 |
17 | 16 | neii1 21850 |
. . . . . . . 8
⊢ ((𝐽 ∈ Top ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑛 ⊆ ∪ 𝐽) |
18 | 15, 17 | sylan 583 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑛 ⊆ ∪ 𝐽) |
19 | | toponuni 21658 |
. . . . . . . . 9
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝑋 = ∪ 𝐽) |
20 | 19 | 3ad2ant1 1134 |
. . . . . . . 8
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → 𝑋 = ∪ 𝐽) |
21 | 20 | adantr 484 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑋 = ∪ 𝐽) |
22 | 18, 21 | sseqtrrd 3916 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → 𝑛 ⊆ 𝑋) |
23 | | elfm 22691 |
. . . . . . . 8
⊢ ((𝑋 ∈ 𝐽 ∧ 𝐿 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑛 ∈ ((𝑋 FilMap 𝐹)‘𝐿) ↔ (𝑛 ⊆ 𝑋 ∧ ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑛))) |
24 | 5, 7, 8, 23 | syl3anc 1372 |
. . . . . . 7
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑛 ∈ ((𝑋 FilMap 𝐹)‘𝐿) ↔ (𝑛 ⊆ 𝑋 ∧ ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑛))) |
25 | 24 | baibd 543 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑛 ⊆ 𝑋) → (𝑛 ∈ ((𝑋 FilMap 𝐹)‘𝐿) ↔ ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑛)) |
26 | 22, 25 | syldan 594 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑛 ∈ ((nei‘𝐽)‘{𝐴})) → (𝑛 ∈ ((𝑋 FilMap 𝐹)‘𝐿) ↔ ∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑛)) |
27 | 26 | ralbidva 3108 |
. . . 4
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})𝑛 ∈ ((𝑋 FilMap 𝐹)‘𝐿) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑛)) |
28 | 13, 27 | syl5bb 286 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (((nei‘𝐽)‘{𝐴}) ⊆ ((𝑋 FilMap 𝐹)‘𝐿) ↔ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑛)) |
29 | 28 | anbi2d 632 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐴 ∈ 𝑋 ∧ ((nei‘𝐽)‘{𝐴}) ⊆ ((𝑋 FilMap 𝐹)‘𝐿)) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑛))) |
30 | 2, 12, 29 | 3bitrd 308 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑛 ∈ ((nei‘𝐽)‘{𝐴})∃𝑠 ∈ 𝐿 (𝐹 “ 𝑠) ⊆ 𝑛))) |