Theorem tx2cn

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

	Ref	Expression
Assertion	tx2cn	⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )

Proof

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