tx1cn

Description: Continuity of the first projection map of a topological product. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)

		Ref	Expression
	Assertion	tx1cn	⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×_t 𝑆 ) Cn 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		f1stres	⊢ ( 1^st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑋
2	1	a1i	⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 1^st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑋 )
3		ffn	⊢ ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑋 → ( 1^st ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) )
4		elpreima	⊢ ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) → ( 𝑧 ∈ ( ^◡ ( 1^st ↾ ( 𝑋 × 𝑌 ) ) “ 𝑤 ) ↔ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ∧ ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) ∈ 𝑤 ) ) )
5	1 3 4	mp2b	⊢ ( 𝑧 ∈ ( ^◡ ( 1^st ↾ ( 𝑋 × 𝑌 ) ) “ 𝑤 ) ↔ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ∧ ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) ∈ 𝑤 ) )
6		fvres	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) = ( 1^st ‘ 𝑧 ) )
7	6	eleq1d	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) ∈ 𝑤 ↔ ( 1^st ‘ 𝑧 ) ∈ 𝑤 ) )
8		1st2nd2	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ )
9		xp2nd	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( 2^nd ‘ 𝑧 ) ∈ 𝑌 )
10		elxp6	⊢ ( 𝑧 ∈ ( 𝑤 × 𝑌 ) ↔ ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( ( 1^st ‘ 𝑧 ) ∈ 𝑤 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑌 ) ) )
11		anass	⊢ ( ( ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( 1^st ‘ 𝑧 ) ∈ 𝑤 ) ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑌 ) ↔ ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( ( 1^st ‘ 𝑧 ) ∈ 𝑤 ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑌 ) ) )
12		an32	⊢ ( ( ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( 1^st ‘ 𝑧 ) ∈ 𝑤 ) ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑌 ) ↔ ( ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑌 ) ∧ ( 1^st ‘ 𝑧 ) ∈ 𝑤 ) )
13	10 11 12	3bitr2i	⊢ ( 𝑧 ∈ ( 𝑤 × 𝑌 ) ↔ ( ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑌 ) ∧ ( 1^st ‘ 𝑧 ) ∈ 𝑤 ) )
14	13	baib	⊢ ( ( 𝑧 = ⟨ ( 1^st ‘ 𝑧 ) , ( 2^nd ‘ 𝑧 ) ⟩ ∧ ( 2^nd ‘ 𝑧 ) ∈ 𝑌 ) → ( 𝑧 ∈ ( 𝑤 × 𝑌 ) ↔ ( 1^st ‘ 𝑧 ) ∈ 𝑤 ) )
15	8 9 14	syl2anc	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( 𝑧 ∈ ( 𝑤 × 𝑌 ) ↔ ( 1^st ‘ 𝑧 ) ∈ 𝑤 ) )
16	7 15	bitr4d	⊢ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) → ( ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) ∈ 𝑤 ↔ 𝑧 ∈ ( 𝑤 × 𝑌 ) ) )
17	16	pm5.32i	⊢ ( ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ∧ ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ 𝑧 ) ∈ 𝑤 ) ↔ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ( 𝑤 × 𝑌 ) ) )
18	5 17	bitri	⊢ ( 𝑧 ∈ ( ^◡ ( 1^st ↾ ( 𝑋 × 𝑌 ) ) “ 𝑤 ) ↔ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ( 𝑤 × 𝑌 ) ) )
19		toponss	⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑤 ∈ 𝑅 ) → 𝑤 ⊆ 𝑋 )
20	19	adantlr	⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑤 ∈ 𝑅 ) → 𝑤 ⊆ 𝑋 )
21		xpss1	⊢ ( 𝑤 ⊆ 𝑋 → ( 𝑤 × 𝑌 ) ⊆ ( 𝑋 × 𝑌 ) )
22	20 21	syl	⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑤 ∈ 𝑅 ) → ( 𝑤 × 𝑌 ) ⊆ ( 𝑋 × 𝑌 ) )
23	22	sseld	⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑤 ∈ 𝑅 ) → ( 𝑧 ∈ ( 𝑤 × 𝑌 ) → 𝑧 ∈ ( 𝑋 × 𝑌 ) ) )
24	23	pm4.71rd	⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑤 ∈ 𝑅 ) → ( 𝑧 ∈ ( 𝑤 × 𝑌 ) ↔ ( 𝑧 ∈ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ( 𝑤 × 𝑌 ) ) ) )
25	18 24	bitr4id	⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑤 ∈ 𝑅 ) → ( 𝑧 ∈ ( ^◡ ( 1^st ↾ ( 𝑋 × 𝑌 ) ) “ 𝑤 ) ↔ 𝑧 ∈ ( 𝑤 × 𝑌 ) ) )
26	25	eqrdv	⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑤 ∈ 𝑅 ) → ( ^◡ ( 1^st ↾ ( 𝑋 × 𝑌 ) ) “ 𝑤 ) = ( 𝑤 × 𝑌 ) )
27		toponmax	⊢ ( 𝑆 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 ∈ 𝑆 )
28	27	ad2antlr	⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑤 ∈ 𝑅 ) → 𝑌 ∈ 𝑆 )
29		txopn	⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ ( 𝑤 ∈ 𝑅 ∧ 𝑌 ∈ 𝑆 ) ) → ( 𝑤 × 𝑌 ) ∈ ( 𝑅 ×_t 𝑆 ) )
30	29	anassrs	⊢ ( ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑤 ∈ 𝑅 ) ∧ 𝑌 ∈ 𝑆 ) → ( 𝑤 × 𝑌 ) ∈ ( 𝑅 ×_t 𝑆 ) )
31	28 30	mpdan	⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑤 ∈ 𝑅 ) → ( 𝑤 × 𝑌 ) ∈ ( 𝑅 ×_t 𝑆 ) )
32	26 31	eqeltrd	⊢ ( ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) ∧ 𝑤 ∈ 𝑅 ) → ( ^◡ ( 1^st ↾ ( 𝑋 × 𝑌 ) ) “ 𝑤 ) ∈ ( 𝑅 ×_t 𝑆 ) )
33	32	ralrimiva	⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ∀ 𝑤 ∈ 𝑅 ( ^◡ ( 1^st ↾ ( 𝑋 × 𝑌 ) ) “ 𝑤 ) ∈ ( 𝑅 ×_t 𝑆 ) )
34		txtopon	⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝑅 ×_t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) )
35		simpl	⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
36		iscn	⊢ ( ( ( 𝑅 ×_t 𝑆 ) ∈ ( TopOn ‘ ( 𝑋 × 𝑌 ) ) ∧ 𝑅 ∈ ( TopOn ‘ 𝑋 ) ) → ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×_t 𝑆 ) Cn 𝑅 ) ↔ ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑋 ∧ ∀ 𝑤 ∈ 𝑅 ( ^◡ ( 1^st ↾ ( 𝑋 × 𝑌 ) ) “ 𝑤 ) ∈ ( 𝑅 ×_t 𝑆 ) ) ) )
37	34 35 36	syl2anc	⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×_t 𝑆 ) Cn 𝑅 ) ↔ ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) : ( 𝑋 × 𝑌 ) ⟶ 𝑋 ∧ ∀ 𝑤 ∈ 𝑅 ( ^◡ ( 1^st ↾ ( 𝑋 × 𝑌 ) ) “ 𝑤 ) ∈ ( 𝑅 ×_t 𝑆 ) ) ) )
38	2 33 37	mpbir2and	⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×_t 𝑆 ) Cn 𝑅 ) )

Metamath Proof Explorer

Theorem tx1cn

Proof