Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  uptx Structured version   Visualization version   GIF version

Theorem uptx 21650
 Description: Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
uptx.1 𝑇 = (𝑅 ×t 𝑆)
uptx.2 𝑋 = 𝑅
uptx.3 𝑌 = 𝑆
uptx.4 𝑍 = (𝑋 × 𝑌)
uptx.5 𝑃 = (1st𝑍)
uptx.6 𝑄 = (2nd𝑍)
Assertion
Ref Expression
uptx ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃! ∈ (𝑈 Cn 𝑇)(𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))
Distinct variable groups:   ,𝐹   ,𝐺   𝑃,   𝑄,   𝑅,   𝑇,   𝑆,   𝑈,   ,𝑋   ,𝑌
Allowed substitution hint:   𝑍()

Proof of Theorem uptx
Dummy variables 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2760 . . . . 5 𝑈 = 𝑈
2 eqid 2760 . . . . 5 (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) = (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)
31, 2txcnmpt 21649 . . . 4 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ∈ (𝑈 Cn (𝑅 ×t 𝑆)))
4 uptx.1 . . . . 5 𝑇 = (𝑅 ×t 𝑆)
54oveq2i 6825 . . . 4 (𝑈 Cn 𝑇) = (𝑈 Cn (𝑅 ×t 𝑆))
63, 5syl6eleqr 2850 . . 3 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ∈ (𝑈 Cn 𝑇))
7 uptx.2 . . . . . 6 𝑋 = 𝑅
81, 7cnf 21272 . . . . 5 (𝐹 ∈ (𝑈 Cn 𝑅) → 𝐹: 𝑈𝑋)
9 uptx.3 . . . . . 6 𝑌 = 𝑆
101, 9cnf 21272 . . . . 5 (𝐺 ∈ (𝑈 Cn 𝑆) → 𝐺: 𝑈𝑌)
11 ffn 6206 . . . . . . . 8 (𝐹: 𝑈𝑋𝐹 Fn 𝑈)
1211adantr 472 . . . . . . 7 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → 𝐹 Fn 𝑈)
13 fo1st 7354 . . . . . . . . . . 11 1st :V–onto→V
14 fofn 6279 . . . . . . . . . . 11 (1st :V–onto→V → 1st Fn V)
1513, 14ax-mp 5 . . . . . . . . . 10 1st Fn V
16 ssv 3766 . . . . . . . . . 10 (𝑋 × 𝑌) ⊆ V
17 fnssres 6165 . . . . . . . . . 10 ((1st Fn V ∧ (𝑋 × 𝑌) ⊆ V) → (1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
1815, 16, 17mp2an 710 . . . . . . . . 9 (1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)
1918a1i 11 . . . . . . . 8 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → (1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
20 ffvelrn 6521 . . . . . . . . . . . 12 ((𝐹: 𝑈𝑋𝑥 𝑈) → (𝐹𝑥) ∈ 𝑋)
21 ffvelrn 6521 . . . . . . . . . . . 12 ((𝐺: 𝑈𝑌𝑥 𝑈) → (𝐺𝑥) ∈ 𝑌)
22 opelxpi 5305 . . . . . . . . . . . 12 (((𝐹𝑥) ∈ 𝑋 ∧ (𝐺𝑥) ∈ 𝑌) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝑋 × 𝑌))
2320, 21, 22syl2an 495 . . . . . . . . . . 11 (((𝐹: 𝑈𝑋𝑥 𝑈) ∧ (𝐺: 𝑈𝑌𝑥 𝑈)) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝑋 × 𝑌))
2423anandirs 909 . . . . . . . . . 10 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑥 𝑈) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝑋 × 𝑌))
2524, 2fmptd 6549 . . . . . . . . 9 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩): 𝑈⟶(𝑋 × 𝑌))
26 ffn 6206 . . . . . . . . 9 ((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩): 𝑈⟶(𝑋 × 𝑌) → (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝑈)
2725, 26syl 17 . . . . . . . 8 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝑈)
28 frn 6214 . . . . . . . . 9 ((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩): 𝑈⟶(𝑋 × 𝑌) → ran (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ⊆ (𝑋 × 𝑌))
2925, 28syl 17 . . . . . . . 8 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → ran (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ⊆ (𝑋 × 𝑌))
30 fnco 6160 . . . . . . . 8 (((1st ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝑈 ∧ ran (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ⊆ (𝑋 × 𝑌)) → ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝑈)
3119, 27, 29, 30syl3anc 1477 . . . . . . 7 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝑈)
32 fvco3 6438 . . . . . . . . 9 (((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩): 𝑈⟶(𝑋 × 𝑌) ∧ 𝑧 𝑈) → (((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((1st ↾ (𝑋 × 𝑌))‘((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
3325, 32sylan 489 . . . . . . . 8 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → (((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((1st ↾ (𝑋 × 𝑌))‘((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
34 fveq2 6353 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
35 fveq2 6353 . . . . . . . . . . . 12 (𝑥 = 𝑧 → (𝐺𝑥) = (𝐺𝑧))
3634, 35opeq12d 4561 . . . . . . . . . . 11 (𝑥 = 𝑧 → ⟨(𝐹𝑥), (𝐺𝑥)⟩ = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
37 opex 5081 . . . . . . . . . . 11 ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ V
3836, 2, 37fvmpt 6445 . . . . . . . . . 10 (𝑧 𝑈 → ((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧) = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
3938adantl 473 . . . . . . . . 9 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → ((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧) = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
4039fveq2d 6357 . . . . . . . 8 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → ((1st ↾ (𝑋 × 𝑌))‘((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)) = ((1st ↾ (𝑋 × 𝑌))‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
41 ffvelrn 6521 . . . . . . . . . . . 12 ((𝐹: 𝑈𝑋𝑧 𝑈) → (𝐹𝑧) ∈ 𝑋)
42 ffvelrn 6521 . . . . . . . . . . . 12 ((𝐺: 𝑈𝑌𝑧 𝑈) → (𝐺𝑧) ∈ 𝑌)
43 opelxpi 5305 . . . . . . . . . . . 12 (((𝐹𝑧) ∈ 𝑋 ∧ (𝐺𝑧) ∈ 𝑌) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝑋 × 𝑌))
4441, 42, 43syl2an 495 . . . . . . . . . . 11 (((𝐹: 𝑈𝑋𝑧 𝑈) ∧ (𝐺: 𝑈𝑌𝑧 𝑈)) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝑋 × 𝑌))
4544anandirs 909 . . . . . . . . . 10 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝑋 × 𝑌))
46 fvres 6369 . . . . . . . . . 10 (⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝑋 × 𝑌) → ((1st ↾ (𝑋 × 𝑌))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (1st ‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
4745, 46syl 17 . . . . . . . . 9 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → ((1st ↾ (𝑋 × 𝑌))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (1st ‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
48 fvex 6363 . . . . . . . . . 10 (𝐹𝑧) ∈ V
49 fvex 6363 . . . . . . . . . 10 (𝐺𝑧) ∈ V
5048, 49op1st 7342 . . . . . . . . 9 (1st ‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐹𝑧)
5147, 50syl6eq 2810 . . . . . . . 8 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → ((1st ↾ (𝑋 × 𝑌))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐹𝑧))
5233, 40, 513eqtrrd 2799 . . . . . . 7 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → (𝐹𝑧) = (((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧))
5312, 31, 52eqfnfvd 6478 . . . . . 6 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → 𝐹 = ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
54 uptx.5 . . . . . . . 8 𝑃 = (1st𝑍)
55 uptx.4 . . . . . . . . 9 𝑍 = (𝑋 × 𝑌)
5655reseq2i 5548 . . . . . . . 8 (1st𝑍) = (1st ↾ (𝑋 × 𝑌))
5754, 56eqtri 2782 . . . . . . 7 𝑃 = (1st ↾ (𝑋 × 𝑌))
5857coeq1i 5437 . . . . . 6 (𝑃 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) = ((1st ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
5953, 58syl6eqr 2812 . . . . 5 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → 𝐹 = (𝑃 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
608, 10, 59syl2an 495 . . . 4 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐹 = (𝑃 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
61 ffn 6206 . . . . . . . 8 (𝐺: 𝑈𝑌𝐺 Fn 𝑈)
6261adantl 473 . . . . . . 7 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → 𝐺 Fn 𝑈)
63 fo2nd 7355 . . . . . . . . . . 11 2nd :V–onto→V
64 fofn 6279 . . . . . . . . . . 11 (2nd :V–onto→V → 2nd Fn V)
6563, 64ax-mp 5 . . . . . . . . . 10 2nd Fn V
66 fnssres 6165 . . . . . . . . . 10 ((2nd Fn V ∧ (𝑋 × 𝑌) ⊆ V) → (2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
6765, 16, 66mp2an 710 . . . . . . . . 9 (2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌)
6867a1i 11 . . . . . . . 8 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → (2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌))
69 fnco 6160 . . . . . . . 8 (((2nd ↾ (𝑋 × 𝑌)) Fn (𝑋 × 𝑌) ∧ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝑈 ∧ ran (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ⊆ (𝑋 × 𝑌)) → ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝑈)
7068, 27, 29, 69syl3anc 1477 . . . . . . 7 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝑈)
71 fvco3 6438 . . . . . . . . 9 (((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩): 𝑈⟶(𝑋 × 𝑌) ∧ 𝑧 𝑈) → (((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((2nd ↾ (𝑋 × 𝑌))‘((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
7225, 71sylan 489 . . . . . . . 8 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → (((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((2nd ↾ (𝑋 × 𝑌))‘((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
7339fveq2d 6357 . . . . . . . 8 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → ((2nd ↾ (𝑋 × 𝑌))‘((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)) = ((2nd ↾ (𝑋 × 𝑌))‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
74 fvres 6369 . . . . . . . . . 10 (⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝑋 × 𝑌) → ((2nd ↾ (𝑋 × 𝑌))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (2nd ‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
7545, 74syl 17 . . . . . . . . 9 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → ((2nd ↾ (𝑋 × 𝑌))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (2nd ‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
7648, 49op2nd 7343 . . . . . . . . 9 (2nd ‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐺𝑧)
7775, 76syl6eq 2810 . . . . . . . 8 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → ((2nd ↾ (𝑋 × 𝑌))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐺𝑧))
7872, 73, 773eqtrrd 2799 . . . . . . 7 (((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) ∧ 𝑧 𝑈) → (𝐺𝑧) = (((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧))
7962, 70, 78eqfnfvd 6478 . . . . . 6 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → 𝐺 = ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
80 uptx.6 . . . . . . . 8 𝑄 = (2nd𝑍)
8155reseq2i 5548 . . . . . . . 8 (2nd𝑍) = (2nd ↾ (𝑋 × 𝑌))
8280, 81eqtri 2782 . . . . . . 7 𝑄 = (2nd ↾ (𝑋 × 𝑌))
8382coeq1i 5437 . . . . . 6 (𝑄 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) = ((2nd ↾ (𝑋 × 𝑌)) ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
8479, 83syl6eqr 2812 . . . . 5 ((𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → 𝐺 = (𝑄 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
858, 10, 84syl2an 495 . . . 4 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐺 = (𝑄 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
866, 60, 85jca32 559 . . 3 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) ∧ 𝐺 = (𝑄 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))))
87 eleq1 2827 . . . . 5 ( = (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → ( ∈ (𝑈 Cn 𝑇) ↔ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ∈ (𝑈 Cn 𝑇)))
88 coeq2 5436 . . . . . . 7 ( = (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝑃) = (𝑃 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
8988eqeq2d 2770 . . . . . 6 ( = (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝐹 = (𝑃) ↔ 𝐹 = (𝑃 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))))
90 coeq2 5436 . . . . . . 7 ( = (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝑄) = (𝑄 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
9190eqeq2d 2770 . . . . . 6 ( = (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝐺 = (𝑄) ↔ 𝐺 = (𝑄 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))))
9289, 91anbi12d 749 . . . . 5 ( = (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → ((𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ↔ (𝐹 = (𝑃 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) ∧ 𝐺 = (𝑄 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))))
9387, 92anbi12d 749 . . . 4 ( = (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ↔ ((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) ∧ 𝐺 = (𝑄 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))))))
9493spcegv 3434 . . 3 ((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ∈ (𝑈 Cn 𝑇) → (((𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) ∧ 𝐺 = (𝑄 ∘ (𝑥 𝑈 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))) → ∃( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))))
956, 86, 94sylc 65 . 2 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))))
96 eqid 2760 . . . . . . . 8 𝑇 = 𝑇
971, 96cnf 21272 . . . . . . 7 ( ∈ (𝑈 Cn 𝑇) → : 𝑈 𝑇)
98 cntop2 21267 . . . . . . . . 9 (𝐹 ∈ (𝑈 Cn 𝑅) → 𝑅 ∈ Top)
99 cntop2 21267 . . . . . . . . 9 (𝐺 ∈ (𝑈 Cn 𝑆) → 𝑆 ∈ Top)
1007, 9txuni 21617 . . . . . . . . . 10 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → (𝑋 × 𝑌) = (𝑅 ×t 𝑆))
1014unieqi 4597 . . . . . . . . . 10 𝑇 = (𝑅 ×t 𝑆)
102100, 101syl6reqr 2813 . . . . . . . . 9 ((𝑅 ∈ Top ∧ 𝑆 ∈ Top) → 𝑇 = (𝑋 × 𝑌))
10398, 99, 102syl2an 495 . . . . . . . 8 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝑇 = (𝑋 × 𝑌))
104103feq3d 6193 . . . . . . 7 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (: 𝑈 𝑇: 𝑈⟶(𝑋 × 𝑌)))
10597, 104syl5ib 234 . . . . . 6 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ( ∈ (𝑈 Cn 𝑇) → : 𝑈⟶(𝑋 × 𝑌)))
106105anim1d 589 . . . . 5 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → (: 𝑈⟶(𝑋 × 𝑌) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))))
107 3anass 1081 . . . . 5 ((: 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ↔ (: 𝑈⟶(𝑋 × 𝑌) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))))
108106, 107syl6ibr 242 . . . 4 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → (( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → (: 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))))
109108alrimiv 2004 . . 3 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∀(( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → (: 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))))
110 cntop1 21266 . . . . . . 7 (𝐹 ∈ (𝑈 Cn 𝑅) → 𝑈 ∈ Top)
111 uniexg 7121 . . . . . . 7 (𝑈 ∈ Top → 𝑈 ∈ V)
112110, 111syl 17 . . . . . 6 (𝐹 ∈ (𝑈 Cn 𝑅) → 𝑈 ∈ V)
113112adantr 472 . . . . 5 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝑈 ∈ V)
1148adantr 472 . . . . 5 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐹: 𝑈𝑋)
11510adantl 473 . . . . 5 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → 𝐺: 𝑈𝑌)
11657, 82upxp 21648 . . . . 5 (( 𝑈 ∈ V ∧ 𝐹: 𝑈𝑋𝐺: 𝑈𝑌) → ∃!(: 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))
117113, 114, 115, 116syl3anc 1477 . . . 4 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃!(: 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))
118 eumo 2636 . . . 4 (∃!(: 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) → ∃*(: 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))
119117, 118syl 17 . . 3 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃*(: 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))
120 moim 2657 . . 3 (∀(( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → (: 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → (∃*(: 𝑈⟶(𝑋 × 𝑌) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) → ∃*( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))))
121109, 119, 120sylc 65 . 2 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃*( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))))
122 df-reu 3057 . . 3 (∃! ∈ (𝑈 Cn 𝑇)(𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ↔ ∃!( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))))
123 eu5 2633 . . 3 (∃!( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ↔ (∃( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ ∃*( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))))
124122, 123bitri 264 . 2 (∃! ∈ (𝑈 Cn 𝑇)(𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ↔ (∃( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ ∃*( ∈ (𝑈 Cn 𝑇) ∧ (𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))))
12595, 121, 124sylanbrc 701 1 ((𝐹 ∈ (𝑈 Cn 𝑅) ∧ 𝐺 ∈ (𝑈 Cn 𝑆)) → ∃! ∈ (𝑈 Cn 𝑇)(𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072  ∀wal 1630   = wceq 1632  ∃wex 1853   ∈ wcel 2139  ∃!weu 2607  ∃*wmo 2608  ∃!wreu 3052  Vcvv 3340   ⊆ wss 3715  ⟨cop 4327  ∪ cuni 4588   ↦ cmpt 4881   × cxp 5264  ran crn 5267   ↾ cres 5268   ∘ ccom 5270   Fn wfn 6044  ⟶wf 6045  –onto→wfo 6047  ‘cfv 6049  (class class class)co 6814  1st c1st 7332  2nd c2nd 7333  Topctop 20920   Cn ccn 21250   ×t ctx 21585 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-rep 4923  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7115 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ne 2933  df-ral 3055  df-rex 3056  df-reu 3057  df-rab 3059  df-v 3342  df-sbc 3577  df-csb 3675  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-pw 4304  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-iun 4674  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279  df-iota 6012  df-fun 6051  df-fn 6052  df-f 6053  df-f1 6054  df-fo 6055  df-f1o 6056  df-fv 6057  df-ov 6817  df-oprab 6818  df-mpt2 6819  df-1st 7334  df-2nd 7335  df-map 8027  df-topgen 16326  df-top 20921  df-topon 20938  df-bases 20972  df-cn 21253  df-tx 21587 This theorem is referenced by:  txcn  21651
 Copyright terms: Public domain W3C validator