Metamath Proof Explorer

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 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
initopropd.2 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
Assertion zeroopropd ⊢ φ → ZeroO ⁡ C = ZeroO ⁡ D

Proof

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