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 𝐾 ) ↔ ( 𝐹 : 𝑋𝑌 ∧ ∀ 𝑦𝐵 ( 𝐹𝑦 ) ∈ 𝐽 ) ) )