| Step | Hyp | Ref
| Expression |
| 1 | | mptexg 7241 |
. . . 4
⊢ (𝐴 ∈ 𝐷 → (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ V) |
| 2 | | eueq 3714 |
. . . 4
⊢ ((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ∈ V ↔ ∃!ℎ ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) |
| 3 | 1, 2 | sylib 218 |
. . 3
⊢ (𝐴 ∈ 𝐷 → ∃!ℎ ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) |
| 4 | 3 | 3ad2ant1 1134 |
. 2
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ∃!ℎ ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) |
| 5 | | ffn 6736 |
. . . . . . . 8
⊢ (ℎ:𝐴⟶(𝐵 × 𝐶) → ℎ Fn 𝐴) |
| 6 | 5 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) → ℎ Fn 𝐴) |
| 7 | 6 | adantl 481 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → ℎ Fn 𝐴) |
| 8 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ 𝐵) |
| 9 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝐺:𝐴⟶𝐶 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ 𝐶) |
| 10 | | opelxpi 5722 |
. . . . . . . . . . . . 13
⊢ (((𝐹‘𝑥) ∈ 𝐵 ∧ (𝐺‘𝑥) ∈ 𝐶) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶)) |
| 11 | 8, 9, 10 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑥 ∈ 𝐴) ∧ (𝐺:𝐴⟶𝐶 ∧ 𝑥 ∈ 𝐴)) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶)) |
| 12 | 11 | anandirs 679 |
. . . . . . . . . . 11
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑥 ∈ 𝐴) → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶)) |
| 13 | 12 | ralrimiva 3146 |
. . . . . . . . . 10
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ∀𝑥 ∈ 𝐴 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶)) |
| 14 | 13 | 3adant1 1131 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ∀𝑥 ∈ 𝐴 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶)) |
| 15 | | eqid 2737 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) |
| 16 | 15 | fmpt 7130 |
. . . . . . . . 9
⊢
(∀𝑥 ∈
𝐴 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 ∈ (𝐵 × 𝐶) ↔ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):𝐴⟶(𝐵 × 𝐶)) |
| 17 | 14, 16 | sylib 218 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):𝐴⟶(𝐵 × 𝐶)) |
| 18 | 17 | ffnd 6737 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn 𝐴) |
| 19 | 18 | adantr 480 |
. . . . . 6
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn 𝐴) |
| 20 | | xpss 5701 |
. . . . . . . . . . 11
⊢ (𝐵 × 𝐶) ⊆ (V × V) |
| 21 | | ffvelcdm 7101 |
. . . . . . . . . . 11
⊢ ((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧 ∈ 𝐴) → (ℎ‘𝑧) ∈ (𝐵 × 𝐶)) |
| 22 | 20, 21 | sselid 3981 |
. . . . . . . . . 10
⊢ ((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧 ∈ 𝐴) → (ℎ‘𝑧) ∈ (V × V)) |
| 23 | 22 | 3ad2antl1 1186 |
. . . . . . . . 9
⊢ (((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ∧ 𝑧 ∈ 𝐴) → (ℎ‘𝑧) ∈ (V × V)) |
| 24 | 23 | adantll 714 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → (ℎ‘𝑧) ∈ (V × V)) |
| 25 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝐹 = (𝑃 ∘ ℎ) → (𝐹‘𝑧) = ((𝑃 ∘ ℎ)‘𝑧)) |
| 26 | | upxp.1 |
. . . . . . . . . . . . . 14
⊢ 𝑃 = (1st ↾
(𝐵 × 𝐶)) |
| 27 | 26 | coeq1i 5870 |
. . . . . . . . . . . . 13
⊢ (𝑃 ∘ ℎ) = ((1st ↾ (𝐵 × 𝐶)) ∘ ℎ) |
| 28 | 27 | fveq1i 6907 |
. . . . . . . . . . . 12
⊢ ((𝑃 ∘ ℎ)‘𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧) |
| 29 | 25, 28 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝐹 = (𝑃 ∘ ℎ) → (𝐹‘𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧)) |
| 30 | 29 | 3ad2ant2 1135 |
. . . . . . . . . 10
⊢ ((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) → (𝐹‘𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧)) |
| 31 | 30 | ad2antlr 727 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧)) |
| 32 | | simpr1 1195 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → ℎ:𝐴⟶(𝐵 × 𝐶)) |
| 33 | | fvco3 7008 |
. . . . . . . . . 10
⊢ ((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧 ∈ 𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘(ℎ‘𝑧))) |
| 34 | 32, 33 | sylan 580 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘(ℎ‘𝑧))) |
| 35 | 21 | 3ad2antl1 1186 |
. . . . . . . . . . 11
⊢ (((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ∧ 𝑧 ∈ 𝐴) → (ℎ‘𝑧) ∈ (𝐵 × 𝐶)) |
| 36 | 35 | adantll 714 |
. . . . . . . . . 10
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → (ℎ‘𝑧) ∈ (𝐵 × 𝐶)) |
| 37 | 36 | fvresd 6926 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → ((1st ↾ (𝐵 × 𝐶))‘(ℎ‘𝑧)) = (1st ‘(ℎ‘𝑧))) |
| 38 | 31, 34, 37 | 3eqtrrd 2782 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → (1st ‘(ℎ‘𝑧)) = (𝐹‘𝑧)) |
| 39 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝐺 = (𝑄 ∘ ℎ) → (𝐺‘𝑧) = ((𝑄 ∘ ℎ)‘𝑧)) |
| 40 | | upxp.2 |
. . . . . . . . . . . . . 14
⊢ 𝑄 = (2nd ↾
(𝐵 × 𝐶)) |
| 41 | 40 | coeq1i 5870 |
. . . . . . . . . . . . 13
⊢ (𝑄 ∘ ℎ) = ((2nd ↾ (𝐵 × 𝐶)) ∘ ℎ) |
| 42 | 41 | fveq1i 6907 |
. . . . . . . . . . . 12
⊢ ((𝑄 ∘ ℎ)‘𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧) |
| 43 | 39, 42 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝐺 = (𝑄 ∘ ℎ) → (𝐺‘𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧)) |
| 44 | 43 | 3ad2ant3 1136 |
. . . . . . . . . 10
⊢ ((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) → (𝐺‘𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧)) |
| 45 | 44 | ad2antlr 727 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧)) |
| 46 | | fvco3 7008 |
. . . . . . . . . 10
⊢ ((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝑧 ∈ 𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘(ℎ‘𝑧))) |
| 47 | 32, 46 | sylan 580 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ ℎ)‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘(ℎ‘𝑧))) |
| 48 | 36 | fvresd 6926 |
. . . . . . . . 9
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘(ℎ‘𝑧)) = (2nd ‘(ℎ‘𝑧))) |
| 49 | 45, 47, 48 | 3eqtrrd 2782 |
. . . . . . . 8
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → (2nd ‘(ℎ‘𝑧)) = (𝐺‘𝑧)) |
| 50 | | eqopi 8050 |
. . . . . . . 8
⊢ (((ℎ‘𝑧) ∈ (V × V) ∧ ((1st
‘(ℎ‘𝑧)) = (𝐹‘𝑧) ∧ (2nd ‘(ℎ‘𝑧)) = (𝐺‘𝑧))) → (ℎ‘𝑧) = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) |
| 51 | 24, 38, 49, 50 | syl12anc 837 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → (ℎ‘𝑧) = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) |
| 52 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝐹‘𝑥) = (𝐹‘𝑧)) |
| 53 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑧 → (𝐺‘𝑥) = (𝐺‘𝑧)) |
| 54 | 52, 53 | opeq12d 4881 |
. . . . . . . . 9
⊢ (𝑥 = 𝑧 → 〈(𝐹‘𝑥), (𝐺‘𝑥)〉 = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) |
| 55 | | opex 5469 |
. . . . . . . . 9
⊢
〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ V |
| 56 | 54, 15, 55 | fvmpt 7016 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝐴 → ((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧) = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) |
| 57 | 56 | adantl 481 |
. . . . . . 7
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧) = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) |
| 58 | 51, 57 | eqtr4d 2780 |
. . . . . 6
⊢ ((((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) ∧ 𝑧 ∈ 𝐴) → (ℎ‘𝑧) = ((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧)) |
| 59 | 7, 19, 58 | eqfnfvd 7054 |
. . . . 5
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) → ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) |
| 60 | 59 | ex 412 |
. . . 4
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) → ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
| 61 | | ffn 6736 |
. . . . . . . . 9
⊢ (𝐹:𝐴⟶𝐵 → 𝐹 Fn 𝐴) |
| 62 | 61 | 3ad2ant2 1135 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → 𝐹 Fn 𝐴) |
| 63 | | fo1st 8034 |
. . . . . . . . . . 11
⊢
1st :V–onto→V |
| 64 | | fofn 6822 |
. . . . . . . . . . 11
⊢
(1st :V–onto→V → 1st Fn V) |
| 65 | 63, 64 | ax-mp 5 |
. . . . . . . . . 10
⊢
1st Fn V |
| 66 | | ssv 4008 |
. . . . . . . . . 10
⊢ (𝐵 × 𝐶) ⊆ V |
| 67 | | fnssres 6691 |
. . . . . . . . . 10
⊢
((1st Fn V ∧ (𝐵 × 𝐶) ⊆ V) → (1st ↾
(𝐵 × 𝐶)) Fn (𝐵 × 𝐶)) |
| 68 | 65, 66, 67 | mp2an 692 |
. . . . . . . . 9
⊢
(1st ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶) |
| 69 | 17 | frnd 6744 |
. . . . . . . . 9
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ran (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⊆ (𝐵 × 𝐶)) |
| 70 | | fnco 6686 |
. . . . . . . . 9
⊢
(((1st ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶) ∧ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn 𝐴 ∧ ran (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⊆ (𝐵 × 𝐶)) → ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn 𝐴) |
| 71 | 68, 18, 69, 70 | mp3an2i 1468 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn 𝐴) |
| 72 | | fvco3 7008 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):𝐴⟶(𝐵 × 𝐶) ∧ 𝑧 ∈ 𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) |
| 73 | 17, 72 | sylan 580 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → (((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((1st ↾ (𝐵 × 𝐶))‘((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) |
| 74 | 56 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → ((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧) = 〈(𝐹‘𝑧), (𝐺‘𝑧)〉) |
| 75 | 74 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → ((1st ↾ (𝐵 × 𝐶))‘((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧)) = ((1st ↾ (𝐵 × 𝐶))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) |
| 76 | | ffvelcdm 7101 |
. . . . . . . . . . . . . 14
⊢ ((𝐹:𝐴⟶𝐵 ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) ∈ 𝐵) |
| 77 | | ffvelcdm 7101 |
. . . . . . . . . . . . . 14
⊢ ((𝐺:𝐴⟶𝐶 ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) ∈ 𝐶) |
| 78 | | opelxpi 5722 |
. . . . . . . . . . . . . 14
⊢ (((𝐹‘𝑧) ∈ 𝐵 ∧ (𝐺‘𝑧) ∈ 𝐶) → 〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝐵 × 𝐶)) |
| 79 | 76, 77, 78 | syl2an 596 |
. . . . . . . . . . . . 13
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝑧 ∈ 𝐴) ∧ (𝐺:𝐴⟶𝐶 ∧ 𝑧 ∈ 𝐴)) → 〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝐵 × 𝐶)) |
| 80 | 79 | anandirs 679 |
. . . . . . . . . . . 12
⊢ (((𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → 〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝐵 × 𝐶)) |
| 81 | 80 | 3adantl1 1167 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → 〈(𝐹‘𝑧), (𝐺‘𝑧)〉 ∈ (𝐵 × 𝐶)) |
| 82 | 81 | fvresd 6926 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → ((1st ↾ (𝐵 × 𝐶))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (1st
‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) |
| 83 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝐹‘𝑧) ∈ V |
| 84 | | fvex 6919 |
. . . . . . . . . . 11
⊢ (𝐺‘𝑧) ∈ V |
| 85 | 83, 84 | op1st 8022 |
. . . . . . . . . 10
⊢
(1st ‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐹‘𝑧) |
| 86 | 82, 85 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → ((1st ↾ (𝐵 × 𝐶))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐹‘𝑧)) |
| 87 | 73, 75, 86 | 3eqtrrd 2782 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → (𝐹‘𝑧) = (((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧)) |
| 88 | 62, 71, 87 | eqfnfvd 7054 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → 𝐹 = ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
| 89 | 26 | coeq1i 5870 |
. . . . . . 7
⊢ (𝑃 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) = ((1st ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) |
| 90 | 88, 89 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → 𝐹 = (𝑃 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
| 91 | | ffn 6736 |
. . . . . . . . 9
⊢ (𝐺:𝐴⟶𝐶 → 𝐺 Fn 𝐴) |
| 92 | 91 | 3ad2ant3 1136 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → 𝐺 Fn 𝐴) |
| 93 | | fo2nd 8035 |
. . . . . . . . . . 11
⊢
2nd :V–onto→V |
| 94 | | fofn 6822 |
. . . . . . . . . . 11
⊢
(2nd :V–onto→V → 2nd Fn V) |
| 95 | 93, 94 | ax-mp 5 |
. . . . . . . . . 10
⊢
2nd Fn V |
| 96 | | fnssres 6691 |
. . . . . . . . . 10
⊢
((2nd Fn V ∧ (𝐵 × 𝐶) ⊆ V) → (2nd ↾
(𝐵 × 𝐶)) Fn (𝐵 × 𝐶)) |
| 97 | 95, 66, 96 | mp2an 692 |
. . . . . . . . 9
⊢
(2nd ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶) |
| 98 | | fnco 6686 |
. . . . . . . . 9
⊢
(((2nd ↾ (𝐵 × 𝐶)) Fn (𝐵 × 𝐶) ∧ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) Fn 𝐴 ∧ ran (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) ⊆ (𝐵 × 𝐶)) → ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn 𝐴) |
| 99 | 97, 18, 69, 98 | mp3an2i 1468 |
. . . . . . . 8
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) Fn 𝐴) |
| 100 | | fvco3 7008 |
. . . . . . . . . 10
⊢ (((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):𝐴⟶(𝐵 × 𝐶) ∧ 𝑧 ∈ 𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) |
| 101 | 17, 100 | sylan 580 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → (((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧) = ((2nd ↾ (𝐵 × 𝐶))‘((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧))) |
| 102 | 74 | fveq2d 6910 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)‘𝑧)) = ((2nd ↾ (𝐵 × 𝐶))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) |
| 103 | 81 | fvresd 6926 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (2nd
‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉)) |
| 104 | 83, 84 | op2nd 8023 |
. . . . . . . . . 10
⊢
(2nd ‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐺‘𝑧) |
| 105 | 103, 104 | eqtrdi 2793 |
. . . . . . . . 9
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → ((2nd ↾ (𝐵 × 𝐶))‘〈(𝐹‘𝑧), (𝐺‘𝑧)〉) = (𝐺‘𝑧)) |
| 106 | 101, 102,
105 | 3eqtrrd 2782 |
. . . . . . . 8
⊢ (((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) ∧ 𝑧 ∈ 𝐴) → (𝐺‘𝑧) = (((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))‘𝑧)) |
| 107 | 92, 99, 106 | eqfnfvd 7054 |
. . . . . . 7
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → 𝐺 = ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
| 108 | 40 | coeq1i 5870 |
. . . . . . 7
⊢ (𝑄 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) = ((2nd ↾ (𝐵 × 𝐶)) ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) |
| 109 | 107, 108 | eqtr4di 2795 |
. . . . . 6
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → 𝐺 = (𝑄 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
| 110 | 17, 90, 109 | 3jca 1129 |
. . . . 5
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) ∧ 𝐺 = (𝑄 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)))) |
| 111 | | feq1 6716 |
. . . . . 6
⊢ (ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (ℎ:𝐴⟶(𝐵 × 𝐶) ↔ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):𝐴⟶(𝐵 × 𝐶))) |
| 112 | | coeq2 5869 |
. . . . . . 7
⊢ (ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝑃 ∘ ℎ) = (𝑃 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
| 113 | 112 | eqeq2d 2748 |
. . . . . 6
⊢ (ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝐹 = (𝑃 ∘ ℎ) ↔ 𝐹 = (𝑃 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)))) |
| 114 | | coeq2 5869 |
. . . . . . 7
⊢ (ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝑄 ∘ ℎ) = (𝑄 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
| 115 | 114 | eqeq2d 2748 |
. . . . . 6
⊢ (ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (𝐺 = (𝑄 ∘ ℎ) ↔ 𝐺 = (𝑄 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)))) |
| 116 | 111, 113,
115 | 3anbi123d 1438 |
. . . . 5
⊢ (ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → ((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ↔ ((𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉):𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉)) ∧ 𝐺 = (𝑄 ∘ (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))))) |
| 117 | 110, 116 | syl5ibrcom 247 |
. . . 4
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → (ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉) → (ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)))) |
| 118 | 60, 117 | impbid 212 |
. . 3
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ((ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ↔ ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
| 119 | 118 | eubidv 2586 |
. 2
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → (∃!ℎ(ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ)) ↔ ∃!ℎ ℎ = (𝑥 ∈ 𝐴 ↦ 〈(𝐹‘𝑥), (𝐺‘𝑥)〉))) |
| 120 | 4, 119 | mpbird 257 |
1
⊢ ((𝐴 ∈ 𝐷 ∧ 𝐹:𝐴⟶𝐵 ∧ 𝐺:𝐴⟶𝐶) → ∃!ℎ(ℎ:𝐴⟶(𝐵 × 𝐶) ∧ 𝐹 = (𝑃 ∘ ℎ) ∧ 𝐺 = (𝑄 ∘ ℎ))) |