Step | Hyp | Ref
| Expression |
1 | | catpropd.1 |
. . . . . 6
⊢ (𝜑 → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
2 | 1 | homfeqbas 17576 |
. . . . 5
⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷)) |
3 | 2 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (Base‘𝐶) = (Base‘𝐷)) |
4 | | eqid 2736 |
. . . . . . . . . 10
⊢
(Base‘𝐶) =
(Base‘𝐶) |
5 | | eqid 2736 |
. . . . . . . . . 10
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
6 | | eqid 2736 |
. . . . . . . . . 10
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
7 | 1 | ad4antr 730 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
8 | | simpr 485 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶)) |
9 | | simpllr 774 |
. . . . . . . . . 10
⊢
(((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
10 | 4, 5, 6, 7, 8, 9 | homfeqval 17577 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐷)𝑥)) |
11 | | eqid 2736 |
. . . . . . . . . . 11
⊢
(comp‘𝐶) =
(comp‘𝐶) |
12 | | eqid 2736 |
. . . . . . . . . . 11
⊢
(comp‘𝐷) =
(comp‘𝐷) |
13 | 1 | ad5antr 732 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
14 | | catpropd.2 |
. . . . . . . . . . . 12
⊢ (𝜑 →
(compf‘𝐶) = (compf‘𝐷)) |
15 | 14 | ad5antr 732 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) →
(compf‘𝐶) = (compf‘𝐷)) |
16 | | simplr 767 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑦 ∈ (Base‘𝐶)) |
17 | | simp-4r 782 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑥 ∈ (Base‘𝐶)) |
18 | | simpr 485 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) |
19 | | simpllr 774 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) |
20 | 4, 5, 11, 12, 13, 15, 16, 17, 17, 18, 19 | comfeqval 17588 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = (𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓)) |
21 | 20 | eqeq1d 2738 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → ((𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ (𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓)) |
22 | 10, 21 | raleqbidva 3321 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓)) |
23 | 4, 5, 6, 7, 9, 8 | homfeqval 17577 |
. . . . . . . . 9
⊢
(((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦)) |
24 | 7 | adantr 481 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
25 | 14 | ad5antr 732 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) →
(compf‘𝐶) = (compf‘𝐷)) |
26 | 9 | adantr 481 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶)) |
27 | | simplr 767 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶)) |
28 | | simpllr 774 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) |
29 | | simpr 485 |
. . . . . . . . . . 11
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) |
30 | 4, 5, 11, 12, 24, 25, 26, 26, 27, 28, 29 | comfeqval 17588 |
. . . . . . . . . 10
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = (𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔)) |
31 | 30 | eqeq1d 2738 |
. . . . . . . . 9
⊢
((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ (𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓)) |
32 | 23, 31 | raleqbidva 3321 |
. . . . . . . 8
⊢
(((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓)) |
33 | 22, 32 | anbi12d 631 |
. . . . . . 7
⊢
(((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → ((∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓))) |
34 | 33 | ralbidva 3172 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓))) |
35 | 34 | riotabidva 7333 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓)) = (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓))) |
36 | 1 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (Homf
‘𝐶) =
(Homf ‘𝐷)) |
37 | | simpr 485 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶)) |
38 | 4, 5, 6, 36, 37, 37 | homfeqval 17577 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑥) = (𝑥(Hom ‘𝐷)𝑥)) |
39 | 2 | ad2antrr 724 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷)) |
40 | 39 | raleqdv 3313 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓))) |
41 | 38, 40 | riotaeqbidv 7316 |
. . . . 5
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓)) = (℩𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓))) |
42 | 35, 41 | eqtrd 2776 |
. . . 4
⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓)) = (℩𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓))) |
43 | 3, 42 | mpteq12dva 5194 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝑥 ∈ (Base‘𝐶) ↦ (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓))) = (𝑥 ∈ (Base‘𝐷) ↦ (℩𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓)))) |
44 | | simpr 485 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐶 ∈ Cat) |
45 | | eqid 2736 |
. . . 4
⊢
(Id‘𝐶) =
(Id‘𝐶) |
46 | 4, 5, 11, 44, 45 | cidfval 17556 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (Id‘𝐶) = (𝑥 ∈ (Base‘𝐶) ↦ (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐶)𝑦)𝑔) = 𝑓)))) |
47 | | eqid 2736 |
. . . 4
⊢
(Base‘𝐷) =
(Base‘𝐷) |
48 | | catpropd.3 |
. . . . . 6
⊢ (𝜑 → 𝐶 ∈ 𝑉) |
49 | | catpropd.4 |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ 𝑊) |
50 | 1, 14, 48, 49 | catpropd 17589 |
. . . . 5
⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat)) |
51 | 50 | biimpa 477 |
. . . 4
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐷 ∈ Cat) |
52 | | eqid 2736 |
. . . 4
⊢
(Id‘𝐷) =
(Id‘𝐷) |
53 | 47, 6, 12, 51, 52 | cidfval 17556 |
. . 3
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (Id‘𝐷) = (𝑥 ∈ (Base‘𝐷) ↦ (℩𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(〈𝑦, 𝑥〉(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(〈𝑥, 𝑥〉(comp‘𝐷)𝑦)𝑔) = 𝑓)))) |
54 | 43, 46, 53 | 3eqtr4d 2786 |
. 2
⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (Id‘𝐶) = (Id‘𝐷)) |
55 | | simpr 485 |
. . . . 5
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → ¬ 𝐶 ∈ Cat) |
56 | | cidffn 17558 |
. . . . . . 7
⊢ Id Fn
Cat |
57 | 56 | fndmi 6606 |
. . . . . 6
⊢ dom Id =
Cat |
58 | 57 | eleq2i 2829 |
. . . . 5
⊢ (𝐶 ∈ dom Id ↔ 𝐶 ∈ Cat) |
59 | 55, 58 | sylnibr 328 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → ¬ 𝐶 ∈ dom Id) |
60 | | ndmfv 6877 |
. . . 4
⊢ (¬
𝐶 ∈ dom Id →
(Id‘𝐶) =
∅) |
61 | 59, 60 | syl 17 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → (Id‘𝐶) = ∅) |
62 | 57 | eleq2i 2829 |
. . . . . . 7
⊢ (𝐷 ∈ dom Id ↔ 𝐷 ∈ Cat) |
63 | 50, 62 | bitr4di 288 |
. . . . . 6
⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ dom Id)) |
64 | 63 | notbid 317 |
. . . . 5
⊢ (𝜑 → (¬ 𝐶 ∈ Cat ↔ ¬ 𝐷 ∈ dom Id)) |
65 | 64 | biimpa 477 |
. . . 4
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → ¬ 𝐷 ∈ dom Id) |
66 | | ndmfv 6877 |
. . . 4
⊢ (¬
𝐷 ∈ dom Id →
(Id‘𝐷) =
∅) |
67 | 65, 66 | syl 17 |
. . 3
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → (Id‘𝐷) = ∅) |
68 | 61, 67 | eqtr4d 2779 |
. 2
⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → (Id‘𝐶) = (Id‘𝐷)) |
69 | 54, 68 | pm2.61dan 811 |
1
⊢ (𝜑 → (Id‘𝐶) = (Id‘𝐷)) |