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

Metamath Proof Explorer

Theorem txss12

Description: Subset property of the topological product. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion txss12 ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) ) → ( 𝐴 ×t 𝐶 ) ⊆ ( 𝐵 ×t 𝐷 ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) )
2 1 txbasex ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) ∈ V )
3 resmpo ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) ↾ ( 𝐴 × 𝐶 ) ) = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) )
4 resss ⊢ ( ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) ↾ ( 𝐴 × 𝐶 ) ) ⊆ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) )
5 3 4 eqsstrrdi ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ⊆ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) )
6 5 adantl ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ⊆ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) )
7 rnss ⊢ ( ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ⊆ ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) → ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ⊆ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) )
8 6 7 syl ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) ) → ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ⊆ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) )
9 tgss ⊢ ( ( ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) ∈ V ∧ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ⊆ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) ) → ( topGen ‘ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ) ⊆ ( topGen ‘ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) ) )
10 2 8 9 syl2an2r ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) ) → ( topGen ‘ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ) ⊆ ( topGen ‘ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) ) )
11 ssexg ⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) → 𝐴 ∈ V )
12 ssexg ⊢ ( ( 𝐶 ⊆ 𝐷 ∧ 𝐷 ∈ 𝑊 ) → 𝐶 ∈ V )
13 eqid ⊢ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) = ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) )
14 13 txval ⊢ ( ( 𝐴 ∈ V ∧ 𝐶 ∈ V ) → ( 𝐴 ×t 𝐶 ) = ( topGen ‘ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ) )
15 11 12 14 syl2an ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ⊆ 𝐷 ∧ 𝐷 ∈ 𝑊 ) ) → ( 𝐴 ×t 𝐶 ) = ( topGen ‘ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ) )
16 15 an4s ⊢ ( ( ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) ∧ ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ) → ( 𝐴 ×t 𝐶 ) = ( topGen ‘ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ) )
17 16 ancoms ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) ) → ( 𝐴 ×t 𝐶 ) = ( topGen ‘ ran ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐶 ↦ ( 𝑥 × 𝑦 ) ) ) )
18 1 txval ⊢ ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) → ( 𝐵 ×t 𝐷 ) = ( topGen ‘ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) ) )
19 18 adantr ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) ) → ( 𝐵 ×t 𝐷 ) = ( topGen ‘ ran ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐷 ↦ ( 𝑥 × 𝑦 ) ) ) )
20 10 17 19 3sstr4d ⊢ ( ( ( 𝐵 ∈ 𝑉 ∧ 𝐷 ∈ 𝑊 ) ∧ ( 𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷 ) ) → ( 𝐴 ×t 𝐶 ) ⊆ ( 𝐵 ×t 𝐷 ) )