Theorem zeroopropd

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

	Ref	Expression
Hypotheses	initopropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
	initopropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
Assertion	zeroopropd	⊢ ( 𝜑 → ( ZeroO ‘ 𝐶 ) = ( ZeroO ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		initopropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2		initopropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
3	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
4	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
5		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → ¬ 𝐶 ∈ V )
6	3 4 5	zeroopropdlem	⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → ( ZeroO ‘ 𝐶 ) = ( ZeroO ‘ 𝐷 ) )
7	1	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐷 ∈ V ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
8	7	eqcomd	⊢ ( ( 𝜑 ∧ ¬ 𝐷 ∈ V ) → ( Homf ‘ 𝐷 ) = ( Homf ‘ 𝐶 ) )
9	2	adantr	⊢ ( ( 𝜑 ∧ ¬ 𝐷 ∈ V ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
10	9	eqcomd	⊢ ( ( 𝜑 ∧ ¬ 𝐷 ∈ V ) → ( compf ‘ 𝐷 ) = ( compf ‘ 𝐶 ) )
11		simpr	⊢ ( ( 𝜑 ∧ ¬ 𝐷 ∈ V ) → ¬ 𝐷 ∈ V )
12	8 10 11	zeroopropdlem	⊢ ( ( 𝜑 ∧ ¬ 𝐷 ∈ V ) → ( ZeroO ‘ 𝐷 ) = ( ZeroO ‘ 𝐶 ) )
13	12	eqcomd	⊢ ( ( 𝜑 ∧ ¬ 𝐷 ∈ V ) → ( ZeroO ‘ 𝐶 ) = ( ZeroO ‘ 𝐷 ) )
14	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
15	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
16	14 15	initopropd	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( InitO ‘ 𝐶 ) = ( InitO ‘ 𝐷 ) )
17	14 15	termopropd	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( TermO ‘ 𝐶 ) = ( TermO ‘ 𝐷 ) )
18	16 17	ineq12d	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) = ( ( InitO ‘ 𝐷 ) ∩ ( TermO ‘ 𝐷 ) ) )
19		simpr	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → 𝐶 ∈ Cat )
20		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
21		eqid	⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
22	19 20 21	zerooval	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( ZeroO ‘ 𝐶 ) = ( ( InitO ‘ 𝐶 ) ∩ ( TermO ‘ 𝐶 ) ) )
23	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
24	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
25		simprl	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → 𝐶 ∈ V )
26		simprr	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → 𝐷 ∈ V )
27	23 24 25 26	catpropd	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → ( 𝐶 ∈ Cat ↔ 𝐷 ∈ Cat ) )
28	27	biimpa	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → 𝐷 ∈ Cat )
29		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
30		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
31	28 29 30	zerooval	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( ZeroO ‘ 𝐷 ) = ( ( InitO ‘ 𝐷 ) ∩ ( TermO ‘ 𝐷 ) ) )
32	18 22 31	3eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( ZeroO ‘ 𝐶 ) = ( ZeroO ‘ 𝐷 ) )
33	27	pm5.32i	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) ↔ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐷 ∈ Cat ) )
34	33 32	sylbir	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐷 ∈ Cat ) → ( ZeroO ‘ 𝐶 ) = ( ZeroO ‘ 𝐷 ) )
35		zeroofn	⊢ ZeroO Fn Cat
36	35	fndmi	⊢ dom ZeroO = Cat
37	36	eleq2i	⊢ ( 𝐶 ∈ dom ZeroO ↔ 𝐶 ∈ Cat )
38		ndmfv	⊢ ( ¬ 𝐶 ∈ dom ZeroO → ( ZeroO ‘ 𝐶 ) = ∅ )
39	37 38	sylnbir	⊢ ( ¬ 𝐶 ∈ Cat → ( ZeroO ‘ 𝐶 ) = ∅ )
40	39	ad2antrl	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ ( ¬ 𝐶 ∈ Cat ∧ ¬ 𝐷 ∈ Cat ) ) → ( ZeroO ‘ 𝐶 ) = ∅ )
41	36	eleq2i	⊢ ( 𝐷 ∈ dom ZeroO ↔ 𝐷 ∈ Cat )
42		ndmfv	⊢ ( ¬ 𝐷 ∈ dom ZeroO → ( ZeroO ‘ 𝐷 ) = ∅ )
43	41 42	sylnbir	⊢ ( ¬ 𝐷 ∈ Cat → ( ZeroO ‘ 𝐷 ) = ∅ )
44	43	ad2antll	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ ( ¬ 𝐶 ∈ Cat ∧ ¬ 𝐷 ∈ Cat ) ) → ( ZeroO ‘ 𝐷 ) = ∅ )
45	40 44	eqtr4d	⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ ( ¬ 𝐶 ∈ Cat ∧ ¬ 𝐷 ∈ Cat ) ) → ( ZeroO ‘ 𝐶 ) = ( ZeroO ‘ 𝐷 ) )
46	32 34 45	pm2.61ddan	⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → ( ZeroO ‘ 𝐶 ) = ( ZeroO ‘ 𝐷 ) )
47	6 13 46	pm2.61dda	⊢ ( 𝜑 → ( ZeroO ‘ 𝐶 ) = ( ZeroO ‘ 𝐷 ) )