Metamath Proof Explorer

Theorem termopropd

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

Ref Expression
Hypotheses initopropd.1 ⊢ φ → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
initopropd.2 ⊢ φ → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
Assertion termopropd ⊢ φ → TermO ⁡ C = TermO ⁡ 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 termopropdlem ⊢ φ ∧ ¬ C ∈ V → TermO ⁡ C = TermO ⁡ 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 termopropdlem ⊢ φ ∧ ¬ D ∈ V → TermO ⁡ D = TermO ⁡ C
13 12 eqcomd ⊢ φ ∧ ¬ D ∈ V → TermO ⁡ C = TermO ⁡ D
14 1 adantr ⊢ φ ∧ C ∈ V ∧ D ∈ V → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
15 14 adantr ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D
16 eqid ⊢ Hom ⁡ C = Hom ⁡ C
17 eqid ⊢ Hom ⁡ D = Hom ⁡ D
18 eqidd ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → Base C = Base C
19 15 homfeqbas ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → Base C = Base D
20 16 17 18 19 homfeq ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D ↔ ∀ b ∈ Base C ∀ a ∈ Base C b Hom ⁡ C a = b Hom ⁡ D a
21 ralcom ⊢ ∀ b ∈ Base C ∀ a ∈ Base C b Hom ⁡ C a = b Hom ⁡ D a ↔ ∀ a ∈ Base C ∀ b ∈ Base C b Hom ⁡ C a = b Hom ⁡ D a
22 20 21 bitrdi ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → Hom 𝑓 ⁡ C = Hom 𝑓 ⁡ D ↔ ∀ a ∈ Base C ∀ b ∈ Base C b Hom ⁡ C a = b Hom ⁡ D a
23 15 22 mpbid ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → ∀ a ∈ Base C ∀ b ∈ Base C b Hom ⁡ C a = b Hom ⁡ D a
24 23 r19.21bi ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat ∧ a ∈ Base C → ∀ b ∈ Base C b Hom ⁡ C a = b Hom ⁡ D a
25 24 r19.21bi ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat ∧ a ∈ Base C ∧ b ∈ Base C → b Hom ⁡ C a = b Hom ⁡ D a
26 25 eleq2d ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat ∧ a ∈ Base C ∧ b ∈ Base C → h ∈ b Hom ⁡ C a ↔ h ∈ b Hom ⁡ D a
27 26 eubidv ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat ∧ a ∈ Base C ∧ b ∈ Base C → ∃! h h ∈ b Hom ⁡ C a ↔ ∃! h h ∈ b Hom ⁡ D a
28 27 ralbidva ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat ∧ a ∈ Base C → ∀ b ∈ Base C ∃! h h ∈ b Hom ⁡ C a ↔ ∀ b ∈ Base C ∃! h h ∈ b Hom ⁡ D a
29 28 pm5.32da ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → a ∈ Base C ∧ ∀ b ∈ Base C ∃! h h ∈ b Hom ⁡ C a ↔ a ∈ Base C ∧ ∀ b ∈ Base C ∃! h h ∈ b Hom ⁡ D a
30 19 eleq2d ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → a ∈ Base C ↔ a ∈ Base D
31 19 raleqdv ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → ∀ b ∈ Base C ∃! h h ∈ b Hom ⁡ D a ↔ ∀ b ∈ Base D ∃! h h ∈ b Hom ⁡ D a
32 30 31 anbi12d ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → a ∈ Base C ∧ ∀ b ∈ Base C ∃! h h ∈ b Hom ⁡ D a ↔ a ∈ Base D ∧ ∀ b ∈ Base D ∃! h h ∈ b Hom ⁡ D a
33 29 32 bitrd ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → a ∈ Base C ∧ ∀ b ∈ Base C ∃! h h ∈ b Hom ⁡ C a ↔ a ∈ Base D ∧ ∀ b ∈ Base D ∃! h h ∈ b Hom ⁡ D a
34 33 rabbidva2 ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → a ∈ Base C | ∀ b ∈ Base C ∃! h h ∈ b Hom ⁡ C a = a ∈ Base D | ∀ b ∈ Base D ∃! h h ∈ b Hom ⁡ D a
35 simpr ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → C ∈ Cat
36 eqid ⊢ Base C = Base C
37 35 36 16 termoval ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → TermO ⁡ C = a ∈ Base C | ∀ b ∈ Base C ∃! h h ∈ b Hom ⁡ C a
38 2 adantr ⊢ φ ∧ C ∈ V ∧ D ∈ V → comp 𝑓 ⁡ C = comp 𝑓 ⁡ D
39 simprl ⊢ φ ∧ C ∈ V ∧ D ∈ V → C ∈ V
40 simprr ⊢ φ ∧ C ∈ V ∧ D ∈ V → D ∈ V
41 14 38 39 40 catpropd ⊢ φ ∧ C ∈ V ∧ D ∈ V → C ∈ Cat ↔ D ∈ Cat
42 41 biimpa ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → D ∈ Cat
43 eqid ⊢ Base D = Base D
44 42 43 17 termoval ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → TermO ⁡ D = a ∈ Base D | ∀ b ∈ Base D ∃! h h ∈ b Hom ⁡ D a
45 34 37 44 3eqtr4d ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat → TermO ⁡ C = TermO ⁡ D
46 41 pm5.32i ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ C ∈ Cat ↔ φ ∧ C ∈ V ∧ D ∈ V ∧ D ∈ Cat
47 46 45 sylbir ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ D ∈ Cat → TermO ⁡ C = TermO ⁡ D
48 termofn ⊢ TermO Fn Cat
49 48 fndmi ⊢ dom ⁡ TermO = Cat
50 49 eleq2i ⊢ C ∈ dom ⁡ TermO ↔ C ∈ Cat
51 ndmfv ⊢ ¬ C ∈ dom ⁡ TermO → TermO ⁡ C = ∅
52 50 51 sylnbir ⊢ ¬ C ∈ Cat → TermO ⁡ C = ∅
53 52 ad2antrl ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ ¬ C ∈ Cat ∧ ¬ D ∈ Cat → TermO ⁡ C = ∅
54 49 eleq2i ⊢ D ∈ dom ⁡ TermO ↔ D ∈ Cat
55 ndmfv ⊢ ¬ D ∈ dom ⁡ TermO → TermO ⁡ D = ∅
56 54 55 sylnbir ⊢ ¬ D ∈ Cat → TermO ⁡ D = ∅
57 56 ad2antll ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ ¬ C ∈ Cat ∧ ¬ D ∈ Cat → TermO ⁡ D = ∅
58 53 57 eqtr4d ⊢ φ ∧ C ∈ V ∧ D ∈ V ∧ ¬ C ∈ Cat ∧ ¬ D ∈ Cat → TermO ⁡ C = TermO ⁡ D
59 45 47 58 pm2.61ddan ⊢ φ ∧ C ∈ V ∧ D ∈ V → TermO ⁡ C = TermO ⁡ D
60 6 13 59 pm2.61dda ⊢ φ → TermO ⁡ C = TermO ⁡ D