Metamath Proof Explorer

Theorem txcnmpt

Description: A map into the product of two topological spaces is continuous if both of its projections are continuous. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses txcnmpt.1 ⊢ 𝑊 = ∪ 𝑈
txcnmpt.2 ⊢ 𝐻 = ( 𝑥 ∈ 𝑊 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
Assertion txcnmpt ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝐻 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 txcnmpt.1 ⊢ 𝑊 = ∪ 𝑈
2 txcnmpt.2 ⊢ 𝐻 = ( 𝑥 ∈ 𝑊 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
3 eqid ⊢ ∪ 𝑅 = ∪ 𝑅
4 1 3 cnf ⊢ ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) → 𝐹 : 𝑊 ⟶ ∪ 𝑅 )
5 4 adantr ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝐹 : 𝑊 ⟶ ∪ 𝑅 )
6 5 ffvelrnda ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝐹 ‘ 𝑥 ) ∈ ∪ 𝑅 )
7 eqid ⊢ ∪ 𝑆 = ∪ 𝑆
8 1 7 cnf ⊢ ( 𝐺 ∈ ( 𝑈 Cn 𝑆 ) → 𝐺 : 𝑊 ⟶ ∪ 𝑆 )
9 8 adantl ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝐺 : 𝑊 ⟶ ∪ 𝑆 )
10 9 ffvelrnda ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝐺 ‘ 𝑥 ) ∈ ∪ 𝑆 )
11 6 10 opelxpd ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( ∪ 𝑅 × ∪ 𝑆 ) )
12 11 2 fmptd ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝐻 : 𝑊 ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) )
13 2 mptpreima ⊢ ( ◡ 𝐻 “ ( 𝑟 × 𝑠 ) ) = { 𝑥 ∈ 𝑊 ∣ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝑟 × 𝑠 ) }
14 5 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝐹 : 𝑊 ⟶ ∪ 𝑅 )
15 14 adantr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → 𝐹 : 𝑊 ⟶ ∪ 𝑅 )
16 ffn ⊢ ( 𝐹 : 𝑊 ⟶ ∪ 𝑅 → 𝐹 Fn 𝑊 )
17 elpreima ⊢ ( 𝐹 Fn 𝑊 → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑟 ) ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑟 ) ) )
18 15 16 17 3syl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑟 ) ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑟 ) ) )
19 ibar ⊢ ( 𝑥 ∈ 𝑊 → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑟 ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑟 ) ) )
20 19 adantl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑟 ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝐹 ‘ 𝑥 ) ∈ 𝑟 ) ) )
21 18 20 bitr4d ⊢ ( ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑟 ) ↔ ( 𝐹 ‘ 𝑥 ) ∈ 𝑟 ) )
22 9 ad2antrr ⊢ ( ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → 𝐺 : 𝑊 ⟶ ∪ 𝑆 )
23 ffn ⊢ ( 𝐺 : 𝑊 ⟶ ∪ 𝑆 → 𝐺 Fn 𝑊 )
24 elpreima ⊢ ( 𝐺 Fn 𝑊 → ( 𝑥 ∈ ( ◡ 𝐺 “ 𝑠 ) ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝑠 ) ) )
25 22 23 24 3syl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝑥 ∈ ( ◡ 𝐺 “ 𝑠 ) ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝑠 ) ) )
26 ibar ⊢ ( 𝑥 ∈ 𝑊 → ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑠 ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝑠 ) ) )
27 26 adantl ⊢ ( ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → ( ( 𝐺 ‘ 𝑥 ) ∈ 𝑠 ↔ ( 𝑥 ∈ 𝑊 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝑠 ) ) )
28 25 27 bitr4d ⊢ ( ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝑥 ∈ ( ◡ 𝐺 “ 𝑠 ) ↔ ( 𝐺 ‘ 𝑥 ) ∈ 𝑠 ) )
29 21 28 anbi12d ⊢ ( ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → ( ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑟 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ 𝑠 ) ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑟 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝑠 ) ) )
30 elin ⊢ ( 𝑥 ∈ ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) ↔ ( 𝑥 ∈ ( ◡ 𝐹 “ 𝑟 ) ∧ 𝑥 ∈ ( ◡ 𝐺 “ 𝑠 ) ) )
31 opelxp ⊢ ( ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ↔ ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑟 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝑠 ) )
32 29 30 31 3bitr4g ⊢ ( ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) ∧ 𝑥 ∈ 𝑊 ) → ( 𝑥 ∈ ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) ↔ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝑟 × 𝑠 ) ) )
33 32 rabbi2dva ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝑊 ∩ ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) ) = { 𝑥 ∈ 𝑊 ∣ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝑟 × 𝑠 ) } )
34 inss1 ⊢ ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) ⊆ ( ◡ 𝐹 “ 𝑟 )
35 cnvimass ⊢ ( ◡ 𝐹 “ 𝑟 ) ⊆ dom 𝐹
36 34 35 sstri ⊢ ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) ⊆ dom 𝐹
37 36 14 fssdm ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) ⊆ 𝑊 )
38 sseqin2 ⊢ ( ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) ⊆ 𝑊 ↔ ( 𝑊 ∩ ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) ) = ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) )
39 37 38 sylib ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( 𝑊 ∩ ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) ) = ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) )
40 33 39 eqtr3d ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → { 𝑥 ∈ 𝑊 ∣ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝑟 × 𝑠 ) } = ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) )
41 13 40 syl5eq ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ◡ 𝐻 “ ( 𝑟 × 𝑠 ) ) = ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) )
42 cntop1 ⊢ ( 𝐺 ∈ ( 𝑈 Cn 𝑆 ) → 𝑈 ∈ Top )
43 42 adantl ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝑈 ∈ Top )
44 43 adantr ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → 𝑈 ∈ Top )
45 cnima ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝑟 ∈ 𝑅 ) → ( ◡ 𝐹 “ 𝑟 ) ∈ 𝑈 )
46 45 ad2ant2r ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ◡ 𝐹 “ 𝑟 ) ∈ 𝑈 )
47 cnima ⊢ ( ( 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ∧ 𝑠 ∈ 𝑆 ) → ( ◡ 𝐺 “ 𝑠 ) ∈ 𝑈 )
48 47 ad2ant2l ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ◡ 𝐺 “ 𝑠 ) ∈ 𝑈 )
49 inopn ⊢ ( ( 𝑈 ∈ Top ∧ ( ◡ 𝐹 “ 𝑟 ) ∈ 𝑈 ∧ ( ◡ 𝐺 “ 𝑠 ) ∈ 𝑈 ) → ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) ∈ 𝑈 )
50 44 46 48 49 syl3anc ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ( ◡ 𝐹 “ 𝑟 ) ∩ ( ◡ 𝐺 “ 𝑠 ) ) ∈ 𝑈 )
51 41 50 eqeltrd ⊢ ( ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) ∧ ( 𝑟 ∈ 𝑅 ∧ 𝑠 ∈ 𝑆 ) ) → ( ◡ 𝐻 “ ( 𝑟 × 𝑠 ) ) ∈ 𝑈 )
52 51 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∀ 𝑟 ∈ 𝑅 ∀ 𝑠 ∈ 𝑆 ( ◡ 𝐻 “ ( 𝑟 × 𝑠 ) ) ∈ 𝑈 )
53 vex ⊢ 𝑟 ∈ V
54 vex ⊢ 𝑠 ∈ V
55 53 54 xpex ⊢ ( 𝑟 × 𝑠 ) ∈ V
56 55 rgen2w ⊢ ∀ 𝑟 ∈ 𝑅 ∀ 𝑠 ∈ 𝑆 ( 𝑟 × 𝑠 ) ∈ V
57 eqid ⊢ ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) = ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) )
58 imaeq2 ⊢ ( 𝑧 = ( 𝑟 × 𝑠 ) → ( ◡ 𝐻 “ 𝑧 ) = ( ◡ 𝐻 “ ( 𝑟 × 𝑠 ) ) )
59 58 eleq1d ⊢ ( 𝑧 = ( 𝑟 × 𝑠 ) → ( ( ◡ 𝐻 “ 𝑧 ) ∈ 𝑈 ↔ ( ◡ 𝐻 “ ( 𝑟 × 𝑠 ) ) ∈ 𝑈 ) )
60 57 59 ralrnmpo ⊢ ( ∀ 𝑟 ∈ 𝑅 ∀ 𝑠 ∈ 𝑆 ( 𝑟 × 𝑠 ) ∈ V → ( ∀ 𝑧 ∈ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ( ◡ 𝐻 “ 𝑧 ) ∈ 𝑈 ↔ ∀ 𝑟 ∈ 𝑅 ∀ 𝑠 ∈ 𝑆 ( ◡ 𝐻 “ ( 𝑟 × 𝑠 ) ) ∈ 𝑈 ) )
61 56 60 ax-mp ⊢ ( ∀ 𝑧 ∈ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ( ◡ 𝐻 “ 𝑧 ) ∈ 𝑈 ↔ ∀ 𝑟 ∈ 𝑅 ∀ 𝑠 ∈ 𝑆 ( ◡ 𝐻 “ ( 𝑟 × 𝑠 ) ) ∈ 𝑈 )
62 52 61 sylibr ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∀ 𝑧 ∈ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ( ◡ 𝐻 “ 𝑧 ) ∈ 𝑈 )
63 1 toptopon ⊢ ( 𝑈 ∈ Top ↔ 𝑈 ∈ ( TopOn ‘ 𝑊 ) )
64 43 63 sylib ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝑈 ∈ ( TopOn ‘ 𝑊 ) )
65 cntop2 ⊢ ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) → 𝑅 ∈ Top )
66 cntop2 ⊢ ( 𝐺 ∈ ( 𝑈 Cn 𝑆 ) → 𝑆 ∈ Top )
67 eqid ⊢ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) = ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) )
68 67 txval ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ) )
69 65 66 68 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( 𝑅 ×t 𝑆 ) = ( topGen ‘ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ) )
70 toptopon2 ⊢ ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) )
71 65 70 sylib ⊢ ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) → 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) )
72 toptopon2 ⊢ ( 𝑆 ∈ Top ↔ 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) )
73 66 72 sylib ⊢ ( 𝐺 ∈ ( 𝑈 Cn 𝑆 ) → 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) )
74 txtopon ⊢ ( ( 𝑅 ∈ ( TopOn ‘ ∪ 𝑅 ) ∧ 𝑆 ∈ ( TopOn ‘ ∪ 𝑆 ) ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( ∪ 𝑅 × ∪ 𝑆 ) ) )
75 71 73 74 syl2an ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( 𝑅 ×t 𝑆 ) ∈ ( TopOn ‘ ( ∪ 𝑅 × ∪ 𝑆 ) ) )
76 64 69 75 tgcn ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( 𝐻 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ↔ ( 𝐻 : 𝑊 ⟶ ( ∪ 𝑅 × ∪ 𝑆 ) ∧ ∀ 𝑧 ∈ ran ( 𝑟 ∈ 𝑅 , 𝑠 ∈ 𝑆 ↦ ( 𝑟 × 𝑠 ) ) ( ◡ 𝐻 “ 𝑧 ) ∈ 𝑈 ) ) )
77 12 62 76 mpbir2and ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝐻 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) )