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

Proof

Step Hyp Ref Expression
1 tgcn.1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 tgcn.3 ⊢ ( 𝜑 → 𝐾 = ( topGen ‘ 𝐵 ) )
3 tgcn.4 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
4 iscn ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
5 1 3 4 syl2anc ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
6 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
7 3 6 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
8 2 7 eqeltrrd ⊢ ( 𝜑 → ( topGen ‘ 𝐵 ) ∈ Top )
9 tgclb ⊢ ( 𝐵 ∈ TopBases ↔ ( topGen ‘ 𝐵 ) ∈ Top )
10 8 9 sylibr ⊢ ( 𝜑 → 𝐵 ∈ TopBases )
11 bastg ⊢ ( 𝐵 ∈ TopBases → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
12 10 11 syl ⊢ ( 𝜑 → 𝐵 ⊆ ( topGen ‘ 𝐵 ) )
13 12 2 sseqtrrd ⊢ ( 𝜑 → 𝐵 ⊆ 𝐾 )
14 ssralv ⊢ ( 𝐵 ⊆ 𝐾 → ( ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
15 13 14 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
16 2 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 ↔ 𝑥 ∈ ( topGen ‘ 𝐵 ) ) )
17 eltg3 ⊢ ( 𝐵 ∈ TopBases → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑧 ) ) )
18 10 17 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ( topGen ‘ 𝐵 ) ↔ ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑧 ) ) )
19 16 18 bitrd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 ↔ ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑧 ) ) )
20 ssralv ⊢ ( 𝑧 ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∀ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
21 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
22 1 21 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
23 iunopn ⊢ ( ( 𝐽 ∈ Top ∧ ∀ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) → ∪ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
24 23 ex ⊢ ( 𝐽 ∈ Top → ( ∀ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∪ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
25 22 24 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∪ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
26 20 25 sylan9r ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∪ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
27 imaeq2 ⊢ ( 𝑥 = ∪ 𝑧 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ ∪ 𝑧 ) )
28 imauni ⊢ ( ◡ 𝐹 “ ∪ 𝑧 ) = ∪ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 )
29 27 28 eqtrdi ⊢ ( 𝑥 = ∪ 𝑧 → ( ◡ 𝐹 “ 𝑥 ) = ∪ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) )
30 29 eleq1d ⊢ ( 𝑥 = ∪ 𝑧 → ( ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ↔ ∪ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
31 30 imbi2d ⊢ ( 𝑥 = ∪ 𝑧 → ( ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ↔ ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∪ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
32 26 31 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑧 ⊆ 𝐵 ) → ( 𝑥 = ∪ 𝑧 → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
33 32 expimpd ⊢ ( 𝜑 → ( ( 𝑧 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑧 ) → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
34 33 exlimdv ⊢ ( 𝜑 → ( ∃ 𝑧 ( 𝑧 ⊆ 𝐵 ∧ 𝑥 = ∪ 𝑧 ) → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
35 19 34 sylbid ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐾 → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
36 35 imp ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐾 ) → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) )
37 36 ralrimdva ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) )
38 imaeq2 ⊢ ( 𝑥 = 𝑦 → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ 𝑦 ) )
39 38 eleq1d ⊢ ( 𝑥 = 𝑦 → ( ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
40 39 cbvralvw ⊢ ( ∀ 𝑥 ∈ 𝐾 ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ↔ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
41 37 40 syl6ib ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
42 15 41 impbid ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ↔ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
43 42 anbi2d ⊢ ( 𝜑 → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
44 5 43 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )