MPE Home 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  ontowfo 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