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 ⊢ ( 𝜑 → ( Homf ‘ 𝐶 ) = ( Homf ‘ 𝐷 ) )
initopropd.2 ⊢ ( 𝜑 → ( compf ‘ 𝐶 ) = ( compf ‘ 𝐷 ) )
Assertion termopropd ( 𝜑 → ( TermO ‘ 𝐶 ) = ( TermO ‘ 𝐷 ) )

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