| Step | Hyp | Ref
| Expression |
| 1 | | hofpropd.1 |
. . 3
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
| 2 | 1 | homfeqbas 17739 |
. . . . 5
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) |
| 3 | 2 | sqxpeqd 5717 |
. . . 4
⊢ (𝜑 → ((Base‘𝐶) × (Base‘𝐶)) = ((Base‘𝐷) × (Base‘𝐷))) |
| 4 | 3 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Base‘𝐶) × (Base‘𝐶)) = ((Base‘𝐷) × (Base‘𝐷))) |
| 5 | | eqid 2737 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
| 6 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
| 7 | | eqid 2737 |
. . . . . 6
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
| 8 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
| 9 | | xp1st 8046 |
. . . . . . 7
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st
‘𝑦) ∈
(Base‘𝐶)) |
| 10 | 9 | ad2antll 729 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (1st ‘𝑦) ∈ (Base‘𝐶)) |
| 11 | | xp1st 8046 |
. . . . . . 7
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1st
‘𝑥) ∈
(Base‘𝐶)) |
| 12 | 11 | ad2antrl 728 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (1st ‘𝑥) ∈ (Base‘𝐶)) |
| 13 | 5, 6, 7, 8, 10, 12 | homfeqval 17740 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) = ((1st ‘𝑦)(Hom ‘𝐷)(1st ‘𝑥))) |
| 14 | | xp2nd 8047 |
. . . . . . . 8
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd
‘𝑥) ∈
(Base‘𝐶)) |
| 15 | 14 | ad2antrl 728 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (2nd ‘𝑥) ∈ (Base‘𝐶)) |
| 16 | | xp2nd 8047 |
. . . . . . . 8
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2nd
‘𝑦) ∈
(Base‘𝐶)) |
| 17 | 16 | ad2antll 729 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (2nd ‘𝑦) ∈ (Base‘𝐶)) |
| 18 | 5, 6, 7, 8, 15, 17 | homfeqval 17740 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) = ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦))) |
| 19 | 18 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ 𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))) → ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) = ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦))) |
| 20 | 5, 6, 7, 8, 12, 15 | homfeqval 17740 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) = ((1st ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑥))) |
| 21 | | df-ov 7434 |
. . . . . . . . 9
⊢
((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)) = ((Hom ‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
| 22 | | df-ov 7434 |
. . . . . . . . 9
⊢
((1st ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑥)) = ((Hom ‘𝐷)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
| 23 | 20, 21, 22 | 3eqtr3g 2800 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉) = ((Hom ‘𝐷)‘〈(1st
‘𝑥), (2nd
‘𝑥)〉)) |
| 24 | | 1st2nd2 8053 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
| 25 | 24 | ad2antrl 728 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
| 26 | 25 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
| 27 | 25 | fveq2d 6910 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐷)‘𝑥) = ((Hom ‘𝐷)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
| 28 | 23, 26, 27 | 3eqtr4d 2787 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐷)‘𝑥)) |
| 29 | 28 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐷)‘𝑥)) |
| 30 | | eqid 2737 |
. . . . . . . 8
⊢
(comp‘𝐶) =
(comp‘𝐶) |
| 31 | | eqid 2737 |
. . . . . . . 8
⊢
(comp‘𝐷) =
(comp‘𝐷) |
| 32 | 8 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
| 33 | | hofpropd.2 |
. . . . . . . . 9
⊢ (𝜑 →
(compf‘𝐶) = (compf‘𝐷)) |
| 34 | 33 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) →
(compf‘𝐶) = (compf‘𝐷)) |
| 35 | 10 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st ‘𝑦) ∈ (Base‘𝐶)) |
| 36 | 12 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1st ‘𝑥) ∈ (Base‘𝐶)) |
| 37 | 17 | ad2antrr 726 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd ‘𝑦) ∈ (Base‘𝐶)) |
| 38 | | simplrl 777 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥))) |
| 39 | 25 | ad2antrr 726 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑥 = 〈(1st ‘𝑥), (2nd ‘𝑥)〉) |
| 40 | 39 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑥(comp‘𝐶)(2nd ‘𝑦)) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))) |
| 41 | 40 | oveqd 7448 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ) = (𝑔(〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))ℎ)) |
| 42 | | hofpropd.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ Cat) |
| 43 | 42 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝐶 ∈ Cat) |
| 44 | 15 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2nd ‘𝑥) ∈ (Base‘𝐶)) |
| 45 | 26 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘〈(1st ‘𝑥), (2nd ‘𝑥)〉)) |
| 46 | 45, 21 | eqtr4di 2795 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
| 47 | 46 | eleq2d 2827 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↔ ℎ ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥)))) |
| 48 | 47 | biimpa 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ℎ ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑥))) |
| 49 | | simplrr 778 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) |
| 50 | 5, 6, 30, 43, 36, 44, 37, 48, 49 | catcocl 17728 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))ℎ) ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) |
| 51 | 41, 50 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ) ∈ ((1st ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦))) |
| 52 | 5, 6, 30, 31, 32, 34, 35, 36, 37, 38, 51 | comfeqval 17751 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓) = ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))𝑓)) |
| 53 | 5, 6, 30, 31, 32, 34, 36, 44, 37, 48, 49 | comfeqval 17751 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))ℎ) = (𝑔(〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))ℎ)) |
| 54 | 39 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑥(comp‘𝐷)(2nd ‘𝑦)) = (〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))) |
| 55 | 54 | oveqd 7448 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐷)(2nd ‘𝑦))ℎ) = (𝑔(〈(1st ‘𝑥), (2nd ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))ℎ)) |
| 56 | 53, 41, 55 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ) = (𝑔(𝑥(comp‘𝐷)(2nd ‘𝑦))ℎ)) |
| 57 | 56 | oveq1d 7446 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))𝑓) = ((𝑔(𝑥(comp‘𝐷)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))𝑓)) |
| 58 | 52, 57 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓) = ((𝑔(𝑥(comp‘𝐷)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))𝑓)) |
| 59 | 29, 58 | mpteq12dva 5231 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)) ∧ 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)) = (ℎ ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))𝑓))) |
| 60 | 13, 19, 59 | mpoeq123dva 7507 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))) = (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐷)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))𝑓)))) |
| 61 | 3, 4, 60 | mpoeq123dva 7507 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓)))) = (𝑥 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐷)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))𝑓))))) |
| 62 | 1, 61 | opeq12d 4881 |
. 2
⊢ (𝜑 →
〈(Homf ‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))〉 = 〈(Homf
‘𝐷), (𝑥 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐷)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))𝑓))))〉) |
| 63 | | eqid 2737 |
. . 3
⊢
(HomF‘𝐶) = (HomF‘𝐶) |
| 64 | 63, 42, 5, 6, 30 | hofval 18297 |
. 2
⊢ (𝜑 →
(HomF‘𝐶) = 〈(Homf
‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐶)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐶)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐶)(2nd ‘𝑦))𝑓))))〉) |
| 65 | | eqid 2737 |
. . 3
⊢
(HomF‘𝐷) = (HomF‘𝐷) |
| 66 | | hofpropd.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ Cat) |
| 67 | | eqid 2737 |
. . 3
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 68 | 65, 66, 67, 7, 31 | hofval 18297 |
. 2
⊢ (𝜑 →
(HomF‘𝐷) = 〈(Homf
‘𝐷), (𝑥 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ (𝑓 ∈ ((1st ‘𝑦)(Hom ‘𝐷)(1st ‘𝑥)), 𝑔 ∈ ((2nd ‘𝑥)(Hom ‘𝐷)(2nd ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2nd ‘𝑦))ℎ)(〈(1st ‘𝑦), (1st ‘𝑥)〉(comp‘𝐷)(2nd ‘𝑦))𝑓))))〉) |
| 69 | 62, 64, 68 | 3eqtr4d 2787 |
1
⊢ (𝜑 →
(HomF‘𝐶) = (HomF‘𝐷)) |