cnmpt1st

Description: The projection onto the first 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	cnmpt1st	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑌 ↦ 𝑥 ) ∈ ( ( 𝐽 ×_t 𝐾 ) Cn 𝐽 ) )

Proof

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

Metamath Proof Explorer

Theorem cnmpt1st

Proof