Step | Hyp | Ref
| Expression |
1 | | subbascn.1 |
. . 3
⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) |
2 | | subbascn.3 |
. . 3
⊢ (𝜑 → 𝐾 = (topGen‘(fi‘𝐵))) |
3 | | subbascn.4 |
. . 3
⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) |
4 | 1, 2, 3 | tgcn 21854 |
. 2
⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ (fi‘𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽))) |
5 | | subbascn.2 |
. . . . . 6
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
6 | 5 | adantr 483 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → 𝐵 ∈ 𝑉) |
7 | | ssfii 8877 |
. . . . 5
⊢ (𝐵 ∈ 𝑉 → 𝐵 ⊆ (fi‘𝐵)) |
8 | | ssralv 4032 |
. . . . 5
⊢ (𝐵 ⊆ (fi‘𝐵) → (∀𝑦 ∈ (fi‘𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽 → ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) |
9 | 6, 7, 8 | 3syl 18 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑦 ∈ (fi‘𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽 → ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) |
10 | | vex 3497 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
11 | | elfi 8871 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ 𝐵 ∈ 𝑉) → (𝑥 ∈ (fi‘𝐵) ↔ ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)𝑥 = ∩ 𝑧)) |
12 | 10, 6, 11 | sylancr 589 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (𝑥 ∈ (fi‘𝐵) ↔ ∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)𝑥 = ∩ 𝑧)) |
13 | | simpr2 1191 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑥 = ∩ 𝑧) |
14 | 13 | imaeq2d 5923 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ 𝑥) = (◡𝐹 “ ∩ 𝑧)) |
15 | | ffun 6511 |
. . . . . . . . . . . . . 14
⊢ (𝐹:𝑋⟶𝑌 → Fun 𝐹) |
16 | 15 | ad2antlr 725 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → Fun 𝐹) |
17 | 13, 10 | eqeltrrdi 2922 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → ∩ 𝑧 ∈ V) |
18 | | intex 5232 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ≠ ∅ ↔ ∩ 𝑧
∈ V) |
19 | 17, 18 | sylibr 236 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑧 ≠ ∅) |
20 | | intpreima 6832 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ 𝑧 ≠ ∅) → (◡𝐹 “ ∩ 𝑧) = ∩ 𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦)) |
21 | 16, 19, 20 | syl2anc 586 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ ∩ 𝑧) = ∩ 𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦)) |
22 | 14, 21 | eqtrd 2856 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ 𝑥) = ∩ 𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦)) |
23 | | topontop 21515 |
. . . . . . . . . . . . . 14
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ Top) |
24 | 1, 23 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐽 ∈ Top) |
25 | 24 | ad2antrr 724 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝐽 ∈ Top) |
26 | | simpr1 1190 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑧 ∈ (𝒫 𝐵 ∩ Fin)) |
27 | 26 | elin2d 4175 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑧 ∈ Fin) |
28 | 26 | elin1d 4174 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑧 ∈ 𝒫 𝐵) |
29 | 28 | elpwid 4552 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → 𝑧 ⊆ 𝐵) |
30 | | simpr3 1192 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽) |
31 | | ssralv 4032 |
. . . . . . . . . . . . 13
⊢ (𝑧 ⊆ 𝐵 → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∀𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽)) |
32 | 29, 30, 31 | sylc 65 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → ∀𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽) |
33 | | iinopn 21504 |
. . . . . . . . . . . 12
⊢ ((𝐽 ∈ Top ∧ (𝑧 ∈ Fin ∧ 𝑧 ≠ ∅ ∧
∀𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽)) → ∩ 𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽) |
34 | 25, 27, 19, 32, 33 | syl13anc 1368 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → ∩ 𝑦 ∈ 𝑧 (◡𝐹 “ 𝑦) ∈ 𝐽) |
35 | 22, 34 | eqeltrd 2913 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹:𝑋⟶𝑌) ∧ (𝑧 ∈ (𝒫 𝐵 ∩ Fin) ∧ 𝑥 = ∩ 𝑧 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) → (◡𝐹 “ 𝑥) ∈ 𝐽) |
36 | 35 | 3exp2 1350 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (𝑧 ∈ (𝒫 𝐵 ∩ Fin) → (𝑥 = ∩ 𝑧 → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → (◡𝐹 “ 𝑥) ∈ 𝐽)))) |
37 | 36 | rexlimdv 3283 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∃𝑧 ∈ (𝒫 𝐵 ∩ Fin)𝑥 = ∩ 𝑧 → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → (◡𝐹 “ 𝑥) ∈ 𝐽))) |
38 | 12, 37 | sylbid 242 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (𝑥 ∈ (fi‘𝐵) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → (◡𝐹 “ 𝑥) ∈ 𝐽))) |
39 | 38 | com23 86 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → (𝑥 ∈ (fi‘𝐵) → (◡𝐹 “ 𝑥) ∈ 𝐽))) |
40 | 39 | ralrimdv 3188 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∀𝑥 ∈ (fi‘𝐵)(◡𝐹 “ 𝑥) ∈ 𝐽)) |
41 | | imaeq2 5919 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → (◡𝐹 “ 𝑦) = (◡𝐹 “ 𝑥)) |
42 | 41 | eleq1d 2897 |
. . . . . 6
⊢ (𝑦 = 𝑥 → ((◡𝐹 “ 𝑦) ∈ 𝐽 ↔ (◡𝐹 “ 𝑥) ∈ 𝐽)) |
43 | 42 | cbvralvw 3449 |
. . . . 5
⊢
(∀𝑦 ∈
(fi‘𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽 ↔ ∀𝑥 ∈ (fi‘𝐵)(◡𝐹 “ 𝑥) ∈ 𝐽) |
44 | 40, 43 | syl6ibr 254 |
. . . 4
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽 → ∀𝑦 ∈ (fi‘𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽)) |
45 | 9, 44 | impbid 214 |
. . 3
⊢ ((𝜑 ∧ 𝐹:𝑋⟶𝑌) → (∀𝑦 ∈ (fi‘𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽 ↔ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽)) |
46 | 45 | pm5.32da 581 |
. 2
⊢ (𝜑 → ((𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ (fi‘𝐵)(◡𝐹 “ 𝑦) ∈ 𝐽) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽))) |
47 | 4, 46 | bitrd 281 |
1
⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝐵 (◡𝐹 “ 𝑦) ∈ 𝐽))) |