Step | Hyp | Ref
| Expression |
1 | | flffbas.l |
. . . 4
⊢ 𝐿 = (𝑌filGen𝐵) |
2 | | fgcl 21492 |
. . . 4
⊢ (𝐵 ∈ (fBas‘𝑌) → (𝑌filGen𝐵) ∈ (Fil‘𝑌)) |
3 | 1, 2 | syl5eqel 2692 |
. . 3
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐿 ∈ (Fil‘𝑌)) |
4 | | isflf 21607 |
. . 3
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐿 ∈ (Fil‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∃𝑡 ∈ 𝐿 (𝐹 “ 𝑡) ⊆ 𝑜)))) |
5 | 3, 4 | syl3an2 1352 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∃𝑡 ∈ 𝐿 (𝐹 “ 𝑡) ⊆ 𝑜)))) |
6 | 1 | eleq2i 2680 |
. . . . . . . 8
⊢ (𝑡 ∈ 𝐿 ↔ 𝑡 ∈ (𝑌filGen𝐵)) |
7 | | elfg 21485 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (fBas‘𝑌) → (𝑡 ∈ (𝑌filGen𝐵) ↔ (𝑡 ⊆ 𝑌 ∧ ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡))) |
8 | 7 | 3ad2ant2 1076 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑡 ∈ (𝑌filGen𝐵) ↔ (𝑡 ⊆ 𝑌 ∧ ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡))) |
9 | | imass2 5420 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑠 ⊆ 𝑡 → (𝐹 “ 𝑠) ⊆ (𝐹 “ 𝑡)) |
10 | | sstr2 3575 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐹 “ 𝑠) ⊆ (𝐹 “ 𝑡) → ((𝐹 “ 𝑡) ⊆ 𝑜 → (𝐹 “ 𝑠) ⊆ 𝑜)) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑠 ⊆ 𝑡 → ((𝐹 “ 𝑡) ⊆ 𝑜 → (𝐹 “ 𝑠) ⊆ 𝑜)) |
12 | 11 | com12 32 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹 “ 𝑡) ⊆ 𝑜 → (𝑠 ⊆ 𝑡 → (𝐹 “ 𝑠) ⊆ 𝑜)) |
13 | 12 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐹 “ 𝑡) ⊆ 𝑜) → (𝑠 ⊆ 𝑡 → (𝐹 “ 𝑠) ⊆ 𝑜)) |
14 | 13 | reximdv 2999 |
. . . . . . . . . . . . 13
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ (𝐹 “ 𝑡) ⊆ 𝑜) → (∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜)) |
15 | 14 | ex 449 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐹 “ 𝑡) ⊆ 𝑜 → (∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜))) |
16 | 15 | com23 84 |
. . . . . . . . . . 11
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡 → ((𝐹 “ 𝑡) ⊆ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜))) |
17 | 16 | adantld 482 |
. . . . . . . . . 10
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝑡 ⊆ 𝑌 ∧ ∃𝑠 ∈ 𝐵 𝑠 ⊆ 𝑡) → ((𝐹 “ 𝑡) ⊆ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜))) |
18 | 8, 17 | sylbid 229 |
. . . . . . . . 9
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝑡 ∈ (𝑌filGen𝐵) → ((𝐹 “ 𝑡) ⊆ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜))) |
19 | 18 | adantr 480 |
. . . . . . . 8
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ 𝑋) → (𝑡 ∈ (𝑌filGen𝐵) → ((𝐹 “ 𝑡) ⊆ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜))) |
20 | 6, 19 | syl5bi 231 |
. . . . . . 7
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ 𝑋) → (𝑡 ∈ 𝐿 → ((𝐹 “ 𝑡) ⊆ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜))) |
21 | 20 | rexlimdv 3012 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ 𝑋) → (∃𝑡 ∈ 𝐿 (𝐹 “ 𝑡) ⊆ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜)) |
22 | | ssfg 21486 |
. . . . . . . . . . . 12
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ (𝑌filGen𝐵)) |
23 | 22, 1 | syl6sseqr 3615 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ (fBas‘𝑌) → 𝐵 ⊆ 𝐿) |
24 | 23 | sselda 3568 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ (fBas‘𝑌) ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ 𝐿) |
25 | 24 | 3ad2antl2 1217 |
. . . . . . . . 9
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝑠 ∈ 𝐵) → 𝑠 ∈ 𝐿) |
26 | 25 | ad2ant2r 779 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ 𝑋) ∧ (𝑠 ∈ 𝐵 ∧ (𝐹 “ 𝑠) ⊆ 𝑜)) → 𝑠 ∈ 𝐿) |
27 | | simprr 792 |
. . . . . . . 8
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ 𝑋) ∧ (𝑠 ∈ 𝐵 ∧ (𝐹 “ 𝑠) ⊆ 𝑜)) → (𝐹 “ 𝑠) ⊆ 𝑜) |
28 | | imaeq2 5381 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑠 → (𝐹 “ 𝑡) = (𝐹 “ 𝑠)) |
29 | 28 | sseq1d 3595 |
. . . . . . . . 9
⊢ (𝑡 = 𝑠 → ((𝐹 “ 𝑡) ⊆ 𝑜 ↔ (𝐹 “ 𝑠) ⊆ 𝑜)) |
30 | 29 | rspcev 3282 |
. . . . . . . 8
⊢ ((𝑠 ∈ 𝐿 ∧ (𝐹 “ 𝑠) ⊆ 𝑜) → ∃𝑡 ∈ 𝐿 (𝐹 “ 𝑡) ⊆ 𝑜) |
31 | 26, 27, 30 | syl2anc 691 |
. . . . . . 7
⊢ ((((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ 𝑋) ∧ (𝑠 ∈ 𝐵 ∧ (𝐹 “ 𝑠) ⊆ 𝑜)) → ∃𝑡 ∈ 𝐿 (𝐹 “ 𝑡) ⊆ 𝑜) |
32 | 31 | rexlimdvaa 3014 |
. . . . . 6
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ 𝑋) → (∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜 → ∃𝑡 ∈ 𝐿 (𝐹 “ 𝑡) ⊆ 𝑜)) |
33 | 21, 32 | impbid 201 |
. . . . 5
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ 𝑋) → (∃𝑡 ∈ 𝐿 (𝐹 “ 𝑡) ⊆ 𝑜 ↔ ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜)) |
34 | 33 | imbi2d 329 |
. . . 4
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ 𝑋) → ((𝐴 ∈ 𝑜 → ∃𝑡 ∈ 𝐿 (𝐹 “ 𝑡) ⊆ 𝑜) ↔ (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜))) |
35 | 34 | ralbidv 2969 |
. . 3
⊢ (((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) ∧ 𝐴 ∈ 𝑋) → (∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∃𝑡 ∈ 𝐿 (𝐹 “ 𝑡) ⊆ 𝑜) ↔ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜))) |
36 | 35 | pm5.32da 671 |
. 2
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → ((𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∃𝑡 ∈ 𝐿 (𝐹 “ 𝑡) ⊆ 𝑜)) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜)))) |
37 | 5, 36 | bitrd 267 |
1
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (𝐴 ∈ ((𝐽 fLimf 𝐿)‘𝐹) ↔ (𝐴 ∈ 𝑋 ∧ ∀𝑜 ∈ 𝐽 (𝐴 ∈ 𝑜 → ∃𝑠 ∈ 𝐵 (𝐹 “ 𝑠) ⊆ 𝑜)))) |