Metamath Proof Explorer


Theorem uptx

Description: Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)

Ref Expression
Hypotheses uptx.1 𝑇 = ( 𝑅 ×t 𝑆 )
uptx.2 𝑋 = 𝑅
uptx.3 𝑌 = 𝑆
uptx.4 𝑍 = ( 𝑋 × 𝑌 )
uptx.5 𝑃 = ( 1st𝑍 )
uptx.6 𝑄 = ( 2nd𝑍 )
Assertion uptx ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃! ∈ ( 𝑈 Cn 𝑇 ) ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) )

Proof

Step Hyp Ref Expression
1 uptx.1 𝑇 = ( 𝑅 ×t 𝑆 )
2 uptx.2 𝑋 = 𝑅
3 uptx.3 𝑌 = 𝑆
4 uptx.4 𝑍 = ( 𝑋 × 𝑌 )
5 uptx.5 𝑃 = ( 1st𝑍 )
6 uptx.6 𝑄 = ( 2nd𝑍 )
7 eqid 𝑈 = 𝑈
8 eqid ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) = ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ )
9 7 8 txcnmpt ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ∈ ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) ) )
10 1 oveq2i ( 𝑈 Cn 𝑇 ) = ( 𝑈 Cn ( 𝑅 ×t 𝑆 ) )
11 9 10 eleqtrrdi ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) )
12 7 2 cnf ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) → 𝐹 : 𝑈𝑋 )
13 7 3 cnf ( 𝐺 ∈ ( 𝑈 Cn 𝑆 ) → 𝐺 : 𝑈𝑌 )
14 ffn ( 𝐹 : 𝑈𝑋𝐹 Fn 𝑈 )
15 14 adantr ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → 𝐹 Fn 𝑈 )
16 fo1st 1st : V –onto→ V
17 fofn ( 1st : V –onto→ V → 1st Fn V )
18 16 17 ax-mp 1st Fn V
19 ssv ( 𝑋 × 𝑌 ) ⊆ V
20 fnssres ( ( 1st Fn V ∧ ( 𝑋 × 𝑌 ) ⊆ V ) → ( 1st ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) )
21 18 19 20 mp2an ( 1st ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 )
22 ffvelrn ( ( 𝐹 : 𝑈𝑋𝑥 𝑈 ) → ( 𝐹𝑥 ) ∈ 𝑋 )
23 ffvelrn ( ( 𝐺 : 𝑈𝑌𝑥 𝑈 ) → ( 𝐺𝑥 ) ∈ 𝑌 )
24 opelxpi ( ( ( 𝐹𝑥 ) ∈ 𝑋 ∧ ( 𝐺𝑥 ) ∈ 𝑌 ) → ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
25 22 23 24 syl2an ( ( ( 𝐹 : 𝑈𝑋𝑥 𝑈 ) ∧ ( 𝐺 : 𝑈𝑌𝑥 𝑈 ) ) → ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
26 25 anandirs ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑥 𝑈 ) → ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
27 26 fmpttd ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) : 𝑈 ⟶ ( 𝑋 × 𝑌 ) )
28 ffn ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) : 𝑈 ⟶ ( 𝑋 × 𝑌 ) → ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) Fn 𝑈 )
29 27 28 syl ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) Fn 𝑈 )
30 27 frnd ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → ran ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ⊆ ( 𝑋 × 𝑌 ) )
31 fnco ( ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) ∧ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) Fn 𝑈 ∧ ran ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ⊆ ( 𝑋 × 𝑌 ) ) → ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) Fn 𝑈 )
32 21 29 30 31 mp3an2i ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) Fn 𝑈 )
33 fvco3 ( ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝑈 ) → ( ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
34 27 33 sylan ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ( ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
35 fveq2 ( 𝑥 = 𝑧 → ( 𝐹𝑥 ) = ( 𝐹𝑧 ) )
36 fveq2 ( 𝑥 = 𝑧 → ( 𝐺𝑥 ) = ( 𝐺𝑧 ) )
37 35 36 opeq12d ( 𝑥 = 𝑧 → ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ = ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ )
38 opex ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ∈ V
39 37 8 38 fvmpt ( 𝑧 𝑈 → ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ‘ 𝑧 ) = ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ )
40 39 adantl ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ‘ 𝑧 ) = ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ )
41 40 fveq2d ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ‘ 𝑧 ) ) = ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ) )
42 ffvelrn ( ( 𝐹 : 𝑈𝑋𝑧 𝑈 ) → ( 𝐹𝑧 ) ∈ 𝑋 )
43 ffvelrn ( ( 𝐺 : 𝑈𝑌𝑧 𝑈 ) → ( 𝐺𝑧 ) ∈ 𝑌 )
44 opelxpi ( ( ( 𝐹𝑧 ) ∈ 𝑋 ∧ ( 𝐺𝑧 ) ∈ 𝑌 ) → ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
45 42 43 44 syl2an ( ( ( 𝐹 : 𝑈𝑋𝑧 𝑈 ) ∧ ( 𝐺 : 𝑈𝑌𝑧 𝑈 ) ) → ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
46 45 anandirs ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
47 46 fvresd ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ) = ( 1st ‘ ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ) )
48 fvex ( 𝐹𝑧 ) ∈ V
49 fvex ( 𝐺𝑧 ) ∈ V
50 48 49 op1st ( 1st ‘ ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ) = ( 𝐹𝑧 )
51 47 50 eqtrdi ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ) = ( 𝐹𝑧 ) )
52 34 41 51 3eqtrrd ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ( 𝐹𝑧 ) = ( ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ‘ 𝑧 ) )
53 15 32 52 eqfnfvd ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → 𝐹 = ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) )
54 4 reseq2i ( 1st𝑍 ) = ( 1st ↾ ( 𝑋 × 𝑌 ) )
55 5 54 eqtri 𝑃 = ( 1st ↾ ( 𝑋 × 𝑌 ) )
56 55 coeq1i ( 𝑃 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) = ( ( 1st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) )
57 53 56 eqtr4di ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → 𝐹 = ( 𝑃 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) )
58 12 13 57 syl2an ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝐹 = ( 𝑃 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) )
59 ffn ( 𝐺 : 𝑈𝑌𝐺 Fn 𝑈 )
60 59 adantl ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → 𝐺 Fn 𝑈 )
61 fo2nd 2nd : V –onto→ V
62 fofn ( 2nd : V –onto→ V → 2nd Fn V )
63 61 62 ax-mp 2nd Fn V
64 fnssres ( ( 2nd Fn V ∧ ( 𝑋 × 𝑌 ) ⊆ V ) → ( 2nd ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) )
65 63 19 64 mp2an ( 2nd ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 )
66 fnco ( ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) ∧ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) Fn 𝑈 ∧ ran ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ⊆ ( 𝑋 × 𝑌 ) ) → ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) Fn 𝑈 )
67 65 29 30 66 mp3an2i ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) Fn 𝑈 )
68 fvco3 ( ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝑧 𝑈 ) → ( ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
69 27 68 sylan ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ( ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
70 40 fveq2d ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ‘ 𝑧 ) ) = ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ) )
71 46 fvresd ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ) = ( 2nd ‘ ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ) )
72 48 49 op2nd ( 2nd ‘ ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ) = ( 𝐺𝑧 )
73 71 72 eqtrdi ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹𝑧 ) , ( 𝐺𝑧 ) ⟩ ) = ( 𝐺𝑧 ) )
74 69 70 73 3eqtrrd ( ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) ∧ 𝑧 𝑈 ) → ( 𝐺𝑧 ) = ( ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ‘ 𝑧 ) )
75 60 67 74 eqfnfvd ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → 𝐺 = ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) )
76 4 reseq2i ( 2nd𝑍 ) = ( 2nd ↾ ( 𝑋 × 𝑌 ) )
77 6 76 eqtri 𝑄 = ( 2nd ↾ ( 𝑋 × 𝑌 ) )
78 77 coeq1i ( 𝑄 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) = ( ( 2nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) )
79 75 78 eqtr4di ( ( 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → 𝐺 = ( 𝑄 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) )
80 12 13 79 syl2an ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝐺 = ( 𝑄 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) )
81 11 58 80 jca32 ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ∧ 𝐺 = ( 𝑄 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ) ) )
82 eleq1 ( = ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) → ( ∈ ( 𝑈 Cn 𝑇 ) ↔ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) ) )
83 coeq2 ( = ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) → ( 𝑃 ) = ( 𝑃 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) )
84 83 eqeq2d ( = ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) → ( 𝐹 = ( 𝑃 ) ↔ 𝐹 = ( 𝑃 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ) )
85 coeq2 ( = ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) → ( 𝑄 ) = ( 𝑄 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) )
86 85 eqeq2d ( = ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) → ( 𝐺 = ( 𝑄 ) ↔ 𝐺 = ( 𝑄 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ) )
87 84 86 anbi12d ( = ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) → ( ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ↔ ( 𝐹 = ( 𝑃 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ∧ 𝐺 = ( 𝑄 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ) ) )
88 82 87 anbi12d ( = ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) → ( ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) ↔ ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ∧ 𝐺 = ( 𝑄 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ) ) ) )
89 88 spcegv ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) → ( ( ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ∧ 𝐺 = ( 𝑄 ∘ ( 𝑥 𝑈 ↦ ⟨ ( 𝐹𝑥 ) , ( 𝐺𝑥 ) ⟩ ) ) ) ) → ∃ ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) ) )
90 11 81 89 sylc ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃ ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) )
91 eqid 𝑇 = 𝑇
92 7 91 cnf ( ∈ ( 𝑈 Cn 𝑇 ) → : 𝑈 𝑇 )
93 cntop2 ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) → 𝑅 ∈ Top )
94 cntop2 ( 𝐺 ∈ ( 𝑈 Cn 𝑆 ) → 𝑆 ∈ Top )
95 1 unieqi 𝑇 = ( 𝑅 ×t 𝑆 )
96 2 3 txuni ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × 𝑌 ) = ( 𝑅 ×t 𝑆 ) )
97 95 96 eqtr4id ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → 𝑇 = ( 𝑋 × 𝑌 ) )
98 93 94 97 syl2an ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝑇 = ( 𝑋 × 𝑌 ) )
99 98 feq3d ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( : 𝑈 𝑇 : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ) )
100 92 99 syl5ib ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( ∈ ( 𝑈 Cn 𝑇 ) → : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ) )
101 100 anim1d ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) → ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) ) )
102 3anass ( ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ↔ ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) )
103 101 102 syl6ibr ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) → ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) )
104 103 alrimiv ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∀ ( ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) → ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) )
105 cntop1 ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) → 𝑈 ∈ Top )
106 105 uniexd ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) → 𝑈 ∈ V )
107 55 77 upxp ( ( 𝑈 ∈ V ∧ 𝐹 : 𝑈𝑋𝐺 : 𝑈𝑌 ) → ∃! ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) )
108 106 12 13 107 syl2an3an ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃! ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) )
109 eumo ( ∃! ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) → ∃* ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) )
110 108 109 syl ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃* ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) )
111 moim ( ∀ ( ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) → ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) → ( ∃* ( : 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) → ∃* ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) ) )
112 104 110 111 sylc ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃* ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) )
113 df-reu ( ∃! ∈ ( 𝑈 Cn 𝑇 ) ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ↔ ∃! ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) )
114 df-eu ( ∃! ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) ↔ ( ∃ ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) ∧ ∃* ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) ) )
115 113 114 bitri ( ∃! ∈ ( 𝑈 Cn 𝑇 ) ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ↔ ( ∃ ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) ∧ ∃* ( ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) ) ) )
116 90 112 115 sylanbrc ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃! ∈ ( 𝑈 Cn 𝑇 ) ( 𝐹 = ( 𝑃 ) ∧ 𝐺 = ( 𝑄 ) ) )