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

Theorem upxp 23646
Description: Universal property of the Cartesian product considered as a categorical product in the category of sets. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
Hypotheses
Ref Expression
upxp.1 𝑃 = (1st ↾ (𝐵 × 𝐶))
upxp.2 𝑄 = (2nd ↾ (𝐵 × 𝐶))
Assertion
Ref Expression
upxp ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ∃!(:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))
Distinct variable groups:   𝐴,   𝐵,   𝐶,   ,𝐹   ,𝐺   𝐷,
Allowed substitution hints:   𝑃()   𝑄()

Proof of Theorem upxp
Dummy variables 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mptexg 7240 . . . 4 (𝐴𝐷 → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ∈ V)
2 eueq 3716 . . . 4 ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ∈ V ↔ ∃! = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
31, 2sylib 218 . . 3 (𝐴𝐷 → ∃! = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
433ad2ant1 1132 . 2 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ∃! = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
5 ffn 6736 . . . . . . . 8 (:𝐴⟶(𝐵 × 𝐶) → Fn 𝐴)
653ad2ant1 1132 . . . . . . 7 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) → Fn 𝐴)
76adantl 481 . . . . . 6 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → Fn 𝐴)
8 ffvelcdm 7100 . . . . . . . . . . . . 13 ((𝐹:𝐴𝐵𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
9 ffvelcdm 7100 . . . . . . . . . . . . 13 ((𝐺:𝐴𝐶𝑥𝐴) → (𝐺𝑥) ∈ 𝐶)
10 opelxpi 5725 . . . . . . . . . . . . 13 (((𝐹𝑥) ∈ 𝐵 ∧ (𝐺𝑥) ∈ 𝐶) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
118, 9, 10syl2an 596 . . . . . . . . . . . 12 (((𝐹:𝐴𝐵𝑥𝐴) ∧ (𝐺:𝐴𝐶𝑥𝐴)) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
1211anandirs 679 . . . . . . . . . . 11 (((𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑥𝐴) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
1312ralrimiva 3143 . . . . . . . . . 10 ((𝐹:𝐴𝐵𝐺:𝐴𝐶) → ∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
14133adant1 1129 . . . . . . . . 9 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
15 eqid 2734 . . . . . . . . . 10 (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)
1615fmpt 7129 . . . . . . . . 9 (∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶) ↔ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶))
1714, 16sylib 218 . . . . . . . 8 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶))
1817ffnd 6737 . . . . . . 7 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴)
1918adantr 480 . . . . . 6 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴)
20 xpss 5704 . . . . . . . . . . 11 (𝐵 × 𝐶) ⊆ (V × V)
21 ffvelcdm 7100 . . . . . . . . . . 11 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (𝑧) ∈ (𝐵 × 𝐶))
2220, 21sselid 3992 . . . . . . . . . 10 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (𝑧) ∈ (V × V))
23223ad2antl1 1184 . . . . . . . . 9 (((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ∧ 𝑧𝐴) → (𝑧) ∈ (V × V))
2423adantll 714 . . . . . . . 8 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝑧) ∈ (V × V))
25 fveq1 6905 . . . . . . . . . . . 12 (𝐹 = (𝑃) → (𝐹𝑧) = ((𝑃)‘𝑧))
26 upxp.1 . . . . . . . . . . . . . 14 𝑃 = (1st ↾ (𝐵 × 𝐶))
2726coeq1i 5872 . . . . . . . . . . . . 13 (𝑃) = ((1st ↾ (𝐵 × 𝐶)) ∘ )
2827fveq1i 6907 . . . . . . . . . . . 12 ((𝑃)‘𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧)
2925, 28eqtrdi 2790 . . . . . . . . . . 11 (𝐹 = (𝑃) → (𝐹𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
30293ad2ant2 1133 . . . . . . . . . 10 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) → (𝐹𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
3130ad2antlr 727 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝐹𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
32 simpr1 1193 . . . . . . . . . 10 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → :𝐴⟶(𝐵 × 𝐶))
33 fvco3 7007 . . . . . . . . . 10 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘(𝑧)))
3432, 33sylan 580 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘(𝑧)))
35213ad2antl1 1184 . . . . . . . . . . 11 (((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ∧ 𝑧𝐴) → (𝑧) ∈ (𝐵 × 𝐶))
3635adantll 714 . . . . . . . . . 10 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝑧) ∈ (𝐵 × 𝐶))
3736fvresd 6926 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → ((1st ↾ (𝐵 × 𝐶))‘(𝑧)) = (1st ‘(𝑧)))
3831, 34, 373eqtrrd 2779 . . . . . . . 8 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (1st ‘(𝑧)) = (𝐹𝑧))
39 fveq1 6905 . . . . . . . . . . . 12 (𝐺 = (𝑄) → (𝐺𝑧) = ((𝑄)‘𝑧))
40 upxp.2 . . . . . . . . . . . . . 14 𝑄 = (2nd ↾ (𝐵 × 𝐶))
4140coeq1i 5872 . . . . . . . . . . . . 13 (𝑄) = ((2nd ↾ (𝐵 × 𝐶)) ∘ )
4241fveq1i 6907 . . . . . . . . . . . 12 ((𝑄)‘𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧)
4339, 42eqtrdi 2790 . . . . . . . . . . 11 (𝐺 = (𝑄) → (𝐺𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
44433ad2ant3 1134 . . . . . . . . . 10 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) → (𝐺𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
4544ad2antlr 727 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝐺𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
46 fvco3 7007 . . . . . . . . . 10 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘(𝑧)))
4732, 46sylan 580 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘(𝑧)))
4836fvresd 6926 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘(𝑧)) = (2nd ‘(𝑧)))
4945, 47, 483eqtrrd 2779 . . . . . . . 8 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (2nd ‘(𝑧)) = (𝐺𝑧))
50 eqopi 8048 . . . . . . . 8 (((𝑧) ∈ (V × V) ∧ ((1st ‘(𝑧)) = (𝐹𝑧) ∧ (2nd ‘(𝑧)) = (𝐺𝑧))) → (𝑧) = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
5124, 38, 49, 50syl12anc 837 . . . . . . 7 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝑧) = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
52 fveq2 6906 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
53 fveq2 6906 . . . . . . . . . 10 (𝑥 = 𝑧 → (𝐺𝑥) = (𝐺𝑧))
5452, 53opeq12d 4885 . . . . . . . . 9 (𝑥 = 𝑧 → ⟨(𝐹𝑥), (𝐺𝑥)⟩ = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
55 opex 5474 . . . . . . . . 9 ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ V
5654, 15, 55fvmpt 7015 . . . . . . . 8 (𝑧𝐴 → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧) = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
5756adantl 481 . . . . . . 7 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧) = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
5851, 57eqtr4d 2777 . . . . . 6 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝑧) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧))
597, 19, 58eqfnfvd 7053 . . . . 5 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
6059ex 412 . . . 4 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) → = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
61 ffn 6736 . . . . . . . . 9 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
62613ad2ant2 1133 . . . . . . . 8 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐹 Fn 𝐴)
63 fo1st 8032 . . . . . . . . . . 11 1st :V–onto→V
64 fofn 6822 . . . . . . . . . . 11 (1st :V–onto→V → 1st Fn V)
6563, 64ax-mp 5 . . . . . . . . . 10 1st Fn V
66 ssv 4019 . . . . . . . . . 10 (𝐵 × 𝐶) ⊆ V
67 fnssres 6691 . . . . . . . . . 10 ((1st Fn V ∧ (𝐵 × 𝐶) ⊆ V) → (1st ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶))
6865, 66, 67mp2an 692 . . . . . . . . 9 (1st ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶)
6917frnd 6744 . . . . . . . . 9 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ran (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ⊆ (𝐵 × 𝐶))
70 fnco 6686 . . . . . . . . 9 (((1st ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶) ∧ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴 ∧ ran (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ⊆ (𝐵 × 𝐶)) → ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝐴)
7168, 18, 69, 70mp3an2i 1465 . . . . . . . 8 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝐴)
72 fvco3 7007 . . . . . . . . . 10 (((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
7317, 72sylan 580 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
7456adantl 481 . . . . . . . . . 10 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧) = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
7574fveq2d 6910 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((1st ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)) = ((1st ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
76 ffvelcdm 7100 . . . . . . . . . . . . . 14 ((𝐹:𝐴𝐵𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
77 ffvelcdm 7100 . . . . . . . . . . . . . 14 ((𝐺:𝐴𝐶𝑧𝐴) → (𝐺𝑧) ∈ 𝐶)
78 opelxpi 5725 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ 𝐵 ∧ (𝐺𝑧) ∈ 𝐶) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝐵 × 𝐶))
7976, 77, 78syl2an 596 . . . . . . . . . . . . 13 (((𝐹:𝐴𝐵𝑧𝐴) ∧ (𝐺:𝐴𝐶𝑧𝐴)) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝐵 × 𝐶))
8079anandirs 679 . . . . . . . . . . . 12 (((𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝐵 × 𝐶))
81803adantl1 1165 . . . . . . . . . . 11 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝐵 × 𝐶))
8281fvresd 6926 . . . . . . . . . 10 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((1st ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (1st ‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
83 fvex 6919 . . . . . . . . . . 11 (𝐹𝑧) ∈ V
84 fvex 6919 . . . . . . . . . . 11 (𝐺𝑧) ∈ V
8583, 84op1st 8020 . . . . . . . . . 10 (1st ‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐹𝑧)
8682, 85eqtrdi 2790 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((1st ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐹𝑧))
8773, 75, 863eqtrrd 2779 . . . . . . . 8 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (𝐹𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧))
8862, 71, 87eqfnfvd 7053 . . . . . . 7 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐹 = ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
8926coeq1i 5872 . . . . . . 7 (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) = ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
9088, 89eqtr4di 2792 . . . . . 6 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐹 = (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
91 ffn 6736 . . . . . . . . 9 (𝐺:𝐴𝐶𝐺 Fn 𝐴)
92913ad2ant3 1134 . . . . . . . 8 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐺 Fn 𝐴)
93 fo2nd 8033 . . . . . . . . . . 11 2nd :V–onto→V
94 fofn 6822 . . . . . . . . . . 11 (2nd :V–onto→V → 2nd Fn V)
9593, 94ax-mp 5 . . . . . . . . . 10 2nd Fn V
96 fnssres 6691 . . . . . . . . . 10 ((2nd Fn V ∧ (𝐵 × 𝐶) ⊆ V) → (2nd ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶))
9795, 66, 96mp2an 692 . . . . . . . . 9 (2nd ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶)
98 fnco 6686 . . . . . . . . 9 (((2nd ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶) ∧ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴 ∧ ran (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ⊆ (𝐵 × 𝐶)) → ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝐴)
9997, 18, 69, 98mp3an2i 1465 . . . . . . . 8 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝐴)
100 fvco3 7007 . . . . . . . . . 10 (((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
10117, 100sylan 580 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
10274fveq2d 6910 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)) = ((2nd ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
10381fvresd 6926 . . . . . . . . . 10 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (2nd ‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
10483, 84op2nd 8021 . . . . . . . . . 10 (2nd ‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐺𝑧)
105103, 104eqtrdi 2790 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐺𝑧))
106101, 102, 1053eqtrrd 2779 . . . . . . . 8 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (𝐺𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧))
10792, 99, 106eqfnfvd 7053 . . . . . . 7 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐺 = ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
10840coeq1i 5872 . . . . . . 7 (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) = ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
109107, 108eqtr4di 2792 . . . . . 6 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐺 = (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
11017, 90, 1093jca 1127 . . . . 5 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) ∧ 𝐺 = (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))))
111 feq1 6716 . . . . . 6 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (:𝐴⟶(𝐵 × 𝐶) ↔ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶)))
112 coeq2 5871 . . . . . . 7 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝑃) = (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
113112eqeq2d 2745 . . . . . 6 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝐹 = (𝑃) ↔ 𝐹 = (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))))
114 coeq2 5871 . . . . . . 7 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝑄) = (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
115114eqeq2d 2745 . . . . . 6 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝐺 = (𝑄) ↔ 𝐺 = (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))))
116111, 113, 1153anbi123d 1435 . . . . 5 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ↔ ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) ∧ 𝐺 = (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))))
117110, 116syl5ibrcom 247 . . . 4 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))))
11860, 117impbid 212 . . 3 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ↔ = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
119118eubidv 2583 . 2 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → (∃!(:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ↔ ∃! = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
1204, 119mpbird 257 1 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ∃!(:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1536  wcel 2105  ∃!weu 2565  wral 3058  Vcvv 3477  wss 3962  cop 4636  cmpt 5230   × cxp 5686  ran crn 5689  cres 5690  ccom 5692   Fn wfn 6557  wf 6558  ontowfo 6560  cfv 6562  1st c1st 8010  2nd c2nd 8011
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-1st 8012  df-2nd 8013
This theorem is referenced by:  uptx  23648  txcn  23649
  Copyright terms: Public domain W3C validator