Metamath Proof Explorer

Theorem tgcnp

Description: The "continuous at a point" predicate when the range is given by a basis for a topology. (Contributed by Mario Carneiro, 3-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
tgcnp.5 ⊢ φ → P ∈ X
Assertion tgcnp ⊢ φ → F ∈ J CnP K ⁡ P ↔ F : X ⟶ Y ∧ ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y

Proof

Step Hyp Ref Expression
1 tgcn.1 ⊢ φ → J ∈ TopOn ⁡ X
2 tgcn.3 ⊢ φ → K = topGen ⁡ B
3 tgcn.4 ⊢ φ → K ∈ TopOn ⁡ Y
4 tgcnp.5 ⊢ φ → P ∈ X
5 iscnp ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ P ∈ X → F ∈ J CnP K ⁡ P ↔ F : X ⟶ Y ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y
6 1 3 4 5 syl3anc ⊢ φ → F ∈ J CnP K ⁡ P ↔ F : X ⟶ Y ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y
7 topontop ⊢ K ∈ TopOn ⁡ Y → K ∈ Top
8 3 7 syl ⊢ φ → K ∈ Top
9 2 8 eqeltrrd ⊢ φ → topGen ⁡ B ∈ Top
10 tgclb ⊢ B ∈ TopBases ↔ topGen ⁡ B ∈ Top
11 9 10 sylibr ⊢ φ → B ∈ TopBases
12 bastg ⊢ B ∈ TopBases → B ⊆ topGen ⁡ B
13 11 12 syl ⊢ φ → B ⊆ topGen ⁡ B
14 13 2 sseqtrrd ⊢ φ → B ⊆ K
15 ssralv ⊢ B ⊆ K → ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y
16 14 15 syl ⊢ φ → ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y
17 16 anim2d ⊢ φ → F : X ⟶ Y ∧ ∀ y ∈ K F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → F : X ⟶ Y ∧ ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y
18 6 17 sylbid ⊢ φ → F ∈ J CnP K ⁡ P → F : X ⟶ Y ∧ ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y
19 2 eleq2d ⊢ φ → z ∈ K ↔ z ∈ topGen ⁡ B
20 19 biimpa ⊢ φ ∧ z ∈ K → z ∈ topGen ⁡ B
21 tg2 ⊢ z ∈ topGen ⁡ B ∧ F ⁡ P ∈ z → ∃ y ∈ B F ⁡ P ∈ y ∧ y ⊆ z
22 r19.29 ⊢ ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ∧ ∃ y ∈ B F ⁡ P ∈ y ∧ y ⊆ z → ∃ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ∧ F ⁡ P ∈ y ∧ y ⊆ z
23 sstr ⊢ F x ⊆ y ∧ y ⊆ z → F x ⊆ z
24 23 expcom ⊢ y ⊆ z → F x ⊆ y → F x ⊆ z
25 24 anim2d ⊢ y ⊆ z → P ∈ x ∧ F x ⊆ y → P ∈ x ∧ F x ⊆ z
26 25 reximdv ⊢ y ⊆ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
27 26 com12 ⊢ ∃ x ∈ J P ∈ x ∧ F x ⊆ y → y ⊆ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
28 27 imim2i ⊢ F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → F ⁡ P ∈ y → y ⊆ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
29 28 imp32 ⊢ F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ∧ F ⁡ P ∈ y ∧ y ⊆ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
30 29 rexlimivw ⊢ ∃ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ∧ F ⁡ P ∈ y ∧ y ⊆ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
31 22 30 syl ⊢ ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y ∧ ∃ y ∈ B F ⁡ P ∈ y ∧ y ⊆ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
32 31 expcom ⊢ ∃ y ∈ B F ⁡ P ∈ y ∧ y ⊆ z → ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
33 21 32 syl ⊢ z ∈ topGen ⁡ B ∧ F ⁡ P ∈ z → ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
34 33 ex ⊢ z ∈ topGen ⁡ B → F ⁡ P ∈ z → ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
35 34 com23 ⊢ z ∈ topGen ⁡ B → ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → F ⁡ P ∈ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
36 20 35 syl ⊢ φ ∧ z ∈ K → ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → F ⁡ P ∈ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
37 36 ralrimdva ⊢ φ → ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → ∀ z ∈ K F ⁡ P ∈ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
38 37 anim2d ⊢ φ → F : X ⟶ Y ∧ ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → F : X ⟶ Y ∧ ∀ z ∈ K F ⁡ P ∈ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
39 iscnp ⊢ J ∈ TopOn ⁡ X ∧ K ∈ TopOn ⁡ Y ∧ P ∈ X → F ∈ J CnP K ⁡ P ↔ F : X ⟶ Y ∧ ∀ z ∈ K F ⁡ P ∈ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
40 1 3 4 39 syl3anc ⊢ φ → F ∈ J CnP K ⁡ P ↔ F : X ⟶ Y ∧ ∀ z ∈ K F ⁡ P ∈ z → ∃ x ∈ J P ∈ x ∧ F x ⊆ z
41 38 40 sylibrd ⊢ φ → F : X ⟶ Y ∧ ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y → F ∈ J CnP K ⁡ P
42 18 41 impbid ⊢ φ → F ∈ J CnP K ⁡ P ↔ F : X ⟶ Y ∧ ∀ y ∈ B F ⁡ P ∈ y → ∃ x ∈ J P ∈ x ∧ F x ⊆ y