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 ffvelcdm ⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝑥 ∈ ∪ 𝑈 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
23 ffvelcdm ⊢ ( ( 𝐺 : ∪ 𝑈 ⟶ 𝑌 ∧ 𝑥 ∈ ∪ 𝑈 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑌 )
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 ffvelcdm ⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝑧 ∈ ∪ 𝑈 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑋 )
43 ffvelcdm ⊢ ( ( 𝐺 : ∪ 𝑈 ⟶ 𝑌 ∧ 𝑧 ∈ ∪ 𝑈 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑌 )
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 imbitrid ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( ℎ ∈ ( 𝑈 Cn 𝑇 ) → ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ) )
101 100 anim1d ⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) → ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ) )
102 3anass ⊢ ( ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ↔ ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) )
103 101 102 imbitrrdi ⊢ ( ( 𝐹 ∈ ( 𝑈 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 𝑇 ) ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) )