This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑆 ) )