Theorem cidpropd 16972

Description: Two structures with the same base, hom-sets and composition operation have the same identity function. (Contributed by Mario Carneiro, 17-Jan-2017.)

Hypotheses

Ref	Expression
catpropd.1	⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))
catpropd.2	⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))
catpropd.3	⊢ (𝜑 → 𝐶 ∈ 𝑉)
catpropd.4	⊢ (𝜑 → 𝐷 ∈ 𝑊)

Assertion

Ref	Expression
cidpropd	⊢ (𝜑 → (Id‘𝐶) = (Id‘𝐷))

Proof of Theorem cidpropd

Dummy variables 𝑓 𝑔 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		catpropd.1	. . . . . 6 ⊢ (𝜑 → (Homf ‘𝐶) = (Homf ‘𝐷))
2	1	homfeqbas 16958	. . . . 5 ⊢ (𝜑 → (Base‘𝐶) = (Base‘𝐷))
3	2	adantr 484	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (Base‘𝐶) = (Base‘𝐷))
4		eqid 2798	. . . . . . . . . 10 ⊢ (Base‘𝐶) = (Base‘𝐶)
5		eqid 2798	. . . . . . . . . 10 ⊢ (Hom ‘𝐶) = (Hom ‘𝐶)
6		eqid 2798	. . . . . . . . . 10 ⊢ (Hom ‘𝐷) = (Hom ‘𝐷)
7	1	ad4antr 731	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (Homf ‘𝐶) = (Homf ‘𝐷))
8		simpr 488	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑦 ∈ (Base‘𝐶))
9		simpllr 775	. . . . . . . . . 10 ⊢ (((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
10	4, 5, 6, 7, 8, 9	homfeqval 16959	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑦(Hom ‘𝐶)𝑥) = (𝑦(Hom ‘𝐷)𝑥))
11		eqid 2798	. . . . . . . . . . 11 ⊢ (comp‘𝐶) = (comp‘𝐶)
12		eqid 2798	. . . . . . . . . . 11 ⊢ (comp‘𝐷) = (comp‘𝐷)
13	1	ad5antr 733	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (Homf ‘𝐶) = (Homf ‘𝐷))
14		catpropd.2	. . . . . . . . . . . 12 ⊢ (𝜑 → (compf‘𝐶) = (compf‘𝐷))
15	14	ad5antr 733	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (compf‘𝐶) = (compf‘𝐷))
16		simplr 768	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑦 ∈ (Base‘𝐶))
17		simp-4r 783	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑥 ∈ (Base‘𝐶))
18		simpr 488	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥))
19		simpllr 775	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥))
20	4, 5, 11, 12, 13, 15, 16, 17, 17, 18, 19	comfeqval 16970	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓))
21	20	eqeq1d 2800	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)) → ((𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ (𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓))
22	10, 21	raleqbidva 3370	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ↔ ∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓))
23	4, 5, 6, 7, 9, 8	homfeqval 16959	. . . . . . . . 9 ⊢ (((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐷)𝑦))
24	7	adantr 484	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (Homf ‘𝐶) = (Homf ‘𝐷))
25	14	ad5antr 733	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (compf‘𝐶) = (compf‘𝐷))
26	9	adantr 484	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑥 ∈ (Base‘𝐶))
27		simplr 768	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑦 ∈ (Base‘𝐶))
28		simpllr 775	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥))
29		simpr 488	. . . . . . . . . . 11 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦))
30	4, 5, 11, 12, 24, 25, 26, 26, 27, 28, 29	comfeqval 16970	. . . . . . . . . 10 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔))
31	30	eqeq1d 2800	. . . . . . . . 9 ⊢ ((((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) ∧ 𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)) → ((𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ (𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))
32	23, 31	raleqbidva 3370	. . . . . . . 8 ⊢ (((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → (∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓 ↔ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))
33	22, 32	anbi12d 633	. . . . . . 7 ⊢ (((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) ∧ 𝑦 ∈ (Base‘𝐶)) → ((∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ (∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
34	33	ralbidva 3161	. . . . . 6 ⊢ ((((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) ∧ 𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
35	34	riotabidva 7112	. . . . 5 ⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓)) = (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
36	1	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (Homf ‘𝐶) = (Homf ‘𝐷))
37		simpr 488	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → 𝑥 ∈ (Base‘𝐶))
38	4, 5, 6, 36, 37, 37	homfeqval 16959	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (𝑥(Hom ‘𝐶)𝑥) = (𝑥(Hom ‘𝐷)𝑥))
39	2	ad2antrr 725	. . . . . . 7 ⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (Base‘𝐶) = (Base‘𝐷))
40	39	raleqdv 3364	. . . . . 6 ⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓) ↔ ∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
41	38, 40	riotaeqbidv 7096	. . . . 5 ⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)) = (℩𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
42	35, 41	eqtrd 2833	. . . 4 ⊢ (((𝜑 ∧ 𝐶 ∈ Cat) ∧ 𝑥 ∈ (Base‘𝐶)) → (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓)) = (℩𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓)))
43	3, 42	mpteq12dva 5114	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (𝑥 ∈ (Base‘𝐶) ↦ (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓))) = (𝑥 ∈ (Base‘𝐷) ↦ (℩𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))))
44		simpr 488	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐶 ∈ Cat)
45		eqid 2798	. . . 4 ⊢ (Id‘𝐶) = (Id‘𝐶)
46	4, 5, 11, 44, 45	cidfval 16939	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (Id‘𝐶) = (𝑥 ∈ (Base‘𝐶) ↦ (℩𝑔 ∈ (𝑥(Hom ‘𝐶)𝑥)∀𝑦 ∈ (Base‘𝐶)(∀𝑓 ∈ (𝑦(Hom ‘𝐶)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐶)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐶)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐶)𝑦)𝑔) = 𝑓))))
47		eqid 2798	. . . 4 ⊢ (Base‘𝐷) = (Base‘𝐷)
48		catpropd.3	. . . . . 6 ⊢ (𝜑 → 𝐶 ∈ 𝑉)
49		catpropd.4	. . . . . 6 ⊢ (𝜑 → 𝐷 ∈ 𝑊)
50	1, 14, 48, 49	catpropd 16971	. . . . 5 ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ Cat))
51	50	biimpa 480	. . . 4 ⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → 𝐷 ∈ Cat)
52		eqid 2798	. . . 4 ⊢ (Id‘𝐷) = (Id‘𝐷)
53	47, 6, 12, 51, 52	cidfval 16939	. . 3 ⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (Id‘𝐷) = (𝑥 ∈ (Base‘𝐷) ↦ (℩𝑔 ∈ (𝑥(Hom ‘𝐷)𝑥)∀𝑦 ∈ (Base‘𝐷)(∀𝑓 ∈ (𝑦(Hom ‘𝐷)𝑥)(𝑔(⟨𝑦, 𝑥⟩(comp‘𝐷)𝑥)𝑓) = 𝑓 ∧ ∀𝑓 ∈ (𝑥(Hom ‘𝐷)𝑦)(𝑓(⟨𝑥, 𝑥⟩(comp‘𝐷)𝑦)𝑔) = 𝑓))))
54	43, 46, 53	3eqtr4d 2843	. 2 ⊢ ((𝜑 ∧ 𝐶 ∈ Cat) → (Id‘𝐶) = (Id‘𝐷))
55		simpr 488	. . . . 5 ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → ¬ 𝐶 ∈ Cat)
56		cidffn 16941	. . . . . . 7 ⊢ Id Fn Cat
57	56	fndmi 6426	. . . . . 6 ⊢ dom Id = Cat
58	57	eleq2i 2881	. . . . 5 ⊢ (𝐶 ∈ dom Id ↔ 𝐶 ∈ Cat)
59	55, 58	sylnibr 332	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → ¬ 𝐶 ∈ dom Id)
60		ndmfv 6675	. . . 4 ⊢ (¬ 𝐶 ∈ dom Id → (Id‘𝐶) = ∅)
61	59, 60	syl 17	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → (Id‘𝐶) = ∅)
62	57	eleq2i 2881	. . . . . . 7 ⊢ (𝐷 ∈ dom Id ↔ 𝐷 ∈ Cat)
63	50, 62	syl6bbr 292	. . . . . 6 ⊢ (𝜑 → (𝐶 ∈ Cat ↔ 𝐷 ∈ dom Id))
64	63	notbid 321	. . . . 5 ⊢ (𝜑 → (¬ 𝐶 ∈ Cat ↔ ¬ 𝐷 ∈ dom Id))
65	64	biimpa 480	. . . 4 ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → ¬ 𝐷 ∈ dom Id)
66		ndmfv 6675	. . . 4 ⊢ (¬ 𝐷 ∈ dom Id → (Id‘𝐷) = ∅)
67	65, 66	syl 17	. . 3 ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → (Id‘𝐷) = ∅)
68	61, 67	eqtr4d 2836	. 2 ⊢ ((𝜑 ∧ ¬ 𝐶 ∈ Cat) → (Id‘𝐶) = (Id‘𝐷))
69	54, 68	pm2.61dan 812	1 ⊢ (𝜑 → (Id‘𝐶) = (Id‘𝐷))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399   = wceq 1538   ∈ wcel 2111  ∀wral 3106  ∅c0 4243  ⟨cop 4531   ↦ cmpt 5110  dom cdm 5519  ‘cfv 6324  ℩crio 7092  (class class class)co 7135  Basecbs 16475  Hom chom 16568  compcco 16569  Catccat 16927  Idccid 16928  Hom_f chomf 16929  comp_fccomf 16930

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-rep 5154  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-id 5425  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-riota 7093  df-ov 7138  df-oprab 7139  df-mpo 7140  df-1st 7671  df-2nd 7672  df-cat 16931  df-cid 16932  df-homf 16933  df-comf 16934

This theorem is referenced by:  funcpropd  17162  curfpropd  17475