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∈JCnK↔F:X⟶Y∧∀y∈BF-1y∈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∈JCnK↔F:X⟶Y∧∀y∈KF-1y∈J
5 1 3 4 syl2anc ⊢φ→F∈JCnK↔F:X⟶Y∧∀y∈KF-1y∈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∈KF-1y∈J→∀y∈BF-1y∈J
15 13 14 syl ⊢φ→∀y∈KF-1y∈J→∀y∈BF-1y∈J
16 2 eleq2d ⊢φ→x∈K↔x∈topGen⁡B
17 eltg3 ⊢B∈TopBases→x∈topGen⁡B↔∃zz⊆B∧x=⋃z
18 10 17 syl ⊢φ→x∈topGen⁡B↔∃zz⊆B∧x=⋃z
19 16 18 bitrd ⊢φ→x∈K↔∃zz⊆B∧x=⋃z
20 ssralv ⊢z⊆B→∀y∈BF-1y∈J→∀y∈zF-1y∈J
21 topontop ⊢J∈TopOn⁡X→J∈Top
22 1 21 syl ⊢φ→J∈Top
23 iunopn ⊢J∈Top∧∀y∈zF-1y∈J→⋃y∈zF-1y∈J
24 23 ex ⊢J∈Top→∀y∈zF-1y∈J→⋃y∈zF-1y∈J
25 22 24 syl ⊢φ→∀y∈zF-1y∈J→⋃y∈zF-1y∈J
26 20 25 sylan9r ⊢φ∧z⊆B→∀y∈BF-1y∈J→⋃y∈zF-1y∈J
27 imaeq2 ⊢x=⋃z→F-1x=F-1⋃z
28 imauni ⊢F-1⋃z=⋃y∈zF-1y
29 27 28 eqtrdi ⊢x=⋃z→F-1x=⋃y∈zF-1y
30 29 eleq1d ⊢x=⋃z→F-1x∈J↔⋃y∈zF-1y∈J
31 30 imbi2d ⊢x=⋃z→∀y∈BF-1y∈J→F-1x∈J↔∀y∈BF-1y∈J→⋃y∈zF-1y∈J
32 26 31 syl5ibrcom ⊢φ∧z⊆B→x=⋃z→∀y∈BF-1y∈J→F-1x∈J
33 32 expimpd ⊢φ→z⊆B∧x=⋃z→∀y∈BF-1y∈J→F-1x∈J
34 33 exlimdv ⊢φ→∃zz⊆B∧x=⋃z→∀y∈BF-1y∈J→F-1x∈J
35 19 34 sylbid ⊢φ→x∈K→∀y∈BF-1y∈J→F-1x∈J
36 35 imp ⊢φ∧x∈K→∀y∈BF-1y∈J→F-1x∈J
37 36 ralrimdva ⊢φ→∀y∈BF-1y∈J→∀x∈KF-1x∈J
38 imaeq2 ⊢x=y→F-1x=F-1y
39 38 eleq1d ⊢x=y→F-1x∈J↔F-1y∈J
40 39 cbvralvw ⊢∀x∈KF-1x∈J↔∀y∈KF-1y∈J
41 37 40 imbitrdi ⊢φ→∀y∈BF-1y∈J→∀y∈KF-1y∈J
42 15 41 impbid ⊢φ→∀y∈KF-1y∈J↔∀y∈BF-1y∈J
43 42 anbi2d ⊢φ→F:X⟶Y∧∀y∈KF-1y∈J↔F:X⟶Y∧∀y∈BF-1y∈J
44 5 43 bitrd ⊢φ→F∈JCnK↔F:X⟶Y∧∀y∈BF-1y∈J