Metamath Proof Explorer

Theorem zeroopropdlem

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

Ref Expression
Hypotheses initopropd.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
initopropd.2 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
initopropdlem.1 ⊢ φ → ¬ C ∈ V
Assertion zeroopropdlem ⊢ φ → ZeroO ⁡ C = ZeroO ⁡ D

Proof

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