Metamath Proof Explorer

Theorem subbascn

Description: The continuity predicate when the range is given by a subbasis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses subbascn.1 ⊢ φ → J ∈ TopOn ⁡ X
subbascn.2 ⊢ φ → B ∈ V
subbascn.3 ⊢ φ → K = topGen ⁡ fi ⁡ B
subbascn.4 ⊢ φ → K ∈ TopOn ⁡ Y
Assertion subbascn ⊢ φ → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ y ∈ B F -1 y ∈ J

Proof

Step Hyp Ref Expression
1 subbascn.1 ⊢ φ → J ∈ TopOn ⁡ X
2 subbascn.2 ⊢ φ → B ∈ V
3 subbascn.3 ⊢ φ → K = topGen ⁡ fi ⁡ B
4 subbascn.4 ⊢ φ → K ∈ TopOn ⁡ Y
5 1 3 4 tgcn ⊢ φ → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ y ∈ fi ⁡ B F -1 y ∈ J
6 2 adantr ⊢ φ ∧ F : X ⟶ Y → B ∈ V
7 ssfii ⊢ B ∈ V → B ⊆ fi ⁡ B
8 ssralv ⊢ B ⊆ fi ⁡ B → ∀ y ∈ fi ⁡ B F -1 y ∈ J → ∀ y ∈ B F -1 y ∈ J
9 6 7 8 3syl ⊢ φ ∧ F : X ⟶ Y → ∀ y ∈ fi ⁡ B F -1 y ∈ J → ∀ y ∈ B F -1 y ∈ J
10 vex ⊢ x ∈ V
11 elfi ⊢ x ∈ V ∧ B ∈ V → x ∈ fi ⁡ B ↔ ∃ z ∈ 𝒫 B ∩ Fin x = ⋂ z
12 10 6 11 sylancr ⊢ φ ∧ F : X ⟶ Y → x ∈ fi ⁡ B ↔ ∃ z ∈ 𝒫 B ∩ Fin x = ⋂ z
13 simpr2 ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → x = ⋂ z
14 13 imaeq2d ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → F -1 x = F -1 ⋂ z
15 ffun ⊢ F : X ⟶ Y → Fun ⁡ F
16 15 ad2antlr ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → Fun ⁡ F
17 13 10 eqeltrrdi ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → ⋂ z ∈ V
18 intex ⊢ z ≠ ∅ ↔ ⋂ z ∈ V
19 17 18 sylibr ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → z ≠ ∅
20 intpreima ⊢ Fun ⁡ F ∧ z ≠ ∅ → F -1 ⋂ z = ⋂ y ∈ z F -1 y
21 16 19 20 syl2anc ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → F -1 ⋂ z = ⋂ y ∈ z F -1 y
22 14 21 eqtrd ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → F -1 x = ⋂ y ∈ z F -1 y
23 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
24 1 23 syl ⊢ φ → J ∈ Top
25 24 ad2antrr ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → J ∈ Top
26 simpr1 ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → z ∈ 𝒫 B ∩ Fin
27 26 elin2d ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → z ∈ Fin
28 26 elin1d ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → z ∈ 𝒫 B
29 28 elpwid ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → z ⊆ B
30 simpr3 ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → ∀ y ∈ B F -1 y ∈ J
31 ssralv ⊢ z ⊆ B → ∀ y ∈ B F -1 y ∈ J → ∀ y ∈ z F -1 y ∈ J
32 29 30 31 sylc ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → ∀ y ∈ z F -1 y ∈ J
33 iinopn ⊢ J ∈ Top ∧ z ∈ Fin ∧ z ≠ ∅ ∧ ∀ y ∈ z F -1 y ∈ J → ⋂ y ∈ z F -1 y ∈ J
34 25 27 19 32 33 syl13anc ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → ⋂ y ∈ z F -1 y ∈ J
35 22 34 eqeltrd ⊢ φ ∧ F : X ⟶ Y ∧ z ∈ 𝒫 B ∩ Fin ∧ x = ⋂ z ∧ ∀ y ∈ B F -1 y ∈ J → F -1 x ∈ J
36 35 3exp2 ⊢ φ ∧ F : X ⟶ Y → z ∈ 𝒫 B ∩ Fin → x = ⋂ z → ∀ y ∈ B F -1 y ∈ J → F -1 x ∈ J
37 36 rexlimdv ⊢ φ ∧ F : X ⟶ Y → ∃ z ∈ 𝒫 B ∩ Fin x = ⋂ z → ∀ y ∈ B F -1 y ∈ J → F -1 x ∈ J
38 12 37 sylbid ⊢ φ ∧ F : X ⟶ Y → x ∈ fi ⁡ B → ∀ y ∈ B F -1 y ∈ J → F -1 x ∈ J
39 38 com23 ⊢ φ ∧ F : X ⟶ Y → ∀ y ∈ B F -1 y ∈ J → x ∈ fi ⁡ B → F -1 x ∈ J
40 39 ralrimdv ⊢ φ ∧ F : X ⟶ Y → ∀ y ∈ B F -1 y ∈ J → ∀ x ∈ fi ⁡ B F -1 x ∈ J
41 imaeq2 ⊢ y = x → F -1 y = F -1 x
42 41 eleq1d ⊢ y = x → F -1 y ∈ J ↔ F -1 x ∈ J
43 42 cbvralvw ⊢ ∀ y ∈ fi ⁡ B F -1 y ∈ J ↔ ∀ x ∈ fi ⁡ B F -1 x ∈ J
44 40 43 imbitrrdi ⊢ φ ∧ F : X ⟶ Y → ∀ y ∈ B F -1 y ∈ J → ∀ y ∈ fi ⁡ B F -1 y ∈ J
45 9 44 impbid ⊢ φ ∧ F : X ⟶ Y → ∀ y ∈ fi ⁡ B F -1 y ∈ J ↔ ∀ y ∈ B F -1 y ∈ J
46 45 pm5.32da ⊢ φ → F : X ⟶ Y ∧ ∀ y ∈ fi ⁡ B F -1 y ∈ J ↔ F : X ⟶ Y ∧ ∀ y ∈ B F -1 y ∈ J
47 5 46 bitrd ⊢ φ → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ y ∈ B F -1 y ∈ J