Metamath Proof Explorer

Theorem txrest

Description: The subspace of a topological product space induced by a subset with a Cartesian product representation is a topological product of the subspaces induced by the subspaces of the terms of the products. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 2-Sep-2015)

Ref Expression
Assertion txrest ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝐴 × 𝐵 ) ) = ( ( 𝑅 ↾t 𝐴 ) ×t ( 𝑆 ↾t 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 eqid ⊢ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) = ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) )
2 1 txval ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ) )
3 2 adantr ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ) )
4 3 oveq1d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝐴 × 𝐵 ) ) = ( ( topGen ‘ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ) ↾t ( 𝐴 × 𝐵 ) ) )
5 1 txbasex ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) → ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ∈ V )
6 xpexg ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) → ( 𝐴 × 𝐵 ) ∈ V )
7 tgrest ⊢ ( ( ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ∈ V ∧ ( 𝐴 × 𝐵 ) ∈ V ) → ( topGen ‘ ( ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ↾t ( 𝐴 × 𝐵 ) ) ) = ( ( topGen ‘ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ) ↾t ( 𝐴 × 𝐵 ) ) )
8 5 6 7 syl2an ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( topGen ‘ ( ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ↾t ( 𝐴 × 𝐵 ) ) ) = ( ( topGen ‘ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ) ↾t ( 𝐴 × 𝐵 ) ) )
9 elrest ⊢ ( ( ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ∈ V ∧ ( 𝐴 × 𝐵 ) ∈ V ) → ( 𝑥 ∈ ( ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ↾t ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑤 ∈ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) 𝑥 = ( 𝑤 ∩ ( 𝐴 × 𝐵 ) ) ) )
10 5 6 9 syl2an ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑥 ∈ ( ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ↾t ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑤 ∈ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) 𝑥 = ( 𝑤 ∩ ( 𝐴 × 𝐵 ) ) ) )
11 vex ⊢ 𝑟 ∈ V
12 11 inex1 ⊢ ( 𝑟 ∩ 𝐴 ) ∈ V
13 12 a1i ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝑟 ∈ 𝑅 ) → ( 𝑟 ∩ 𝐴 ) ∈ V )
14 elrest ⊢ ( ( 𝑅 ∈ 𝑉 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) ↔ ∃ 𝑟 ∈ 𝑅 𝑢 = ( 𝑟 ∩ 𝐴 ) ) )
15 14 ad2ant2r ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) ↔ ∃ 𝑟 ∈ 𝑅 𝑢 = ( 𝑟 ∩ 𝐴 ) ) )
16 xpeq1 ⊢ ( 𝑢 = ( 𝑟 ∩ 𝐴 ) → ( 𝑢 × 𝑣 ) = ( ( 𝑟 ∩ 𝐴 ) × 𝑣 ) )
17 16 eqeq2d ⊢ ( 𝑢 = ( 𝑟 ∩ 𝐴 ) → ( 𝑥 = ( 𝑢 × 𝑣 ) ↔ 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × 𝑣 ) ) )
18 17 rexbidv ⊢ ( 𝑢 = ( 𝑟 ∩ 𝐴 ) → ( ∃ 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) 𝑥 = ( 𝑢 × 𝑣 ) ↔ ∃ 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × 𝑣 ) ) )
19 vex ⊢ 𝑠 ∈ V
20 19 inex1 ⊢ ( 𝑠 ∩ 𝐵 ) ∈ V
21 20 a1i ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝑠 ∈ 𝑆 ) → ( 𝑠 ∩ 𝐵 ) ∈ V )
22 elrest ⊢ ( ( 𝑆 ∈ 𝑊 ∧ 𝐵 ∈ 𝑌 ) → ( 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↔ ∃ 𝑠 ∈ 𝑆 𝑣 = ( 𝑠 ∩ 𝐵 ) ) )
23 22 ad2ant2l ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↔ ∃ 𝑠 ∈ 𝑆 𝑣 = ( 𝑠 ∩ 𝐵 ) ) )
24 xpeq2 ⊢ ( 𝑣 = ( 𝑠 ∩ 𝐵 ) → ( ( 𝑟 ∩ 𝐴 ) × 𝑣 ) = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) ) )
25 24 eqeq2d ⊢ ( 𝑣 = ( 𝑠 ∩ 𝐵 ) → ( 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × 𝑣 ) ↔ 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) ) ) )
26 25 adantl ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝑣 = ( 𝑠 ∩ 𝐵 ) ) → ( 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × 𝑣 ) ↔ 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) ) ) )
27 21 23 26 rexxfr2d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ∃ 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × 𝑣 ) ↔ ∃ 𝑠 ∈ 𝑆 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) ) ) )
28 18 27 sylan9bbr ⊢ ( ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) ∧ 𝑢 = ( 𝑟 ∩ 𝐴 ) ) → ( ∃ 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) 𝑥 = ( 𝑢 × 𝑣 ) ↔ ∃ 𝑠 ∈ 𝑆 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) ) ) )
29 13 15 28 rexxfr2d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ∃ 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) ∃ 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) 𝑥 = ( 𝑢 × 𝑣 ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) ) ) )
30 11 19 xpex ⊢ ( 𝑟 × 𝑠 ) ∈ V
31 30 rgen2w ⊢ ∀ 𝑟 ∈ 𝑅 ∀ 𝑠 ∈ 𝑆 ( 𝑟 × 𝑠 ) ∈ V
32 eqid ⊢ ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) = ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) )
33 ineq1 ⊢ ( 𝑤 = ( 𝑟 × 𝑠 ) → ( 𝑤 ∩ ( 𝐴 × 𝐵 ) ) = ( ( 𝑟 × 𝑠 ) ∩ ( 𝐴 × 𝐵 ) ) )
34 inxp ⊢ ( ( 𝑟 × 𝑠 ) ∩ ( 𝐴 × 𝐵 ) ) = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) )
35 33 34 eqtrdi ⊢ ( 𝑤 = ( 𝑟 × 𝑠 ) → ( 𝑤 ∩ ( 𝐴 × 𝐵 ) ) = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) ) )
36 35 eqeq2d ⊢ ( 𝑤 = ( 𝑟 × 𝑠 ) → ( 𝑥 = ( 𝑤 ∩ ( 𝐴 × 𝐵 ) ) ↔ 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) ) ) )
37 32 36 rexrnmpo ⊢ ( ∀ 𝑟 ∈ 𝑅 ∀ 𝑠 ∈ 𝑆 ( 𝑟 × 𝑠 ) ∈ V → ( ∃ 𝑤 ∈ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) 𝑥 = ( 𝑤 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) ) ) )
38 31 37 ax-mp ⊢ ( ∃ 𝑤 ∈ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) 𝑥 = ( 𝑤 ∩ ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑟 ∈ 𝑅 ∃ 𝑠 ∈ 𝑆 𝑥 = ( ( 𝑟 ∩ 𝐴 ) × ( 𝑠 ∩ 𝐵 ) ) )
39 29 38 bitr4di ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ∃ 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) ∃ 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) 𝑥 = ( 𝑢 × 𝑣 ) ↔ ∃ 𝑤 ∈ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) 𝑥 = ( 𝑤 ∩ ( 𝐴 × 𝐵 ) ) ) )
40 10 39 bitr4d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( 𝑥 ∈ ( ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ↾t ( 𝐴 × 𝐵 ) ) ↔ ∃ 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) ∃ 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) 𝑥 = ( 𝑢 × 𝑣 ) ) )
41 40 abbi2dv ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ↾t ( 𝐴 × 𝐵 ) ) = { 𝑥 ∣ ∃ 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) ∃ 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) 𝑥 = ( 𝑢 × 𝑣 ) } )
42 eqid ⊢ ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) , 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↦ ( 𝑢 × 𝑣 ) ) = ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) , 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↦ ( 𝑢 × 𝑣 ) )
43 42 rnmpo ⊢ ran ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) , 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↦ ( 𝑢 × 𝑣 ) ) = { 𝑥 ∣ ∃ 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) ∃ 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) 𝑥 = ( 𝑢 × 𝑣 ) }
44 41 43 eqtr4di ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ↾t ( 𝐴 × 𝐵 ) ) = ran ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) , 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↦ ( 𝑢 × 𝑣 ) ) )
45 44 fveq2d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( topGen ‘ ( ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ↾t ( 𝐴 × 𝐵 ) ) ) = ( topGen ‘ ran ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) , 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↦ ( 𝑢 × 𝑣 ) ) ) )
46 4 8 45 3eqtr2d ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝐴 × 𝐵 ) ) = ( topGen ‘ ran ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) , 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↦ ( 𝑢 × 𝑣 ) ) ) )
47 ovex ⊢ ( 𝑅 ↾t 𝐴 ) ∈ V
48 ovex ⊢ ( 𝑆 ↾t 𝐵 ) ∈ V
49 eqid ⊢ ran ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) , 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↦ ( 𝑢 × 𝑣 ) ) = ran ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) , 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↦ ( 𝑢 × 𝑣 ) )
50 49 txval ⊢ ( ( ( 𝑅 ↾t 𝐴 ) ∈ V ∧ ( 𝑆 ↾t 𝐵 ) ∈ V ) → ( ( 𝑅 ↾t 𝐴 ) ×t ( 𝑆 ↾t 𝐵 ) ) = ( topGen ‘ ran ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) , 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↦ ( 𝑢 × 𝑣 ) ) ) )
51 47 48 50 mp2an ⊢ ( ( 𝑅 ↾t 𝐴 ) ×t ( 𝑆 ↾t 𝐵 ) ) = ( topGen ‘ ran ( 𝑢 ∈ ( 𝑅 ↾t 𝐴 ) , 𝑣 ∈ ( 𝑆 ↾t 𝐵 ) ↦ ( 𝑢 × 𝑣 ) ) )
52 46 51 eqtr4di ⊢ ( ( ( 𝑅 ∈ 𝑉 ∧ 𝑆 ∈ 𝑊 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑌 ) ) → ( ( 𝑅 ×t 𝑆 ) ↾t ( 𝐴 × 𝐵 ) ) = ( ( 𝑅 ↾t 𝐴 ) ×t ( 𝑆 ↾t 𝐵 ) ) )