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 1 topopn ⊢ ( 𝑅 ∈ Top → 𝑋 ∈ 𝑅 )
44 2 topopn ⊢ ( 𝑆 ∈ Top → 𝑌 ∈ 𝑆 )
45 xpexg ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑆 ) → ( 𝑋 × 𝑌 ) ∈ V )
46 3 45 eqeltrid ⊢ ( ( 𝑋 ∈ 𝑅 ∧ 𝑌 ∈ 𝑆 ) → 𝑍 ∈ V )
47 43 44 46 syl2an ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝑍 ∈ V )
48 47 3adant3 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) → 𝑍 ∈ V )
49 48 ad2antrr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → 𝑍 ∈ V )
50 fex2 ⊢ ( ( 𝐹 : 𝑊 ⟶ 𝑍 ∧ 𝑊 ∈ 𝑈 ∧ 𝑍 ∈ V ) → 𝐹 ∈ V )
51 41 42 49 50 syl3anc ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → 𝐹 ∈ V )
52 eumo ⊢ ( ∃! ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) → ∃* ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
53 38 52 syl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ∃* ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
54 53 adantr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ∃* ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
55 simpr ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
56 3anass ⊢ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ↔ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) )
57 coeq2 ⊢ ( 𝐹 = ℎ → ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) )
58 coeq2 ⊢ ( 𝐹 = ℎ → ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) )
59 57 58 jca ⊢ ( 𝐹 = ℎ → ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
60 59 eqcoms ⊢ ( ℎ = 𝐹 → ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
61 60 biantrud ⊢ ( ℎ = 𝐹 → ( ℎ : 𝑊 ⟶ 𝑍 ↔ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) ) )
62 feq1 ⊢ ( ℎ = 𝐹 → ( ℎ : 𝑊 ⟶ 𝑍 ↔ 𝐹 : 𝑊 ⟶ 𝑍 ) )
63 61 62 bitr3d ⊢ ( ℎ = 𝐹 → ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) ↔ 𝐹 : 𝑊 ⟶ 𝑍 ) )
64 56 63 syl5bb ⊢ ( ℎ = 𝐹 → ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ↔ 𝐹 : 𝑊 ⟶ 𝑍 ) )
65 64 moi2 ⊢ ( ( ( 𝐹 ∈ V ∧ ∃* ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) ∧ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ) → ℎ = 𝐹 )
66 51 54 55 41 65 syl22anc ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ℎ = 𝐹 )
67 eqid ⊢ ( 𝑅 ×t 𝑆 ) = ( 𝑅 ×t 𝑆 )
68 67 1 2 3 5 6 uptx ⊢ ( ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) → ∃! ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
69 68 adantl ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ∃! ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) )
70 df-reu ⊢ ( ∃! ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ↔ ∃! ℎ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) )
71 euex ⊢ ( ∃! ℎ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ∃ ℎ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) )
72 70 71 sylbi ⊢ ( ∃! ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) → ∃ ℎ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) )
73 eqid ⊢ ∪ ( 𝑅 ×t 𝑆 ) = ∪ ( 𝑅 ×t 𝑆 )
74 4 73 cnf ⊢ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) → ℎ : 𝑊 ⟶ ∪ ( 𝑅 ×t 𝑆 ) )
75 1 2 txuni ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×t 𝑆 ) )
76 3 75 syl5eq ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝑍 = ∪ ( 𝑅 ×t 𝑆 ) )
77 76 3adant3 ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) → 𝑍 = ∪ ( 𝑅 ×t 𝑆 ) )
78 77 adantr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → 𝑍 = ∪ ( 𝑅 ×t 𝑆 ) )
79 78 feq3d ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ℎ : 𝑊 ⟶ 𝑍 ↔ ℎ : 𝑊 ⟶ ∪ ( 𝑅 ×t 𝑆 ) ) )
80 74 79 syl5ibr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) → ℎ : 𝑊 ⟶ 𝑍 ) )
81 80 anim1d ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) ) )
82 81 56 syl6ibr ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) )
83 simpl ⊢ ( ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) )
84 82 83 jca2 ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) ) )
85 84 eximdv ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ∃ ℎ ( ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ∧ ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ∃ ℎ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) ) )
86 72 85 syl5 ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ∃! ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ( ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) → ∃ ℎ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) ) )
87 69 86 mpd ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ∃ ℎ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) )
88 eupick ⊢ ( ( ∃! ℎ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ∃ ℎ ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ∧ ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) ) → ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) → ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) )
89 38 87 88 syl2anc ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → ( ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) → ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) )
90 89 imp ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → ℎ ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) )
91 66 90 eqeltrrd ⊢ ( ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) ∧ ( ℎ : 𝑊 ⟶ 𝑍 ∧ ( 𝑃 ∘ 𝐹 ) = ( 𝑃 ∘ ℎ ) ∧ ( 𝑄 ∘ 𝐹 ) = ( 𝑄 ∘ ℎ ) ) ) → 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) )
92 40 91 exlimddv ⊢ ( ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) ∧ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) → 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) )
93 92 ex ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) → ( ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) → 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ) )
94 23 93 impbid ⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ∧ 𝐹 : 𝑊 ⟶ 𝑍 ) → ( 𝐹 ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) ↔ ( ( 𝑃 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑅 ) ∧ ( 𝑄 ∘ 𝐹 ) ∈ ( 𝑈 Cn 𝑆 ) ) ) )