Metamath Proof Explorer

Theorem tgcn

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

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

Proof

Step Hyp Ref Expression
1 tgcn.1 ⊢ φ → J ∈ TopOn ⁡ X
2 tgcn.3 ⊢ φ → K = topGen ⁡ B
3 tgcn.4 ⊢ φ → K ∈ TopOn ⁡ Y
4 iscn ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ y ∈ K F -1 y ∈ J
5 1 3 4 syl2anc ⊢ φ → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ y ∈ K F -1 y ∈ J
6 topontop ⊢ K ∈ TopOn ⁡ Y → K ∈ Top
7 3 6 syl ⊢ φ → K ∈ Top
8 2 7 eqeltrrd ⊢ φ → topGen ⁡ B ∈ Top
9 tgclb ⊢ B ∈ TopBases ↔ topGen ⁡ B ∈ Top
10 8 9 sylibr ⊢ φ → B ∈ TopBases
11 bastg ⊢ B ∈ TopBases → B ⊆ topGen ⁡ B
12 10 11 syl ⊢ φ → B ⊆ topGen ⁡ B
13 12 2 sseqtrrd ⊢ φ → B ⊆ K
14 ssralv ⊢ B ⊆ K → ∀ y ∈ K F -1 y ∈ J → ∀ y ∈ B F -1 y ∈ J
15 13 14 syl ⊢ φ → ∀ y ∈ K F -1 y ∈ J → ∀ y ∈ B F -1 y ∈ J
16 2 eleq2d ⊢ φ → x ∈ K ↔ x ∈ topGen ⁡ B
17 eltg3 ⊢ B ∈ TopBases → x ∈ topGen ⁡ B ↔ ∃ z z ⊆ B ∧ x = ⋃ z
18 10 17 syl ⊢ φ → x ∈ topGen ⁡ B ↔ ∃ z z ⊆ B ∧ x = ⋃ z
19 16 18 bitrd ⊢ φ → x ∈ K ↔ ∃ z z ⊆ B ∧ x = ⋃ z
20 ssralv ⊢ z ⊆ B → ∀ y ∈ B F -1 y ∈ J → ∀ y ∈ z F -1 y ∈ J
21 topontop ⊢ J ∈ TopOn ⁡ X → J ∈ Top
22 1 21 syl ⊢ φ → J ∈ Top
23 iunopn ⊢ J ∈ Top ∧ ∀ y ∈ z F -1 y ∈ J → ⋃ y ∈ z F -1 y ∈ J
24 23 ex ⊢ J ∈ Top → ∀ y ∈ z F -1 y ∈ J → ⋃ y ∈ z F -1 y ∈ J
25 22 24 syl ⊢ φ → ∀ y ∈ z F -1 y ∈ J → ⋃ y ∈ z F -1 y ∈ J
26 20 25 sylan9r ⊢ φ ∧ z ⊆ B → ∀ y ∈ B F -1 y ∈ J → ⋃ y ∈ z F -1 y ∈ J
27 imaeq2 ⊢ x = ⋃ z → F -1 x = F -1 ⋃ z
28 imauni ⊢ F -1 ⋃ z = ⋃ y ∈ z F -1 y
29 27 28 eqtrdi ⊢ x = ⋃ z → F -1 x = ⋃ y ∈ z F -1 y
30 29 eleq1d ⊢ x = ⋃ z → F -1 x ∈ J ↔ ⋃ y ∈ z F -1 y ∈ J
31 30 imbi2d ⊢ x = ⋃ z → ∀ y ∈ B F -1 y ∈ J → F -1 x ∈ J ↔ ∀ y ∈ B F -1 y ∈ J → ⋃ y ∈ z F -1 y ∈ J
32 26 31 syl5ibrcom ⊢ φ ∧ z ⊆ B → x = ⋃ z → ∀ y ∈ B F -1 y ∈ J → F -1 x ∈ J
33 32 expimpd ⊢ φ → z ⊆ B ∧ x = ⋃ z → ∀ y ∈ B F -1 y ∈ J → F -1 x ∈ J
34 33 exlimdv ⊢ φ → ∃ z z ⊆ B ∧ x = ⋃ z → ∀ y ∈ B F -1 y ∈ J → F -1 x ∈ J
35 19 34 sylbid ⊢ φ → x ∈ K → ∀ y ∈ B F -1 y ∈ J → F -1 x ∈ J
36 35 imp ⊢ φ ∧ x ∈ K → ∀ y ∈ B F -1 y ∈ J → F -1 x ∈ J
37 36 ralrimdva ⊢ φ → ∀ y ∈ B F -1 y ∈ J → ∀ x ∈ K F -1 x ∈ J
38 imaeq2 ⊢ x = y → F -1 x = F -1 y
39 38 eleq1d ⊢ x = y → F -1 x ∈ J ↔ F -1 y ∈ J
40 39 cbvralvw ⊢ ∀ x ∈ K F -1 x ∈ J ↔ ∀ y ∈ K F -1 y ∈ J
41 37 40 imbitrdi ⊢ φ → ∀ y ∈ B F -1 y ∈ J → ∀ y ∈ K F -1 y ∈ J
42 15 41 impbid ⊢ φ → ∀ y ∈ K F -1 y ∈ J ↔ ∀ y ∈ B F -1 y ∈ J
43 42 anbi2d ⊢ φ → F : X ⟶ Y ∧ ∀ y ∈ K F -1 y ∈ J ↔ F : X ⟶ Y ∧ ∀ y ∈ B F -1 y ∈ J
44 5 43 bitrd ⊢ φ → F ∈ J Cn K ↔ F : X ⟶ Y ∧ ∀ y ∈ B F -1 y ∈ J