Theorem cnmpt2nd

Description: The projection onto the second coordinate is continuous. (Contributed by Mario Carneiro, 6-May-2014) (Revised by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	cnmpt21.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
	cnmpt21.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
Assertion	cnmpt2nd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑦 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐾 ) )

Proof

Step	Hyp	Ref	Expression
1		cnmpt21.j	⊢ ( 𝜑 → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2		cnmpt21.k	⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
3		fo2nd	⊢ 2nd : V –onto→ V
4		fofn	⊢ ( 2nd : V –onto→ V → 2nd Fn V )
5	3 4	ax-mp	⊢ 2nd Fn V
6		ssv	⊢ ( 𝑋 × 𝑌 ) ⊆ V
7		fnssres	⊢ ( ( 2nd Fn V ∧ ( 𝑋 × 𝑌 ) ⊆ V ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) )
8	5 6 7	mp2an	⊢ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 )
9		dffn5	⊢ ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) ↔ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) ) )
10	8 9	mpbi	⊢ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) )
11		fvres	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) = ( 2nd ‘ 𝑧 ) )
12	11	mpteq2ia	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) ) = ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2nd ‘ 𝑧 ) )
13		vex	⊢ 𝑥 ∈ V
14		vex	⊢ 𝑦 ∈ V
15	13 14	op2ndd	⊢ ( 𝑧 = ⟨ 𝑥 , 𝑦 ⟩ → ( 2nd ‘ 𝑧 ) = 𝑦 )
16	15	mpompt	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ↦ ( 2nd ‘ 𝑧 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑦 )
17	10 12 16	3eqtri	⊢ ( 2nd ↾ ( 𝑋 × 𝑌 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑦 )
18		tx2cn	⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝐾 ∈ ( TopOn ‘ 𝑌 ) ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐾 ) )
19	1 2 18	syl2anc	⊢ ( 𝜑 → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐾 ) )
20	17 19	eqeltrrid	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑦 ) ∈ ( ( 𝐽 ×t 𝐾 ) Cn 𝐾 ) )