Metamath Proof Explorer

Theorem subbascn

Description: The continuity predicate when the range is given by a subbasis for a topology. (Contributed by Mario Carneiro, 7-Feb-2015) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses subbascn.1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
subbascn.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
subbascn.3 ⊢ ( 𝜑 → 𝐾 = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
subbascn.4 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
Assertion subbascn ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )

Proof

Step Hyp Ref Expression
1 subbascn.1 ⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 subbascn.2 ⊢ ( 𝜑 → 𝐵 ∈ 𝑉 )
3 subbascn.3 ⊢ ( 𝜑 → 𝐾 = ( topGen ‘ ( fi ‘ 𝐵 ) ) )
4 subbascn.4 ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
5 1 3 4 tgcn ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ( fi ‘ 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
6 2 adantr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → 𝐵 ∈ 𝑉 )
7 ssfii ⊢ ( 𝐵 ∈ 𝑉 → 𝐵 ⊆ ( fi ‘ 𝐵 ) )
8 ssralv ⊢ ( 𝐵 ⊆ ( fi ‘ 𝐵 ) → ( ∀ 𝑦 ∈ ( fi ‘ 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
9 6 7 8 3syl ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ ( fi ‘ 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
10 vex ⊢ 𝑥 ∈ V
11 elfi ⊢ ( ( 𝑥 ∈ V ∧ 𝐵 ∈ 𝑉 ) → ( 𝑥 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ∩ 𝑧 ) )
12 10 6 11 sylancr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝑥 ∈ ( fi ‘ 𝐵 ) ↔ ∃ 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ∩ 𝑧 ) )
13 simpr2 ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑥 = ∩ 𝑧 )
14 13 imaeq2d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑥 ) = ( ◡ 𝐹 “ ∩ 𝑧 ) )
15 ffun ⊢ ( 𝐹 : 𝑋 ⟶ 𝑌 → Fun 𝐹 )
16 15 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → Fun 𝐹 )
17 13 10 eqeltrrdi ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ∩ 𝑧 ∈ V )
18 intex ⊢ ( 𝑧 ≠ ∅ ↔ ∩ 𝑧 ∈ V )
19 17 18 sylibr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑧 ≠ ∅ )
20 intpreima ⊢ ( ( Fun 𝐹 ∧ 𝑧 ≠ ∅ ) → ( ◡ 𝐹 “ ∩ 𝑧 ) = ∩ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) )
21 16 19 20 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ ∩ 𝑧 ) = ∩ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) )
22 14 21 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑥 ) = ∩ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) )
23 topontop ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝐽 ∈ Top )
24 1 23 syl ⊢ ( 𝜑 → 𝐽 ∈ Top )
25 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝐽 ∈ Top )
26 simpr1 ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) )
27 26 elin2d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑧 ∈ Fin )
28 26 elin1d ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑧 ∈ 𝒫 𝐵 )
29 28 elpwid ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → 𝑧 ⊆ 𝐵 )
30 simpr3 ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
31 ssralv ⊢ ( 𝑧 ⊆ 𝐵 → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∀ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
32 29 30 31 sylc ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ∀ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
33 iinopn ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑧 ∈ Fin ∧ 𝑧 ≠ ∅ ∧ ∀ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ∩ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
34 25 27 19 32 33 syl13anc ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ∩ 𝑦 ∈ 𝑧 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 )
35 22 34 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) ∧ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) ∧ 𝑥 = ∩ 𝑧 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
36 35 3exp2 ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) → ( 𝑥 = ∩ 𝑧 → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) ) )
37 36 rexlimdv ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∃ 𝑧 ∈ ( 𝒫 𝐵 ∩ Fin ) 𝑥 = ∩ 𝑧 → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
38 12 37 sylbid ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( 𝑥 ∈ ( fi ‘ 𝐵 ) → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
39 38 com23 ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ( 𝑥 ∈ ( fi ‘ 𝐵 ) → ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) ) )
40 39 ralrimdv ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∀ 𝑥 ∈ ( fi ‘ 𝐵 ) ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) )
41 imaeq2 ⊢ ( 𝑦 = 𝑥 → ( ◡ 𝐹 “ 𝑦 ) = ( ◡ 𝐹 “ 𝑥 ) )
42 41 eleq1d ⊢ ( 𝑦 = 𝑥 → ( ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ↔ ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 ) )
43 42 cbvralvw ⊢ ( ∀ 𝑦 ∈ ( fi ‘ 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ↔ ∀ 𝑥 ∈ ( fi ‘ 𝐵 ) ( ◡ 𝐹 “ 𝑥 ) ∈ 𝐽 )
44 40 43 syl6ibr ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 → ∀ 𝑦 ∈ ( fi ‘ 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
45 9 44 impbid ⊢ ( ( 𝜑 ∧ 𝐹 : 𝑋 ⟶ 𝑌 ) → ( ∀ 𝑦 ∈ ( fi ‘ 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ↔ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) )
46 45 pm5.32da ⊢ ( 𝜑 → ( ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ ( fi ‘ 𝐵 ) ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )
47 5 46 bitrd ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐽 Cn 𝐾 ) ↔ ( 𝐹 : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐵 ( ◡ 𝐹 “ 𝑦 ) ∈ 𝐽 ) ) )