cidpropd

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

	Ref	Expression
Hypotheses	catpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	catpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
	catpropd.3	$⊢ φ \to C \in V$
	catpropd.4	$⊢ φ \to D \in W$
Assertion	cidpropd	$⊢ φ \to Id (C) = Id (D)$

Proof

Step	Hyp	Ref	Expression
1		catpropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
2		catpropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
3		catpropd.3	$⊢ φ \to C \in V$
4		catpropd.4	$⊢ φ \to D \in W$
5	1	homfeqbas	$⊢ φ \to {Base}_{C} = {Base}_{D}$
6	5	adantr	$⊢ (φ \land C \in Cat) \to {Base}_{C} = {Base}_{D}$
7		eqid	$⊢ {Base}_{C} = {Base}_{C}$
8		eqid	$⊢ Hom (C) = Hom (C)$
9		eqid	$⊢ Hom (D) = Hom (D)$
10	1	ad4antr	$⊢ ((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
11		simpr	$⊢ ((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \to y \in {Base}_{C}$
12		simpllr	$⊢ ((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \to x \in {Base}_{C}$
13	7 8 9 10 11 12	homfeqval	$⊢ ((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \to y Hom (C) x = y Hom (D) x$
14		eqid	$⊢ comp (C) = comp (C)$
15		eqid	$⊢ comp (D) = comp (D)$
16	1	ad5antr	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (y Hom (C) x)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
17	2	ad5antr	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (y Hom (C) x)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
18		simplr	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (y Hom (C) x)) \to y \in {Base}_{C}$
19		simp-4r	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (y Hom (C) x)) \to x \in {Base}_{C}$
20		simpr	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (y Hom (C) x)) \to f \in (y Hom (C) x)$
21		simpllr	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (y Hom (C) x)) \to g \in (x Hom (C) x)$
22	7 8 14 15 16 17 18 19 19 20 21	comfeqval	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (y Hom (C) x)) \to g (⟨y, x⟩ comp (C) x) f = g (⟨y, x⟩ comp (D) x) f$
23	22	eqeq1d	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (y Hom (C) x)) \to (g (⟨y, x⟩ comp (C) x) f = f \leftrightarrow g (⟨y, x⟩ comp (D) x) f = f)$
24	13 23	raleqbidva	$⊢ ((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \to (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \leftrightarrow \forall f \in (y Hom (D) x) g (⟨y, x⟩ comp (D) x) f = f)$
25	7 8 9 10 12 11	homfeqval	$⊢ ((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \to x Hom (C) y = x Hom (D) y$
26	10	adantr	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (x Hom (C) y)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
27	2	ad5antr	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (x Hom (C) y)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
28	12	adantr	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (x Hom (C) y)) \to x \in {Base}_{C}$
29		simplr	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (x Hom (C) y)) \to y \in {Base}_{C}$
30		simpllr	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (x Hom (C) y)) \to g \in (x Hom (C) x)$
31		simpr	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (x Hom (C) y)) \to f \in (x Hom (C) y)$
32	7 8 14 15 26 27 28 28 29 30 31	comfeqval	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (x Hom (C) y)) \to f (⟨x, x⟩ comp (C) y) g = f (⟨x, x⟩ comp (D) y) g$
33	32	eqeq1d	$⊢ (((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \land f \in (x Hom (C) y)) \to (f (⟨x, x⟩ comp (C) y) g = f \leftrightarrow f (⟨x, x⟩ comp (D) y) g = f)$
34	25 33	raleqbidva	$⊢ ((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \to (\forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f \leftrightarrow \forall f \in (x Hom (D) y) f (⟨x, x⟩ comp (D) y) g = f)$
35	24 34	anbi12d	$⊢ ((((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \land y \in {Base}_{C}) \to ((\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f) \leftrightarrow (\forall f \in (y Hom (D) x) g (⟨y, x⟩ comp (D) x) f = f \land \forall f \in (x Hom (D) y) f (⟨x, x⟩ comp (D) y) g = f))$
36	35	ralbidva	$⊢ (((φ \land C \in Cat) \land x \in {Base}_{C}) \land g \in (x Hom (C) x)) \to (\forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f) \leftrightarrow \forall y \in {Base}_{C} (\forall f \in (y Hom (D) x) g (⟨y, x⟩ comp (D) x) f = f \land \forall f \in (x Hom (D) y) f (⟨x, x⟩ comp (D) y) g = f))$
37	36	riotabidva	$⊢ ((φ \land C \in Cat) \land x \in {Base}_{C}) \to (ι g \in (x Hom (C) x) \| \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f)) = (ι g \in (x Hom (C) x) \| \forall y \in {Base}_{C} (\forall f \in (y Hom (D) x) g (⟨y, x⟩ comp (D) x) f = f \land \forall f \in (x Hom (D) y) f (⟨x, x⟩ comp (D) y) g = f))$
38	1	ad2antrr	$⊢ ((φ \land C \in Cat) \land x \in {Base}_{C}) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
39		simpr	$⊢ ((φ \land C \in Cat) \land x \in {Base}_{C}) \to x \in {Base}_{C}$
40	7 8 9 38 39 39	homfeqval	$⊢ ((φ \land C \in Cat) \land x \in {Base}_{C}) \to x Hom (C) x = x Hom (D) x$
41	5	ad2antrr	$⊢ ((φ \land C \in Cat) \land x \in {Base}_{C}) \to {Base}_{C} = {Base}_{D}$
42	41	raleqdv	$⊢ ((φ \land C \in Cat) \land x \in {Base}_{C}) \to (\forall y \in {Base}_{C} (\forall f \in (y Hom (D) x) g (⟨y, x⟩ comp (D) x) f = f \land \forall f \in (x Hom (D) y) f (⟨x, x⟩ comp (D) y) g = f) \leftrightarrow \forall y \in {Base}_{D} (\forall f \in (y Hom (D) x) g (⟨y, x⟩ comp (D) x) f = f \land \forall f \in (x Hom (D) y) f (⟨x, x⟩ comp (D) y) g = f))$
43	40 42	riotaeqbidv	$⊢ ((φ \land C \in Cat) \land x \in {Base}_{C}) \to (ι g \in (x Hom (C) x) \| \forall y \in {Base}_{C} (\forall f \in (y Hom (D) x) g (⟨y, x⟩ comp (D) x) f = f \land \forall f \in (x Hom (D) y) f (⟨x, x⟩ comp (D) y) g = f)) = (ι g \in (x Hom (D) x) \| \forall y \in {Base}_{D} (\forall f \in (y Hom (D) x) g (⟨y, x⟩ comp (D) x) f = f \land \forall f \in (x Hom (D) y) f (⟨x, x⟩ comp (D) y) g = f))$
44	37 43	eqtrd	$⊢ ((φ \land C \in Cat) \land x \in {Base}_{C}) \to (ι g \in (x Hom (C) x) \| \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f)) = (ι g \in (x Hom (D) x) \| \forall y \in {Base}_{D} (\forall f \in (y Hom (D) x) g (⟨y, x⟩ comp (D) x) f = f \land \forall f \in (x Hom (D) y) f (⟨x, x⟩ comp (D) y) g = f))$
45	6 44	mpteq12dva	$⊢ (φ \land C \in Cat) \to (x \in {Base}_{C} ⟼ (ι g \in (x Hom (C) x) \| \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f))) = (x \in {Base}_{D} ⟼ (ι g \in (x Hom (D) x) \| \forall y \in {Base}_{D} (\forall f \in (y Hom (D) x) g (⟨y, x⟩ comp (D) x) f = f \land \forall f \in (x Hom (D) y) f (⟨x, x⟩ comp (D) y) g = f)))$
46		simpr	$⊢ (φ \land C \in Cat) \to C \in Cat$
47		eqid	$⊢ Id (C) = Id (C)$
48	7 8 14 46 47	cidfval	$⊢ (φ \land C \in Cat) \to Id (C) = (x \in {Base}_{C} ⟼ (ι g \in (x Hom (C) x) \| \forall y \in {Base}_{C} (\forall f \in (y Hom (C) x) g (⟨y, x⟩ comp (C) x) f = f \land \forall f \in (x Hom (C) y) f (⟨x, x⟩ comp (C) y) g = f)))$
49		eqid	$⊢ {Base}_{D} = {Base}_{D}$
50	1 2 3 4	catpropd	$⊢ φ \to (C \in Cat \leftrightarrow D \in Cat)$
51	50	biimpa	$⊢ (φ \land C \in Cat) \to D \in Cat$
52		eqid	$⊢ Id (D) = Id (D)$
53	49 9 15 51 52	cidfval	$⊢ (φ \land C \in Cat) \to Id (D) = (x \in {Base}_{D} ⟼ (ι g \in (x Hom (D) x) \| \forall y \in {Base}_{D} (\forall f \in (y Hom (D) x) g (⟨y, x⟩ comp (D) x) f = f \land \forall f \in (x Hom (D) y) f (⟨x, x⟩ comp (D) y) g = f)))$
54	45 48 53	3eqtr4d	$⊢ (φ \land C \in Cat) \to Id (C) = Id (D)$
55		simpr	$⊢ (φ \land \neg C \in Cat) \to \neg C \in Cat$
56		cidffn	$⊢ Id Fn Cat$
57	56	fndmi	$⊢ dom Id = Cat$
58	57	eleq2i	$⊢ C \in dom Id \leftrightarrow C \in Cat$
59	55 58	sylnibr	$⊢ (φ \land \neg C \in Cat) \to \neg C \in dom Id$
60		ndmfv	$⊢ \neg C \in dom Id \to Id (C) = \emptyset$
61	59 60	syl	$⊢ (φ \land \neg C \in Cat) \to Id (C) = \emptyset$
62	57	eleq2i	$⊢ D \in dom Id \leftrightarrow D \in Cat$
63	50 62	bitr4di	$⊢ φ \to (C \in Cat \leftrightarrow D \in dom Id)$
64	63	notbid	$⊢ φ \to (\neg C \in Cat \leftrightarrow \neg D \in dom Id)$
65	64	biimpa	$⊢ (φ \land \neg C \in Cat) \to \neg D \in dom Id$
66		ndmfv	$⊢ \neg D \in dom Id \to Id (D) = \emptyset$
67	65 66	syl	$⊢ (φ \land \neg C \in Cat) \to Id (D) = \emptyset$
68	61 67	eqtr4d	$⊢ (φ \land \neg C \in Cat) \to Id (C) = Id (D)$
69	54 68	pm2.61dan	$⊢ φ \to Id (C) = Id (D)$

Metamath Proof Explorer

Theorem cidpropd

Proof