Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  upxp GIF version

Theorem upxp 12467
 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 5648 . . . 4 (𝐴𝐷 → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ∈ V)
2 eueq 2855 . . . 4 ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ∈ V ↔ ∃! = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
31, 2sylib 121 . . 3 (𝐴𝐷 → ∃! = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
433ad2ant1 1002 . 2 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ∃! = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
5 ffn 5275 . . . . . . . 8 (:𝐴⟶(𝐵 × 𝐶) → Fn 𝐴)
653ad2ant1 1002 . . . . . . 7 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) → Fn 𝐴)
76adantl 275 . . . . . 6 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → Fn 𝐴)
8 ffvelrn 5556 . . . . . . . . . . . . 13 ((𝐹:𝐴𝐵𝑥𝐴) → (𝐹𝑥) ∈ 𝐵)
9 ffvelrn 5556 . . . . . . . . . . . . 13 ((𝐺:𝐴𝐶𝑥𝐴) → (𝐺𝑥) ∈ 𝐶)
10 opelxpi 4574 . . . . . . . . . . . . 13 (((𝐹𝑥) ∈ 𝐵 ∧ (𝐺𝑥) ∈ 𝐶) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
118, 9, 10syl2an 287 . . . . . . . . . . . 12 (((𝐹:𝐴𝐵𝑥𝐴) ∧ (𝐺:𝐴𝐶𝑥𝐴)) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
1211anandirs 582 . . . . . . . . . . 11 (((𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑥𝐴) → ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
1312ralrimiva 2505 . . . . . . . . . 10 ((𝐹:𝐴𝐵𝐺:𝐴𝐶) → ∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
14133adant1 999 . . . . . . . . 9 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶))
15 eqid 2139 . . . . . . . . . 10 (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)
1615fmpt 5573 . . . . . . . . 9 (∀𝑥𝐴 ⟨(𝐹𝑥), (𝐺𝑥)⟩ ∈ (𝐵 × 𝐶) ↔ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶))
1714, 16sylib 121 . . . . . . . 8 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶))
1817ffnd 5276 . . . . . . 7 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴)
1918adantr 274 . . . . . 6 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴)
20 xpss 4650 . . . . . . . . . . 11 (𝐵 × 𝐶) ⊆ (V × V)
21 ffvelrn 5556 . . . . . . . . . . 11 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (𝑧) ∈ (𝐵 × 𝐶))
2220, 21sseldi 3095 . . . . . . . . . 10 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (𝑧) ∈ (V × V))
23223ad2antl1 1143 . . . . . . . . 9 (((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ∧ 𝑧𝐴) → (𝑧) ∈ (V × V))
2423adantll 467 . . . . . . . 8 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝑧) ∈ (V × V))
25 fveq1 5423 . . . . . . . . . . . 12 (𝐹 = (𝑃) → (𝐹𝑧) = ((𝑃)‘𝑧))
26 upxp.1 . . . . . . . . . . . . . 14 𝑃 = (1st ↾ (𝐵 × 𝐶))
2726coeq1i 4701 . . . . . . . . . . . . 13 (𝑃) = ((1st ↾ (𝐵 × 𝐶)) ∘ )
2827fveq1i 5425 . . . . . . . . . . . 12 ((𝑃)‘𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧)
2925, 28eqtrdi 2188 . . . . . . . . . . 11 (𝐹 = (𝑃) → (𝐹𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
30293ad2ant2 1003 . . . . . . . . . 10 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) → (𝐹𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
3130ad2antlr 480 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝐹𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
32 simpr1 987 . . . . . . . . . 10 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → :𝐴⟶(𝐵 × 𝐶))
33 fvco3 5495 . . . . . . . . . 10 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘(𝑧)))
3432, 33sylan 281 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ )‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘(𝑧)))
35213ad2antl1 1143 . . . . . . . . . . 11 (((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ∧ 𝑧𝐴) → (𝑧) ∈ (𝐵 × 𝐶))
3635adantll 467 . . . . . . . . . 10 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝑧) ∈ (𝐵 × 𝐶))
3736fvresd 5449 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → ((1st ↾ (𝐵 × 𝐶))‘(𝑧)) = (1st ‘(𝑧)))
3831, 34, 373eqtrrd 2177 . . . . . . . 8 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (1st ‘(𝑧)) = (𝐹𝑧))
39 fveq1 5423 . . . . . . . . . . . 12 (𝐺 = (𝑄) → (𝐺𝑧) = ((𝑄)‘𝑧))
40 upxp.2 . . . . . . . . . . . . . 14 𝑄 = (2nd ↾ (𝐵 × 𝐶))
4140coeq1i 4701 . . . . . . . . . . . . 13 (𝑄) = ((2nd ↾ (𝐵 × 𝐶)) ∘ )
4241fveq1i 5425 . . . . . . . . . . . 12 ((𝑄)‘𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧)
4339, 42eqtrdi 2188 . . . . . . . . . . 11 (𝐺 = (𝑄) → (𝐺𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
44433ad2ant3 1004 . . . . . . . . . 10 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) → (𝐺𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
4544ad2antlr 480 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝐺𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧))
46 fvco3 5495 . . . . . . . . . 10 ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘(𝑧)))
4732, 46sylan 281 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ )‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘(𝑧)))
4836fvresd 5449 . . . . . . . . 9 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘(𝑧)) = (2nd ‘(𝑧)))
4945, 47, 483eqtrrd 2177 . . . . . . . 8 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (2nd ‘(𝑧)) = (𝐺𝑧))
50 eqopi 6073 . . . . . . . 8 (((𝑧) ∈ (V × V) ∧ ((1st ‘(𝑧)) = (𝐹𝑧) ∧ (2nd ‘(𝑧)) = (𝐺𝑧))) → (𝑧) = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
5124, 38, 49, 50syl12anc 1214 . . . . . . 7 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝑧) = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
52 fveq2 5424 . . . . . . . . 9 (𝑥 = 𝑧 → (𝐹𝑥) = (𝐹𝑧))
53 fveq2 5424 . . . . . . . . 9 (𝑥 = 𝑧 → (𝐺𝑥) = (𝐺𝑧))
5452, 53opeq12d 3716 . . . . . . . 8 (𝑥 = 𝑧 → ⟨(𝐹𝑥), (𝐺𝑥)⟩ = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
55 simpr 109 . . . . . . . 8 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → 𝑧𝐴)
5651, 36eqeltrrd 2217 . . . . . . . 8 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝐵 × 𝐶))
5715, 54, 55, 56fvmptd3 5517 . . . . . . 7 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧) = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
5851, 57eqtr4d 2175 . . . . . 6 ((((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) ∧ 𝑧𝐴) → (𝑧) = ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧))
597, 19, 58eqfnfvd 5524 . . . . 5 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))) → = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
6059ex 114 . . . 4 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) → = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
61 ffn 5275 . . . . . . . . 9 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
62613ad2ant2 1003 . . . . . . . 8 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐹 Fn 𝐴)
63 fo1st 6058 . . . . . . . . . . 11 1st :V–onto→V
64 fofn 5350 . . . . . . . . . . 11 (1st :V–onto→V → 1st Fn V)
6563, 64ax-mp 5 . . . . . . . . . 10 1st Fn V
66 ssv 3119 . . . . . . . . . 10 (𝐵 × 𝐶) ⊆ V
67 fnssres 5239 . . . . . . . . . 10 ((1st Fn V ∧ (𝐵 × 𝐶) ⊆ V) → (1st ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶))
6865, 66, 67mp2an 422 . . . . . . . . 9 (1st ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶)
6917frnd 5285 . . . . . . . . 9 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ran (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ⊆ (𝐵 × 𝐶))
70 fnco 5234 . . . . . . . . 9 (((1st ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶) ∧ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴 ∧ ran (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ⊆ (𝐵 × 𝐶)) → ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝐴)
7168, 18, 69, 70mp3an2i 1320 . . . . . . . 8 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝐴)
72 fvco3 5495 . . . . . . . . . 10 (((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
7317, 72sylan 281 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
74 simpr 109 . . . . . . . . . . 11 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → 𝑧𝐴)
75 simpl2 985 . . . . . . . . . . . . 13 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → 𝐹:𝐴𝐵)
7675, 74ffvelrnd 5559 . . . . . . . . . . . 12 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
77 simpl3 986 . . . . . . . . . . . . 13 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → 𝐺:𝐴𝐶)
7877, 74ffvelrnd 5559 . . . . . . . . . . . 12 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (𝐺𝑧) ∈ 𝐶)
7976, 78opelxpd 4575 . . . . . . . . . . 11 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝐵 × 𝐶))
8015, 54, 74, 79fvmptd3 5517 . . . . . . . . . 10 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧) = ⟨(𝐹𝑧), (𝐺𝑧)⟩)
8180fveq2d 5428 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((1st ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)) = ((1st ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
82 ffvelrn 5556 . . . . . . . . . . . . . 14 ((𝐹:𝐴𝐵𝑧𝐴) → (𝐹𝑧) ∈ 𝐵)
83 ffvelrn 5556 . . . . . . . . . . . . . 14 ((𝐺:𝐴𝐶𝑧𝐴) → (𝐺𝑧) ∈ 𝐶)
84 opelxpi 4574 . . . . . . . . . . . . . 14 (((𝐹𝑧) ∈ 𝐵 ∧ (𝐺𝑧) ∈ 𝐶) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝐵 × 𝐶))
8582, 83, 84syl2an 287 . . . . . . . . . . . . 13 (((𝐹:𝐴𝐵𝑧𝐴) ∧ (𝐺:𝐴𝐶𝑧𝐴)) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝐵 × 𝐶))
8685anandirs 582 . . . . . . . . . . . 12 (((𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝐵 × 𝐶))
87863adantl1 1137 . . . . . . . . . . 11 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ⟨(𝐹𝑧), (𝐺𝑧)⟩ ∈ (𝐵 × 𝐶))
8887fvresd 5449 . . . . . . . . . 10 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((1st ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (1st ‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
89 op1stg 6051 . . . . . . . . . . 11 (((𝐹𝑧) ∈ 𝐵 ∧ (𝐺𝑧) ∈ 𝐶) → (1st ‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐹𝑧))
9076, 78, 89syl2anc 408 . . . . . . . . . 10 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (1st ‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐹𝑧))
9188, 90eqtrd 2172 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((1st ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐹𝑧))
9273, 81, 913eqtrrd 2177 . . . . . . . 8 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (𝐹𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧))
9362, 71, 92eqfnfvd 5524 . . . . . . 7 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐹 = ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
9426coeq1i 4701 . . . . . . 7 (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) = ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
9593, 94eqtr4di 2190 . . . . . 6 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐹 = (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
96 ffn 5275 . . . . . . . . 9 (𝐺:𝐴𝐶𝐺 Fn 𝐴)
97963ad2ant3 1004 . . . . . . . 8 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐺 Fn 𝐴)
98 fo2nd 6059 . . . . . . . . . . 11 2nd :V–onto→V
99 fofn 5350 . . . . . . . . . . 11 (2nd :V–onto→V → 2nd Fn V)
10098, 99ax-mp 5 . . . . . . . . . 10 2nd Fn V
101 fnssres 5239 . . . . . . . . . 10 ((2nd Fn V ∧ (𝐵 × 𝐶) ⊆ V) → (2nd ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶))
102100, 66, 101mp2an 422 . . . . . . . . 9 (2nd ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶)
103 fnco 5234 . . . . . . . . 9 (((2nd ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶) ∧ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) Fn 𝐴 ∧ ran (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) ⊆ (𝐵 × 𝐶)) → ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝐴)
104102, 18, 69, 103mp3an2i 1320 . . . . . . . 8 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) Fn 𝐴)
105 fvco3 5495 . . . . . . . . . 10 (((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶) ∧ 𝑧𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
10617, 105sylan 281 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)))
10780fveq2d 5428 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)‘𝑧)) = ((2nd ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
10887fvresd 5449 . . . . . . . . . 10 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (2nd ‘⟨(𝐹𝑧), (𝐺𝑧)⟩))
109 op2ndg 6052 . . . . . . . . . . 11 (((𝐹𝑧) ∈ 𝐵 ∧ (𝐺𝑧) ∈ 𝐶) → (2nd ‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐺𝑧))
11076, 78, 109syl2anc 408 . . . . . . . . . 10 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (2nd ‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐺𝑧))
111108, 110eqtrd 2172 . . . . . . . . 9 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘⟨(𝐹𝑧), (𝐺𝑧)⟩) = (𝐺𝑧))
112106, 107, 1113eqtrrd 2177 . . . . . . . 8 (((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) ∧ 𝑧𝐴) → (𝐺𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))‘𝑧))
11397, 104, 112eqfnfvd 5524 . . . . . . 7 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐺 = ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
11440coeq1i 4701 . . . . . . 7 (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) = ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))
115113, 114eqtr4di 2190 . . . . . 6 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → 𝐺 = (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
11617, 95, 1153jca 1161 . . . . 5 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) ∧ 𝐺 = (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))))
117 feq1 5258 . . . . . 6 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (:𝐴⟶(𝐵 × 𝐶) ↔ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶)))
118 coeq2 4700 . . . . . . 7 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝑃) = (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
119118eqeq2d 2151 . . . . . 6 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝐹 = (𝑃) ↔ 𝐹 = (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))))
120 coeq2 4700 . . . . . . 7 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝑄) = (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
121120eqeq2d 2151 . . . . . 6 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (𝐺 = (𝑄) ↔ 𝐺 = (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩))))
122117, 119, 1213anbi123d 1290 . . . . 5 ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ↔ ((𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩):𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)) ∧ 𝐺 = (𝑄 ∘ (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))))
123116, 122syl5ibrcom 156 . . . 4 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ( = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩) → (:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄))))
12460, 123impbid 128 . . 3 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ((:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ↔ = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
125124eubidv 2007 . 2 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → (∃!(:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)) ↔ ∃! = (𝑥𝐴 ↦ ⟨(𝐹𝑥), (𝐺𝑥)⟩)))
1264, 125mpbird 166 1 ((𝐴𝐷𝐹:𝐴𝐵𝐺:𝐴𝐶) → ∃!(:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃) ∧ 𝐺 = (𝑄)))
 Colors of variables: wff set class Syntax hints:   → wi 4   ∧ wa 103   ∧ w3a 962   = wceq 1331   ∈ wcel 1480  ∃!weu 1999  ∀wral 2416  Vcvv 2686   ⊆ wss 3071  ⟨cop 3530   ↦ cmpt 3992   × cxp 4540  ran crn 4543   ↾ cres 4544   ∘ ccom 4546   Fn wfn 5121  ⟶wf 5122  –onto→wfo 5124  ‘cfv 5126  1st c1st 6039  2nd c2nd 6040 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4046  ax-sep 4049  ax-pow 4101  ax-pr 4134  ax-un 4358 This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3740  df-iun 3818  df-br 3933  df-opab 3993  df-mpt 3994  df-id 4218  df-xp 4548  df-rel 4549  df-cnv 4550  df-co 4551  df-dm 4552  df-rn 4553  df-res 4554  df-ima 4555  df-iota 5091  df-fun 5128  df-fn 5129  df-f 5130  df-f1 5131  df-fo 5132  df-f1o 5133  df-fv 5134  df-1st 6041  df-2nd 6042 This theorem is referenced by:  uptx  12469  txcn  12470
 Copyright terms: Public domain W3C validator