initopropd

Description: Two structures with the same base, hom-sets and composition operation have the same initial objects. (Contributed by Zhi Wang, 23-Oct-2025)

	Ref	Expression
Hypotheses	initopropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
	initopropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
Assertion	initopropd	$⊢ φ \to InitO (C) = InitO (D)$

Proof

Step	Hyp	Ref	Expression
1		initopropd.1	$⊢ φ \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
2		initopropd.2	$⊢ φ \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
3	1	adantr	$⊢ (φ \land \neg C \in V) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
4	2	adantr	$⊢ (φ \land \neg C \in V) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
5		simpr	$⊢ (φ \land \neg C \in V) \to \neg C \in V$
6	3 4 5	initopropdlem	$⊢ (φ \land \neg C \in V) \to InitO (C) = InitO (D)$
7	1	adantr	$⊢ (φ \land \neg D \in V) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
8	7	eqcomd	$⊢ (φ \land \neg D \in V) \to {Hom}_{𝑓} (D) = {Hom}_{𝑓} (C)$
9	2	adantr	$⊢ (φ \land \neg D \in V) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
10	9	eqcomd	$⊢ (φ \land \neg D \in V) \to {comp}_{𝑓} (D) = {comp}_{𝑓} (C)$
11		simpr	$⊢ (φ \land \neg D \in V) \to \neg D \in V$
12	8 10 11	initopropdlem	$⊢ (φ \land \neg D \in V) \to InitO (D) = InitO (C)$
13	12	eqcomd	$⊢ (φ \land \neg D \in V) \to InitO (C) = InitO (D)$
14	1	adantr	$⊢ (φ \land (C \in V \land D \in V)) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
15	14	adantr	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to {Hom}_{𝑓} (C) = {Hom}_{𝑓} (D)$
16		eqid	$⊢ Hom (C) = Hom (C)$
17		eqid	$⊢ Hom (D) = Hom (D)$
18		eqidd	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to {Base}_{C} = {Base}_{C}$
19	15	homfeqbas	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to {Base}_{C} = {Base}_{D}$
20	16 17 18 19	homfeq	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to ({Hom}_{𝑓} (C) = {Hom}_{𝑓} (D) \leftrightarrow \forall a \in {Base}_{C} \forall b \in {Base}_{C} a Hom (C) b = a Hom (D) b)$
21	15 20	mpbid	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to \forall a \in {Base}_{C} \forall b \in {Base}_{C} a Hom (C) b = a Hom (D) b$
22	21	r19.21bi	$⊢ (((φ \land (C \in V \land D \in V)) \land C \in Cat) \land a \in {Base}_{C}) \to \forall b \in {Base}_{C} a Hom (C) b = a Hom (D) b$
23	22	r19.21bi	$⊢ ((((φ \land (C \in V \land D \in V)) \land C \in Cat) \land a \in {Base}_{C}) \land b \in {Base}_{C}) \to a Hom (C) b = a Hom (D) b$
24	23	eleq2d	$⊢ ((((φ \land (C \in V \land D \in V)) \land C \in Cat) \land a \in {Base}_{C}) \land b \in {Base}_{C}) \to (h \in (a Hom (C) b) \leftrightarrow h \in (a Hom (D) b))$
25	24	eubidv	$⊢ ((((φ \land (C \in V \land D \in V)) \land C \in Cat) \land a \in {Base}_{C}) \land b \in {Base}_{C}) \to (\exists! h h \in (a Hom (C) b) \leftrightarrow \exists! h h \in (a Hom (D) b))$
26	25	ralbidva	$⊢ (((φ \land (C \in V \land D \in V)) \land C \in Cat) \land a \in {Base}_{C}) \to (\forall b \in {Base}_{C} \exists! h h \in (a Hom (C) b) \leftrightarrow \forall b \in {Base}_{C} \exists! h h \in (a Hom (D) b))$
27	26	pm5.32da	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to ((a \in {Base}_{C} \land \forall b \in {Base}_{C} \exists! h h \in (a Hom (C) b)) \leftrightarrow (a \in {Base}_{C} \land \forall b \in {Base}_{C} \exists! h h \in (a Hom (D) b)))$
28	19	eleq2d	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to (a \in {Base}_{C} \leftrightarrow a \in {Base}_{D})$
29	19	raleqdv	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to (\forall b \in {Base}_{C} \exists! h h \in (a Hom (D) b) \leftrightarrow \forall b \in {Base}_{D} \exists! h h \in (a Hom (D) b))$
30	28 29	anbi12d	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to ((a \in {Base}_{C} \land \forall b \in {Base}_{C} \exists! h h \in (a Hom (D) b)) \leftrightarrow (a \in {Base}_{D} \land \forall b \in {Base}_{D} \exists! h h \in (a Hom (D) b)))$
31	27 30	bitrd	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to ((a \in {Base}_{C} \land \forall b \in {Base}_{C} \exists! h h \in (a Hom (C) b)) \leftrightarrow (a \in {Base}_{D} \land \forall b \in {Base}_{D} \exists! h h \in (a Hom (D) b)))$
32	31	rabbidva2	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to \{a \in {Base}_{C} \| \forall b \in {Base}_{C} \exists! h h \in (a Hom (C) b)\} = \{a \in {Base}_{D} \| \forall b \in {Base}_{D} \exists! h h \in (a Hom (D) b)\}$
33		simpr	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to C \in Cat$
34		eqid	$⊢ {Base}_{C} = {Base}_{C}$
35	33 34 16	initoval	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to InitO (C) = \{a \in {Base}_{C} \| \forall b \in {Base}_{C} \exists! h h \in (a Hom (C) b)\}$
36	2	adantr	$⊢ (φ \land (C \in V \land D \in V)) \to {comp}_{𝑓} (C) = {comp}_{𝑓} (D)$
37		simprl	$⊢ (φ \land (C \in V \land D \in V)) \to C \in V$
38		simprr	$⊢ (φ \land (C \in V \land D \in V)) \to D \in V$
39	14 36 37 38	catpropd	$⊢ (φ \land (C \in V \land D \in V)) \to (C \in Cat \leftrightarrow D \in Cat)$
40	39	biimpa	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to D \in Cat$
41		eqid	$⊢ {Base}_{D} = {Base}_{D}$
42	40 41 17	initoval	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to InitO (D) = \{a \in {Base}_{D} \| \forall b \in {Base}_{D} \exists! h h \in (a Hom (D) b)\}$
43	32 35 42	3eqtr4d	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \to InitO (C) = InitO (D)$
44	39	pm5.32i	$⊢ ((φ \land (C \in V \land D \in V)) \land C \in Cat) \leftrightarrow ((φ \land (C \in V \land D \in V)) \land D \in Cat)$
45	44 43	sylbir	$⊢ ((φ \land (C \in V \land D \in V)) \land D \in Cat) \to InitO (C) = InitO (D)$
46		initofn	$⊢ InitO Fn Cat$
47	46	fndmi	$⊢ dom InitO = Cat$
48	47	eleq2i	$⊢ C \in dom InitO \leftrightarrow C \in Cat$
49		ndmfv	$⊢ \neg C \in dom InitO \to InitO (C) = \emptyset$
50	48 49	sylnbir	$⊢ \neg C \in Cat \to InitO (C) = \emptyset$
51	50	ad2antrl	$⊢ ((φ \land (C \in V \land D \in V)) \land (\neg C \in Cat \land \neg D \in Cat)) \to InitO (C) = \emptyset$
52	47	eleq2i	$⊢ D \in dom InitO \leftrightarrow D \in Cat$
53		ndmfv	$⊢ \neg D \in dom InitO \to InitO (D) = \emptyset$
54	52 53	sylnbir	$⊢ \neg D \in Cat \to InitO (D) = \emptyset$
55	54	ad2antll	$⊢ ((φ \land (C \in V \land D \in V)) \land (\neg C \in Cat \land \neg D \in Cat)) \to InitO (D) = \emptyset$
56	51 55	eqtr4d	$⊢ ((φ \land (C \in V \land D \in V)) \land (\neg C \in Cat \land \neg D \in Cat)) \to InitO (C) = InitO (D)$
57	43 45 56	pm2.61ddan	$⊢ (φ \land (C \in V \land D \in V)) \to InitO (C) = InitO (D)$
58	6 13 57	pm2.61dda	$⊢ φ \to InitO (C) = InitO (D)$

Metamath Proof Explorer

Theorem initopropd

Proof