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

Metamath Proof Explorer

Theorem initopropd

Description: Two structures with the same base, hom-sets and composition operation have the same initial objects. (Contributed by Zhi Wang, 23-Oct-2025)

Ref Expression
Hypotheses initopropd.1 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
initopropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
Assertion initopropd ( 𝜑 → ( InitO ‘ 𝐶 ) = ( InitO ‘ 𝐷 ) )

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 initopropdlem ⊢ ( ( 𝜑 ∧ ¬ 𝐶 ∈ V ) → ( InitO ‘ 𝐶 ) = ( InitO ‘ 𝐷 ) )
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 initopropdlem ⊢ ( ( 𝜑 ∧ ¬ 𝐷 ∈ V ) → ( InitO ‘ 𝐷 ) = ( InitO ‘ 𝐶 ) )
13 12 eqcomd ⊢ ( ( 𝜑 ∧ ¬ 𝐷 ∈ V ) → ( InitO ‘ 𝐶 ) = ( InitO ‘ 𝐷 ) )
14 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
15 14 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
16 eqid ⊢ ( Hom ‘ 𝐶 ) = ( Hom ‘ 𝐶 )
17 eqid ⊢ ( Hom ‘ 𝐷 ) = ( Hom ‘ 𝐷 )
18 eqidd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) )
19 15 homfeqbas ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( Base ‘ 𝐶 ) = ( Base ‘ 𝐷 ) )
20 16 17 18 19 homfeq ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) ↔ ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) = ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ) )
21 15 20 mpbid ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ∀ 𝑎 ∈ ( Base ‘ 𝐶 ) ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) = ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) )
22 21 r19.21bi ⊢ ( ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) → ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) = ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) )
23 22 r19.21bi ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) = ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) )
24 23 eleq2d ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ↔ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ) )
25 24 eubidv ⊢ ( ( ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) ∧ 𝑏 ∈ ( Base ‘ 𝐶 ) ) → ( ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ↔ ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ) )
26 25 ralbidva ⊢ ( ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) ∧ 𝑎 ∈ ( Base ‘ 𝐶 ) ) → ( ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ↔ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ) )
27 26 pm5.32da ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( ( 𝑎 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ↔ ( 𝑎 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ) ) )
28 19 eleq2d ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( 𝑎 ∈ ( Base ‘ 𝐶 ) ↔ 𝑎 ∈ ( Base ‘ 𝐷 ) ) )
29 19 raleqdv ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ↔ ∀ 𝑏 ∈ ( Base ‘ 𝐷 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ) )
30 28 29 anbi12d ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( ( 𝑎 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ) ↔ ( 𝑎 ∈ ( Base ‘ 𝐷 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐷 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ) ) )
31 27 30 bitrd ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( ( 𝑎 ∈ ( Base ‘ 𝐶 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) ) ↔ ( 𝑎 ∈ ( Base ‘ 𝐷 ) ∧ ∀ 𝑏 ∈ ( Base ‘ 𝐷 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) ) ) )
32 31 rabbidva2 ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → { 𝑎 ∈ ( Base ‘ 𝐶 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) } = { 𝑎 ∈ ( Base ‘ 𝐷 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝐷 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) } )
33 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → 𝐶 ∈ Cat )
34 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
35 33 34 16 initoval ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( InitO ‘ 𝐶 ) = { 𝑎 ∈ ( Base ‘ 𝐶 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝐶 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐶 ) 𝑏 ) } )
36 2 adantr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
37 simprl ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → 𝐶 ∈ V )
38 simprr ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → 𝐷 ∈ V )
39 14 36 37 38 catpropd ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → ( 𝐶 ∈ Cat ↔ 𝐷 ∈ Cat ) )
40 39 biimpa ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → 𝐷 ∈ Cat )
41 eqid ⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
42 40 41 17 initoval ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( InitO ‘ 𝐷 ) = { 𝑎 ∈ ( Base ‘ 𝐷 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝐷 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝐷 ) 𝑏 ) } )
43 32 35 42 3eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) → ( InitO ‘ 𝐶 ) = ( InitO ‘ 𝐷 ) )
44 39 pm5.32i ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐶 ∈ Cat ) ↔ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐷 ∈ Cat ) )
45 44 43 sylbir ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ 𝐷 ∈ Cat ) → ( InitO ‘ 𝐶 ) = ( InitO ‘ 𝐷 ) )
46 initofn ⊢ InitO Fn Cat
47 46 fndmi ⊢ dom InitO = Cat
48 47 eleq2i ⊢ ( 𝐶 ∈ dom InitO ↔ 𝐶 ∈ Cat )
49 ndmfv ⊢ ( ¬ 𝐶 ∈ dom InitO → ( InitO ‘ 𝐶 ) = ∅ )
50 48 49 sylnbir ⊢ ( ¬ 𝐶 ∈ Cat → ( InitO ‘ 𝐶 ) = ∅ )
51 50 ad2antrl ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ ( ¬ 𝐶 ∈ Cat ∧ ¬ 𝐷 ∈ Cat ) ) → ( InitO ‘ 𝐶 ) = ∅ )
52 47 eleq2i ⊢ ( 𝐷 ∈ dom InitO ↔ 𝐷 ∈ Cat )
53 ndmfv ⊢ ( ¬ 𝐷 ∈ dom InitO → ( InitO ‘ 𝐷 ) = ∅ )
54 52 53 sylnbir ⊢ ( ¬ 𝐷 ∈ Cat → ( InitO ‘ 𝐷 ) = ∅ )
55 54 ad2antll ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ ( ¬ 𝐶 ∈ Cat ∧ ¬ 𝐷 ∈ Cat ) ) → ( InitO ‘ 𝐷 ) = ∅ )
56 51 55 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) ∧ ( ¬ 𝐶 ∈ Cat ∧ ¬ 𝐷 ∈ Cat ) ) → ( InitO ‘ 𝐶 ) = ( InitO ‘ 𝐷 ) )
57 43 45 56 pm2.61ddan ⊢ ( ( 𝜑 ∧ ( 𝐶 ∈ V ∧ 𝐷 ∈ V ) ) → ( InitO ‘ 𝐶 ) = ( InitO ‘ 𝐷 ) )
58 6 13 57 pm2.61dda ⊢ ( 𝜑 → ( InitO ‘ 𝐶 ) = ( InitO ‘ 𝐷 ) )