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

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 ⊢ ( 𝜑 → ( 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 ‘ 𝐷 ) )