This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐷 ) )