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 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
tgcn.3 ⊢ ( 𝜑 → 𝐾 = ( topGen ‘ 𝐵 ) )
tgcn.4 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
tgcnp.5 ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
Assertion tgcnp ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 tgcn.1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 tgcn.3 ⊢ ( 𝜑 → 𝐾 = ( topGen ‘ 𝐵 ) )
3 tgcn.4 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
4 tgcnp.5 ⊢ ( 𝜑 → 𝑃 ∈ 𝑋 )
5 iscnp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
6 1 3 4 5 syl3anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
7 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
8 3 7 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
9 2 8 eqeltrrd ⊢ ( 𝜑 → ( topGen ‘ 𝐵 ) ∈ Top )
10 tgclb ⊢ ( 𝐵 ∈ TopBases ↔ ( topGen ‘ 𝐵 ) ∈ Top )
11 9 10 sylibr ⊢ ( 𝜑 → 𝐵 ∈ TopBases )
12 bastg ⊢ ( 𝐵 ∈ TopBases → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
13 11 12 syl ⊢ ( 𝜑 → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
14 13 2 sseqtrrd ⊢ ( 𝜑 → 𝐵 ⊆ 𝐾 )
15 ssralv ⊢ ( 𝐵 ⊆ 𝐾 → ( ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) )
16 14 15 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) )
17 16 anim2d ⊢ ( 𝜑 → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
18 6 17 sylbid ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )
19 2 eleq2d ⊢ ( 𝜑 → ( 𝑧 ∈ 𝐾 ↔ 𝑧 ∈ ( topGen ‘ 𝐵 ) ) )
20 19 biimpa ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐾 ) → 𝑧 ∈ ( topGen ‘ 𝐵 ) )
21 tg2 ⊢ ( ( 𝑧 ∈ ( topGen ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 ) → ∃ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) )
22 r19.29 ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) → ∃ 𝑦 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) )
23 sstr ⊢ ( ( ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) → ( 𝐹 “ 𝑥 ) ⊆ 𝑧 )
24 23 expcom ⊢ ( 𝑦 ⊆ 𝑧 → ( ( 𝐹 “ 𝑥 ) ⊆ 𝑦 → ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) )
25 24 anim2d ⊢ ( 𝑦 ⊆ 𝑧 → ( ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) )
26 25 reximdv ⊢ ( 𝑦 ⊆ 𝑧 → ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) )
27 26 com12 ⊢ ( ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) → ( 𝑦 ⊆ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) )
28 27 imim2i ⊢ ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ( 𝑦 ⊆ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) ) )
29 28 imp32 ⊢ ( ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) )
30 29 rexlimivw ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ∧ ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) )
31 22 30 syl ⊢ ( ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ∧ ∃ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) )
32 31 expcom ⊢ ( ∃ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 ∧ 𝑦 ⊆ 𝑧 ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) )
33 21 32 syl ⊢ ( ( 𝑧 ∈ ( topGen ‘ 𝐵 ) ∧ ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) )
34 33 ex ⊢ ( 𝑧 ∈ ( topGen ‘ 𝐵 ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) ) )
35 34 com23 ⊢ ( 𝑧 ∈ ( topGen ‘ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) ) )
36 20 35 syl ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐾 ) → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) ) )
37 36 ralrimdva ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) → ∀ 𝑧 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) ) )
38 37 anim2d ⊢ ( 𝜑 → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) → ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑧 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) ) ) )
39 iscnp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑃 ∈ 𝑋 ) → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑧 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) ) ) )
40 1 3 4 39 syl3anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑧 ∈ 𝐾 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑧 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑧 ) ) ) ) )
41 38 40 sylibrd ⊢ ( 𝜑 → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) → 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ) )
42 18 41 impbid ⊢ ( 𝜑 → ( 𝐹 ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑃 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐵 ( ( 𝐹 ‘ 𝑃 ) ∈ 𝑦 → ∃ 𝑥 ∈ 𝐽 ( 𝑃 ∈ 𝑥 ∧ ( 𝐹 “ 𝑥 ) ⊆ 𝑦 ) ) ) ) )