Theorem zeroopropdlem

Description: Lemma for zeroopropd . (Contributed by Zhi Wang, 26-Oct-2025)

	Ref	Expression
Hypotheses	initopropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
	initopropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
	initopropdlem.1	⊢ ( 𝜑 → ¬ 𝐶 ∈ V )
Assertion	zeroopropdlem	⊢ ( 𝜑 → ( ZeroO ‘ 𝐶 ) = ( ZeroO ‘ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		initopropd.1	⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
2		initopropd.2	⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
3		initopropdlem.1	⊢ ( 𝜑 → ¬ 𝐶 ∈ V )
4		zeroofn	⊢ ZeroO Fn Cat
5		ssv	⊢ Cat ⊆ V
6		simpr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → 𝐷 ∈ Cat )
7		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
8		eqid	⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
9	6 7 8	zerooval	⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → ( ZeroO ‘ 𝐷 ) = ( ( InitO ‘ 𝐷 ) ∩ ( TermO ‘ 𝐷 ) ) )
10	1 2 3	initopropdlem	⊢ ( 𝜑 → ( InitO ‘ 𝐶 ) = ( InitO ‘ 𝐷 ) )
11		fvprc	⊢ ( ¬ 𝐶 ∈ V → ( InitO ‘ 𝐶 ) = ∅ )
12	3 11	syl	⊢ ( 𝜑 → ( InitO ‘ 𝐶 ) = ∅ )
13	10 12	eqtr3d	⊢ ( 𝜑 → ( InitO ‘ 𝐷 ) = ∅ )
14	13	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → ( InitO ‘ 𝐷 ) = ∅ )
15	1 2 3	termopropdlem	⊢ ( 𝜑 → ( TermO ‘ 𝐶 ) = ( TermO ‘ 𝐷 ) )
16		fvprc	⊢ ( ¬ 𝐶 ∈ V → ( TermO ‘ 𝐶 ) = ∅ )
17	3 16	syl	⊢ ( 𝜑 → ( TermO ‘ 𝐶 ) = ∅ )
18	15 17	eqtr3d	⊢ ( 𝜑 → ( TermO ‘ 𝐷 ) = ∅ )
19	18	adantr	⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → ( TermO ‘ 𝐷 ) = ∅ )
20	14 19	ineq12d	⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → ( ( InitO ‘ 𝐷 ) ∩ ( TermO ‘ 𝐷 ) ) = ( ∅ ∩ ∅ ) )
21		inidm	⊢ ( ∅ ∩ ∅ ) = ∅
22	20 21	eqtrdi	⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → ( ( InitO ‘ 𝐷 ) ∩ ( TermO ‘ 𝐷 ) ) = ∅ )
23	9 22	eqtrd	⊢ ( ( 𝜑 ∧ 𝐷 ∈ Cat ) → ( ZeroO ‘ 𝐷 ) = ∅ )
24	4 3 5 23	initopropdlemlem	⊢ ( 𝜑 → ( ZeroO ‘ 𝐶 ) = ( ZeroO ‘ 𝐷 ) )