Metamath Proof Explorer

Theorem cnconst2

Description: A constant function is continuous. (Contributed by Mario Carneiro, 19-Mar-2015)

Ref Expression
Assertion cnconst2 ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) → ( 𝑋 × { 𝐵 } ) ∈ ( 𝐽 Cn 𝐾 ) )

Proof

Step Hyp Ref Expression
1 fconst6g ⊢ ( 𝐵 ∈ 𝑌 → ( 𝑋 × { 𝐵 } ) : 𝑋 ⟶ 𝑌 )
2 1 3ad2ant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) → ( 𝑋 × { 𝐵 } ) : 𝑋 ⟶ 𝑌 )
3 2 adantr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑋 × { 𝐵 } ) : 𝑋 ⟶ 𝑌 )
4 simpll3 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝐾 ) → 𝐵 ∈ 𝑌 )
5 simplr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝐾 ) → 𝑥 ∈ 𝑋 )
6 fvconst2g ⊢ ( ( 𝐵 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑋 × { 𝐵 } ) ‘ 𝑥 ) = 𝐵 )
7 4 5 6 syl2anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝐾 ) → ( ( 𝑋 × { 𝐵 } ) ‘ 𝑥 ) = 𝐵 )
8 7 eleq1d ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝐾 ) → ( ( ( 𝑋 × { 𝐵 } ) ‘ 𝑥 ) ∈ 𝑦 ↔ 𝐵 ∈ 𝑦 ) )
9 simpll1 ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝐵 ∈ 𝑦 ) ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
10 toponmax ⊢ ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) → 𝑋 ∈ 𝐽 )
11 9 10 syl ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝐵 ∈ 𝑦 ) ) → 𝑋 ∈ 𝐽 )
12 simplr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝐵 ∈ 𝑦 ) ) → 𝑥 ∈ 𝑋 )
13 df-ima ⊢ ( ( 𝑋 × { 𝐵 } ) “ 𝑋 ) = ran ( ( 𝑋 × { 𝐵 } ) ↾ 𝑋 )
14 ssid ⊢ 𝑋 ⊆ 𝑋
15 xpssres ⊢ ( 𝑋 ⊆ 𝑋 → ( ( 𝑋 × { 𝐵 } ) ↾ 𝑋 ) = ( 𝑋 × { 𝐵 } ) )
16 14 15 ax-mp ⊢ ( ( 𝑋 × { 𝐵 } ) ↾ 𝑋 ) = ( 𝑋 × { 𝐵 } )
17 16 rneqi ⊢ ran ( ( 𝑋 × { 𝐵 } ) ↾ 𝑋 ) = ran ( 𝑋 × { 𝐵 } )
18 rnxpss ⊢ ran ( 𝑋 × { 𝐵 } ) ⊆ { 𝐵 }
19 17 18 eqsstri ⊢ ran ( ( 𝑋 × { 𝐵 } ) ↾ 𝑋 ) ⊆ { 𝐵 }
20 simprr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝐵 ∈ 𝑦 ) ) → 𝐵 ∈ 𝑦 )
21 20 snssd ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝐵 ∈ 𝑦 ) ) → { 𝐵 } ⊆ 𝑦 )
22 19 21 sstrid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝐵 ∈ 𝑦 ) ) → ran ( ( 𝑋 × { 𝐵 } ) ↾ 𝑋 ) ⊆ 𝑦 )
23 13 22 eqsstrid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝐵 ∈ 𝑦 ) ) → ( ( 𝑋 × { 𝐵 } ) “ 𝑋 ) ⊆ 𝑦 )
24 eleq2 ⊢ ( 𝑢 = 𝑋 → ( 𝑥 ∈ 𝑢 ↔ 𝑥 ∈ 𝑋 ) )
25 imaeq2 ⊢ ( 𝑢 = 𝑋 → ( ( 𝑋 × { 𝐵 } ) “ 𝑢 ) = ( ( 𝑋 × { 𝐵 } ) “ 𝑋 ) )
26 25 sseq1d ⊢ ( 𝑢 = 𝑋 → ( ( ( 𝑋 × { 𝐵 } ) “ 𝑢 ) ⊆ 𝑦 ↔ ( ( 𝑋 × { 𝐵 } ) “ 𝑋 ) ⊆ 𝑦 ) )
27 24 26 anbi12d ⊢ ( 𝑢 = 𝑋 → ( ( 𝑥 ∈ 𝑢 ∧ ( ( 𝑋 × { 𝐵 } ) “ 𝑢 ) ⊆ 𝑦 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑋 × { 𝐵 } ) “ 𝑋 ) ⊆ 𝑦 ) ) )
28 27 rspcev ⊢ ( ( 𝑋 ∈ 𝐽 ∧ ( 𝑥 ∈ 𝑋 ∧ ( ( 𝑋 × { 𝐵 } ) “ 𝑋 ) ⊆ 𝑦 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ( ( 𝑋 × { 𝐵 } ) “ 𝑢 ) ⊆ 𝑦 ) )
29 11 12 23 28 syl12anc ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑦 ∈ 𝐾 ∧ 𝐵 ∈ 𝑦 ) ) → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ( ( 𝑋 × { 𝐵 } ) “ 𝑢 ) ⊆ 𝑦 ) )
30 29 expr ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝐾 ) → ( 𝐵 ∈ 𝑦 → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ( ( 𝑋 × { 𝐵 } ) “ 𝑢 ) ⊆ 𝑦 ) ) )
31 8 30 sylbid ⊢ ( ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑦 ∈ 𝐾 ) → ( ( ( 𝑋 × { 𝐵 } ) ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ( ( 𝑋 × { 𝐵 } ) “ 𝑢 ) ⊆ 𝑦 ) ) )
32 31 ralrimiva ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑦 ∈ 𝐾 ( ( ( 𝑋 × { 𝐵 } ) ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ( ( 𝑋 × { 𝐵 } ) “ 𝑢 ) ⊆ 𝑦 ) ) )
33 simpl1 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
34 simpl2 ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
35 simpr ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
36 iscnp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑋 × { 𝐵 } ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ( ( 𝑋 × { 𝐵 } ) : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( ( 𝑋 × { 𝐵 } ) ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ( ( 𝑋 × { 𝐵 } ) “ 𝑢 ) ⊆ 𝑦 ) ) ) ) )
37 33 34 35 36 syl3anc ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑋 × { 𝐵 } ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ↔ ( ( 𝑋 × { 𝐵 } ) : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑦 ∈ 𝐾 ( ( ( 𝑋 × { 𝐵 } ) ‘ 𝑥 ) ∈ 𝑦 → ∃ 𝑢 ∈ 𝐽 ( 𝑥 ∈ 𝑢 ∧ ( ( 𝑋 × { 𝐵 } ) “ 𝑢 ) ⊆ 𝑦 ) ) ) ) )
38 3 32 37 mpbir2and ⊢ ( ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑋 × { 𝐵 } ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) )
39 38 ralrimiva ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) → ∀ 𝑥 ∈ 𝑋 ( 𝑋 × { 𝐵 } ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) )
40 cncnp ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 𝑋 × { 𝐵 } ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝑋 × { 𝐵 } ) : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑋 × { 𝐵 } ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) )
41 40 3adant3 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) → ( ( 𝑋 × { 𝐵 } ) ∈ ( 𝐽 Cn 𝐾 ) ↔ ( ( 𝑋 × { 𝐵 } ) : 𝑋 ⟶ 𝑌 ∧ ∀ 𝑥 ∈ 𝑋 ( 𝑋 × { 𝐵 } ) ∈ ( ( 𝐽 CnP 𝐾 ) ‘ 𝑥 ) ) ) )
42 2 39 41 mpbir2and ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ∧ 𝐵 ∈ 𝑌 ) → ( 𝑋 × { 𝐵 } ) ∈ ( 𝐽 Cn 𝐾 ) )