Metamath Proof Explorer

Theorem txcn

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

Ref Expression
Hypotheses txcn.1 ⊢ 𝑋 = ∪ 𝑅
txcn.2 ⊢ 𝑌 = ∪ 𝑆
txcn.3 ⊢ 𝑍 = ( 𝑋 × 𝑌 )
txcn.4 ⊢ 𝑊 = ∪ 𝑈
txcn.5 ⊢ 𝑃 = ( 1st ↾ 𝑍 )
txcn.6 ⊢ 𝑄 = ( 2nd ↾ 𝑍 )
Assertion txcn ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) → ( 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ↔ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) )

Proof

Step Hyp Ref Expression
1 txcn.1 ⊢ 𝑋 = ∪ 𝑅
2 txcn.2 ⊢ 𝑌 = ∪ 𝑆
3 txcn.3 ⊢ 𝑍 = ( 𝑋 × 𝑌 )
4 txcn.4 ⊢ 𝑊 = ∪ 𝑈
5 txcn.5 ⊢ 𝑃 = ( 1st ↾ 𝑍 )
6 txcn.6 ⊢ 𝑄 = ( 2nd ↾ 𝑍 )
7 1 toptopon ⊢ ( 𝑅 ∈ Top ↔ 𝑅 ∈ ( TopOn ‘ 𝑋 ) )
8 2 toptopon ⊢ ( 𝑆 ∈ Top ↔ 𝑆 ∈ ( TopOn ‘ 𝑌 ) )
9 3 reseq2i ⊢ ( 1st ↾ 𝑍 ) = ( 1st ↾ ( 𝑋 × 𝑌 ) )
10 5 9 eqtri ⊢ 𝑃 = ( 1st ↾ ( 𝑋 × 𝑌 ) )
11 tx1cn ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) )
12 10 11 eqeltrid ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → 𝑃 ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) )
13 3 reseq2i ⊢ ( 2nd ↾ 𝑍 ) = ( 2nd ↾ ( 𝑋 × 𝑌 ) )
14 6 13 eqtri ⊢ 𝑄 = ( 2nd ↾ ( 𝑋 × 𝑌 ) )
15 tx2cn ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )
16 14 15 eqeltrid ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → 𝑄 ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) )
17 cnco ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ 𝑃 ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) ) → ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) )
18 cnco ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ 𝑄 ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) ) → ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) )
19 17 18 anim12dan ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( 𝑃 ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) ∧ 𝑄 ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) ) ) → ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) )
20 19 expcom ⊢ ( ( 𝑃 ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑅 ) ∧ 𝑄 ∈ ( ( 𝑅 ×t 𝑆 ) Cn 𝑆 ) ) → ( 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) → ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) )
21 12 16 20 syl2anc ⊢ ( ( 𝑅 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑆 ∈ ( TopOn ‘ 𝑌 ) ) → ( 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) → ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) )
22 7 8 21 syl2anb ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) → ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) )
23 22 3adant3 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) → ( 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) → ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) )
24 cntop1 ⊢ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) → 𝑈 ∈ Top )
25 24 ad2antrl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → 𝑈 ∈ Top )
26 4 topopn ⊢ ( 𝑈 ∈ Top → 𝑊 ∈ 𝑈 )
27 25 26 syl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → 𝑊 ∈ 𝑈 )
28 4 1 cnf ⊢ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) → ( 𝑃 ∘ 𝐹 ) : 𝑊 ⟶ 𝑋 )
29 28 ad2antrl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( 𝑃 ∘ 𝐹 ) : 𝑊 ⟶ 𝑋 )
30 4 2 cnf ⊢ ( ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) → ( 𝑄 ∘ 𝐹 ) : 𝑊 ⟶ 𝑌 )
31 30 ad2antll ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( 𝑄 ∘ 𝐹 ) : 𝑊 ⟶ 𝑌 )
32 10 14 upxp ⊢ ( ( 𝑊 ∈ 𝑈 ∧ ( 𝑃 ∘ 𝐹 ) : 𝑊 ⟶ 𝑋 ∧ ( 𝑄 ∘ 𝐹 ) : 𝑊 ⟶ 𝑌 ) → ∃! ℎ ( ℎ : 𝑊 ⟶ ( 𝑋 × 𝑌 ) ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
33 feq3 ⊢ ( 𝑍 = ( 𝑋 × 𝑌 ) → ( ℎ : 𝑊 ⟶ 𝑍 ↔ ℎ : 𝑊 ⟶ ( 𝑋 × 𝑌 ) ) )
34 3 33 ax-mp ⊢ ( ℎ : 𝑊 ⟶ 𝑍 ↔ ℎ : 𝑊 ⟶ ( 𝑋 × 𝑌 ) )
35 34 3anbi1i ⊢ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ↔ ( ℎ : 𝑊 ⟶ ( 𝑋 × 𝑌 ) ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
36 35 eubii ⊢ ( ∃! ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ↔ ∃! ℎ ( ℎ : 𝑊 ⟶ ( 𝑋 × 𝑌 ) ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
37 32 36 sylibr ⊢ ( ( 𝑊 ∈ 𝑈 ∧ ( 𝑃 ∘ 𝐹 ) : 𝑊 ⟶ 𝑋 ∧ ( 𝑄 ∘ 𝐹 ) : 𝑊 ⟶ 𝑌 ) → ∃! ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
38 27 29 31 37 syl3anc ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ∃! ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
39 euex ⊢ ( ∃! ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) → ∃ ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
40 38 39 syl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ∃ ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
41 simpll3 ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → 𝐹 : 𝑊 ⟶ 𝑍 )
42 27 adantr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → 𝑊 ∈ 𝑈 )
43 41 42 fexd ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → 𝐹 ∈ V )
44 eumo ⊢ ( ∃! ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) → ∃* ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
45 38 44 syl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ∃* ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
46 45 adantr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ∃* ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
47 simpr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
48 3anass ⊢ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ↔ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) )
49 coeq2 ⊢ ( 𝐹 = ℎ → ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) )
50 coeq2 ⊢ ( 𝐹 = ℎ → ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) )
51 49 50 jca ⊢ ( 𝐹 = ℎ → ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
52 51 eqcoms ⊢ ( ℎ = 𝐹 → ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
53 52 biantrud ⊢ ( ℎ = 𝐹 → ( ℎ : 𝑊 ⟶ 𝑍 ↔ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) ) )
54 feq1 ⊢ ( ℎ = 𝐹 → ( ℎ : 𝑊 ⟶ 𝑍 ↔ 𝐹 : 𝑊 ⟶ 𝑍 ) )
55 53 54 bitr3d ⊢ ( ℎ = 𝐹 → ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) ↔ 𝐹 : 𝑊 ⟶ 𝑍 ) )
56 48 55 syl5bb ⊢ ( ℎ = 𝐹 → ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ↔ 𝐹 : 𝑊 ⟶ 𝑍 ) )
57 56 moi2 ⊢ ( ( ( 𝐹 ∈ V ∧ ∃* ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) ∧ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ) → ℎ = 𝐹 )
58 43 46 47 41 57 syl22anc ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ℎ = 𝐹 )
59 eqid ⊢ ( 𝑅 ×t 𝑆 ) = ( 𝑅 ×t 𝑆 )
60 59 1 2 3 5 6 uptx ⊢ ( ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) → ∃! ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
61 60 adantl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ∃! ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
62 df-reu ⊢ ( ∃! ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ↔ ∃! ℎ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) )
63 euex ⊢ ( ∃! ℎ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ∃ ℎ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) )
64 62 63 sylbi ⊢ ( ∃! ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) → ∃ ℎ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) )
65 eqid ⊢ ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 )
66 4 65 cnf ⊢ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) → ℎ : 𝑊 ⟶ ∪ ( 𝑅 ×t 𝑆 ) )
67 1 2 txuni ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) )
68 3 67 syl5eq ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝑍 = ∪ ( 𝑅 ×t 𝑆 ) )
69 68 3adant3 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) → 𝑍 = ∪ ( 𝑅 ×t 𝑆 ) )
70 69 adantr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → 𝑍 = ∪ ( 𝑅 ×t 𝑆 ) )
71 70 feq3d ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ℎ : 𝑊 ⟶ 𝑍 ↔ ℎ : 𝑊 ⟶ ∪ ( 𝑅 ×t 𝑆 ) ) )
72 66 71 syl5ibr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) → ℎ : 𝑊 ⟶ 𝑍 ) )
73 72 anim1d ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) ) )
74 73 48 syl6ibr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) )
75 simpl ⊢ ( ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) )
76 74 75 jca2 ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) ) )
77 76 eximdv ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ∃ ℎ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ∃ ℎ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) ) )
78 64 77 syl5 ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ∃! ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) → ∃ ℎ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) ) )
79 61 78 mpd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ∃ ℎ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) )
80 eupick ⊢ ( ( ∃! ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ∃ ℎ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) ) → ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) → ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) )
81 38 79 80 syl2anc ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) → ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) )
82 81 imp ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) )
83 58 82 eqeltrrd ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) )
84 40 83 exlimddv ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) )
85 84 ex ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) → ( ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) → 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) )
86 23 85 impbid ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) → ( 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ↔ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) )