Step | Hyp | Ref
| Expression |
1 | | hofpropd.1 |
. . 3
⊢ (𝜑 → (Hom_{f}
‘𝐶) =
(Hom_{f} ‘𝐷)) |
2 | 1 | homfeqbas 16715 |
. . . . 5
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) |
3 | 2 | sqxpeqd 5378 |
. . . 4
⊢ (𝜑 → ((Base‘𝐶) × (Base‘𝐶)) = ((Base‘𝐷) × (Base‘𝐷))) |
4 | 3 | adantr 474 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶))) → ((Base‘𝐶) × (Base‘𝐶)) = ((Base‘𝐷) × (Base‘𝐷))) |
5 | | eqid 2825 |
. . . . . 6
⊢
(Base‘𝐶) =
(Base‘𝐶) |
6 | | eqid 2825 |
. . . . . 6
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
7 | | eqid 2825 |
. . . . . 6
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
8 | 1 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (Hom_{f}
‘𝐶) =
(Hom_{f} ‘𝐷)) |
9 | | xp1st 7465 |
. . . . . . 7
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1^{st}
‘𝑦) ∈
(Base‘𝐶)) |
10 | 9 | ad2antll 720 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (1^{st} ‘𝑦) ∈ (Base‘𝐶)) |
11 | | xp1st 7465 |
. . . . . . 7
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (1^{st}
‘𝑥) ∈
(Base‘𝐶)) |
12 | 11 | ad2antrl 719 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (1^{st} ‘𝑥) ∈ (Base‘𝐶)) |
13 | 5, 6, 7, 8, 10, 12 | homfeqval 16716 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) = ((1^{st} ‘𝑦)(Hom ‘𝐷)(1^{st} ‘𝑥))) |
14 | | xp2nd 7466 |
. . . . . . . 8
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2^{nd}
‘𝑥) ∈
(Base‘𝐶)) |
15 | 14 | ad2antrl 719 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (2^{nd} ‘𝑥) ∈ (Base‘𝐶)) |
16 | | xp2nd 7466 |
. . . . . . . 8
⊢ (𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) → (2^{nd}
‘𝑦) ∈
(Base‘𝐶)) |
17 | 16 | ad2antll 720 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (2^{nd} ‘𝑦) ∈ (Base‘𝐶)) |
18 | 5, 6, 7, 8, 15, 17 | homfeqval 16716 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) = ((2^{nd} ‘𝑥)(Hom ‘𝐷)(2^{nd} ‘𝑦))) |
19 | 18 | adantr 474 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ 𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥))) → ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) = ((2^{nd} ‘𝑥)(Hom ‘𝐷)(2^{nd} ‘𝑦))) |
20 | 5, 6, 7, 8, 12, 15 | homfeqval 16716 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) = ((1^{st} ‘𝑥)(Hom ‘𝐷)(2^{nd} ‘𝑥))) |
21 | | df-ov 6913 |
. . . . . . . . 9
⊢
((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)) = ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
22 | | df-ov 6913 |
. . . . . . . . 9
⊢
((1^{st} ‘𝑥)(Hom ‘𝐷)(2^{nd} ‘𝑥)) = ((Hom ‘𝐷)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
23 | 20, 21, 22 | 3eqtr3g 2884 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) = ((Hom ‘𝐷)‘⟨(1^{st}
‘𝑥), (2^{nd}
‘𝑥)⟩)) |
24 | | 1st2nd2 7472 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
25 | 24 | ad2antrl 719 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
26 | 25 | fveq2d 6441 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
27 | 25 | fveq2d 6441 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐷)‘𝑥) = ((Hom ‘𝐷)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
28 | 23, 26, 27 | 3eqtr4d 2871 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐷)‘𝑥)) |
29 | 28 | adantr 474 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐷)‘𝑥)) |
30 | | eqid 2825 |
. . . . . . . 8
⊢
(comp‘𝐶) =
(comp‘𝐶) |
31 | | eqid 2825 |
. . . . . . . 8
⊢
(comp‘𝐷) =
(comp‘𝐷) |
32 | 8 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (Hom_{f}
‘𝐶) =
(Hom_{f} ‘𝐷)) |
33 | | hofpropd.2 |
. . . . . . . . 9
⊢ (𝜑 →
(comp_{f}‘𝐶) = (comp_{f}‘𝐷)) |
34 | 33 | ad3antrrr 721 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) →
(comp_{f}‘𝐶) = (comp_{f}‘𝐷)) |
35 | 10 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1^{st} ‘𝑦) ∈ (Base‘𝐶)) |
36 | 12 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (1^{st} ‘𝑥) ∈ (Base‘𝐶)) |
37 | 17 | ad2antrr 717 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2^{nd} ‘𝑦) ∈ (Base‘𝐶)) |
38 | | simplrl 795 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥))) |
39 | 25 | ad2antrr 717 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑥 = ⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩) |
40 | 39 | oveq1d 6925 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑥(comp‘𝐶)(2^{nd} ‘𝑦)) = (⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))) |
41 | 40 | oveqd 6927 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ) = (𝑔(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)) |
42 | | hofpropd.c |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐶 ∈ Cat) |
43 | 42 | ad3antrrr 721 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝐶 ∈ Cat) |
44 | 15 | ad2antrr 717 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (2^{nd} ‘𝑥) ∈ (Base‘𝐶)) |
45 | 26 | adantr 474 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((Hom ‘𝐶)‘⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩)) |
46 | 45, 21 | syl6eqr 2879 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → ((Hom ‘𝐶)‘𝑥) = ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
47 | 46 | eleq2d 2892 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↔ ℎ ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥)))) |
48 | 47 | biimpa 470 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ℎ ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑥))) |
49 | | simplrr 796 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
50 | 5, 6, 30, 43, 36, 44, 37, 48, 49 | catcocl 16705 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))ℎ) ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
51 | 41, 50 | eqeltrd 2906 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ) ∈ ((1^{st} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦))) |
52 | 5, 6, 30, 31, 32, 34, 35, 36, 37, 38, 51 | comfeqval 16727 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓) = ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))𝑓)) |
53 | 5, 6, 30, 31, 32, 34, 36, 44, 37, 48, 49 | comfeqval 16727 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))ℎ) = (𝑔(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))ℎ)) |
54 | 39 | oveq1d 6925 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑥(comp‘𝐷)(2^{nd} ‘𝑦)) = (⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))) |
55 | 54 | oveqd 6927 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐷)(2^{nd} ‘𝑦))ℎ) = (𝑔(⟨(1^{st} ‘𝑥), (2^{nd} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))ℎ)) |
56 | 53, 41, 55 | 3eqtr4d 2871 |
. . . . . . . 8
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → (𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ) = (𝑔(𝑥(comp‘𝐷)(2^{nd} ‘𝑦))ℎ)) |
57 | 56 | oveq1d 6925 |
. . . . . . 7
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))𝑓) = ((𝑔(𝑥(comp‘𝐷)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))𝑓)) |
58 | 52, 57 | eqtrd 2861 |
. . . . . 6
⊢ ((((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) ∧ ℎ ∈ ((Hom ‘𝐶)‘𝑥)) → ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓) = ((𝑔(𝑥(comp‘𝐷)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))𝑓)) |
59 | 29, 58 | mpteq12dva 4957 |
. . . . 5
⊢ (((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) ∧ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)) ∧ 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)))) → (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)) = (ℎ ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))𝑓))) |
60 | 13, 19, 59 | mpt2eq123dva 6981 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)) ∧ 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)))) → (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))) = (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐷)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐷)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))𝑓)))) |
61 | 3, 4, 60 | mpt2eq123dva 6981 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓)))) = (𝑥 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐷)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐷)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))𝑓))))) |
62 | 1, 61 | opeq12d 4633 |
. 2
⊢ (𝜑 →
⟨(Hom_{f} ‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))))⟩ = ⟨(Hom_{f}
‘𝐷), (𝑥 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐷)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐷)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))𝑓))))⟩) |
63 | | eqid 2825 |
. . 3
⊢
(Hom_{F}‘𝐶) = (Hom_{F}‘𝐶) |
64 | 63, 42, 5, 6, 30 | hofval 17252 |
. 2
⊢ (𝜑 →
(Hom_{F}‘𝐶) = ⟨(Hom_{f}
‘𝐶), (𝑥 ∈ ((Base‘𝐶) × (Base‘𝐶)), 𝑦 ∈ ((Base‘𝐶) × (Base‘𝐶)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐶)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐶)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐶)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐶)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐶)(2^{nd} ‘𝑦))𝑓))))⟩) |
65 | | eqid 2825 |
. . 3
⊢
(Hom_{F}‘𝐷) = (Hom_{F}‘𝐷) |
66 | | hofpropd.d |
. . 3
⊢ (𝜑 → 𝐷 ∈ Cat) |
67 | | eqid 2825 |
. . 3
⊢
(Base‘𝐷) =
(Base‘𝐷) |
68 | 65, 66, 67, 7, 31 | hofval 17252 |
. 2
⊢ (𝜑 →
(Hom_{F}‘𝐷) = ⟨(Hom_{f}
‘𝐷), (𝑥 ∈ ((Base‘𝐷) × (Base‘𝐷)), 𝑦 ∈ ((Base‘𝐷) × (Base‘𝐷)) ↦ (𝑓 ∈ ((1^{st} ‘𝑦)(Hom ‘𝐷)(1^{st} ‘𝑥)), 𝑔 ∈ ((2^{nd} ‘𝑥)(Hom ‘𝐷)(2^{nd} ‘𝑦)) ↦ (ℎ ∈ ((Hom ‘𝐷)‘𝑥) ↦ ((𝑔(𝑥(comp‘𝐷)(2^{nd} ‘𝑦))ℎ)(⟨(1^{st} ‘𝑦), (1^{st} ‘𝑥)⟩(comp‘𝐷)(2^{nd} ‘𝑦))𝑓))))⟩) |
69 | 62, 64, 68 | 3eqtr4d 2871 |
1
⊢ (𝜑 →
(Hom_{F}‘𝐶) = (Hom_{F}‘𝐷)) |