Metamath Proof Explorer

Theorem termolmd

Description: Terminal objects are the object part of limits of the empty diagram. (Contributed by Zhi Wang, 20-Nov-2025)

Ref Expression
Assertion termolmd ( TermO ‘ 𝐶 ) = dom ( ∅ ( 𝐶 Limit ∅ ) ∅ )

Proof

Step Hyp Ref Expression
1 termorcl ⊢ ( 𝑥 ∈ ( TermO ‘ 𝐶 ) → 𝐶 ∈ Cat )
2 vex ⊢ 𝑥 ∈ V
3 2 eldm ⊢ ( 𝑥 ∈ dom ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) ↔ ∃ 𝑦 𝑥 ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) 𝑦 )
4 df-br ⊢ ( 𝑥 ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) 𝑦 ↔ ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) )
5 lmdrcl ⊢ ( ⟨ 𝑥 , 𝑦 ⟩ ∈ ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) → ⟨ ∅ , ∅ ⟩ ∈ ( ∅ Func 𝐶 ) )
6 4 5 sylbi ⊢ ( 𝑥 ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) 𝑦 → ⟨ ∅ , ∅ ⟩ ∈ ( ∅ Func 𝐶 ) )
7 6 func1st2nd ⊢ ( 𝑥 ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) 𝑦 → ( 1st ‘ ⟨ ∅ , ∅ ⟩ ) ( ∅ Func 𝐶 ) ( 2nd ‘ ⟨ ∅ , ∅ ⟩ ) )
8 7 funcrcl3 ⊢ ( 𝑥 ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) 𝑦 → 𝐶 ∈ Cat )
9 8 exlimiv ⊢ ( ∃ 𝑦 𝑥 ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) 𝑦 → 𝐶 ∈ Cat )
10 3 9 sylbi ⊢ ( 𝑥 ∈ dom ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) → 𝐶 ∈ Cat )
11 initocmd ⊢ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) = dom ( ∅ ( ( oppCat ‘ 𝐶 ) Colimit ∅ ) ∅ )
12 oppctermo ⊢ ( 𝑥 ∈ ( TermO ‘ 𝐶 ) ↔ 𝑥 ∈ ( InitO ‘ ( oppCat ‘ 𝐶 ) ) )
13 12 eqriv ⊢ ( TermO ‘ 𝐶 ) = ( InitO ‘ ( oppCat ‘ 𝐶 ) )
14 13 a1i ⊢ ( 𝐶 ∈ Cat → ( TermO ‘ 𝐶 ) = ( InitO ‘ ( oppCat ‘ 𝐶 ) ) )
15 eqid ⊢ ( oppCat ‘ 𝐶 ) = ( oppCat ‘ 𝐶 )
16 15 2oppchomf ⊢ ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ ( oppCat ‘ 𝐶 ) ) )
17 16 a1i ⊢ ( 𝐶 ∈ Cat → ( Homf ‘ 𝐶 ) = ( Homf ‘ ( oppCat ‘ ( oppCat ‘ 𝐶 ) ) ) )
18 15 2oppccomf ⊢ ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ ( oppCat ‘ 𝐶 ) ) )
19 18 a1i ⊢ ( 𝐶 ∈ Cat → ( compf ‘ 𝐶 ) = ( compf ‘ ( oppCat ‘ ( oppCat ‘ 𝐶 ) ) ) )
20 ral0 ⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) = ( 𝑥 ( Hom ‘ ( oppCat ‘ ∅ ) ) 𝑦 )
21 eqid ⊢ ( Hom ‘ ∅ ) = ( Hom ‘ ∅ )
22 eqid ⊢ ( Hom ‘ ( oppCat ‘ ∅ ) ) = ( Hom ‘ ( oppCat ‘ ∅ ) )
23 base0 ⊢ ∅ = ( Base ‘ ∅ )
24 23 a1i ⊢ ( 𝐶 ∈ Cat → ∅ = ( Base ‘ ∅ ) )
25 eqid ⊢ ( oppCat ‘ ∅ ) = ( oppCat ‘ ∅ )
26 25 23 oppcbas ⊢ ∅ = ( Base ‘ ( oppCat ‘ ∅ ) )
27 26 a1i ⊢ ( 𝐶 ∈ Cat → ∅ = ( Base ‘ ( oppCat ‘ ∅ ) ) )
28 21 22 24 27 homfeq ⊢ ( 𝐶 ∈ Cat → ( ( Homf ‘ ∅ ) = ( Homf ‘ ( oppCat ‘ ∅ ) ) ↔ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) = ( 𝑥 ( Hom ‘ ( oppCat ‘ ∅ ) ) 𝑦 ) ) )
29 20 28 mpbiri ⊢ ( 𝐶 ∈ Cat → ( Homf ‘ ∅ ) = ( Homf ‘ ( oppCat ‘ ∅ ) ) )
30 ral0 ⊢ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ ∅ ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ∅ ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ ∅ ) ) 𝑧 ) 𝑓 )
31 eqid ⊢ ( comp ‘ ∅ ) = ( comp ‘ ∅ )
32 eqid ⊢ ( comp ‘ ( oppCat ‘ ∅ ) ) = ( comp ‘ ( oppCat ‘ ∅ ) )
33 31 32 21 24 27 29 comfeq ⊢ ( 𝐶 ∈ Cat → ( ( compf ‘ ∅ ) = ( compf ‘ ( oppCat ‘ ∅ ) ) ↔ ∀ 𝑥 ∈ ∅ ∀ 𝑦 ∈ ∅ ∀ 𝑧 ∈ ∅ ∀ 𝑓 ∈ ( 𝑥 ( Hom ‘ ∅ ) 𝑦 ) ∀ 𝑔 ∈ ( 𝑦 ( Hom ‘ ∅ ) 𝑧 ) ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ∅ ) 𝑧 ) 𝑓 ) = ( 𝑔 ( ⟨ 𝑥 , 𝑦 ⟩ ( comp ‘ ( oppCat ‘ ∅ ) ) 𝑧 ) 𝑓 ) ) )
34 30 33 mpbiri ⊢ ( 𝐶 ∈ Cat → ( compf ‘ ∅ ) = ( compf ‘ ( oppCat ‘ ∅ ) ) )
35 elex ⊢ ( 𝐶 ∈ Cat → 𝐶 ∈ V )
36 fvexd ⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ ( oppCat ‘ 𝐶 ) ) ∈ V )
37 0ex ⊢ ∅ ∈ V
38 37 a1i ⊢ ( 𝐶 ∈ Cat → ∅ ∈ V )
39 fvexd ⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ ∅ ) ∈ V )
40 17 19 29 34 35 36 38 39 lmdpropd ⊢ ( 𝐶 ∈ Cat → ( 𝐶 Limit ∅ ) = ( ( oppCat ‘ ( oppCat ‘ 𝐶 ) ) Limit ( oppCat ‘ ∅ ) ) )
41 eqidd ⊢ ( 𝐶 ∈ Cat → ∅ = ∅ )
42 0cat ⊢ ∅ ∈ Cat
43 42 a1i ⊢ ( 𝐶 ∈ Cat → ∅ ∈ Cat )
44 43 24 43 0funcg2 ⊢ ( 𝐶 ∈ Cat → ( ∅ ( ∅ Func ∅ ) ∅ ↔ ( ∅ = ∅ ∧ ∅ = ∅ ) ) )
45 41 41 44 mpbir2and ⊢ ( 𝐶 ∈ Cat → ∅ ( ∅ Func ∅ ) ∅ )
46 oppfval ⊢ ( ∅ ( ∅ Func ∅ ) ∅ → ( ∅ oppFunc ∅ ) = ⟨ ∅ , tpos ∅ ⟩ )
47 45 46 syl ⊢ ( 𝐶 ∈ Cat → ( ∅ oppFunc ∅ ) = ⟨ ∅ , tpos ∅ ⟩ )
48 tpos0 ⊢ tpos ∅ = ∅
49 48 opeq2i ⊢ ⟨ ∅ , tpos ∅ ⟩ = ⟨ ∅ , ∅ ⟩
50 47 49 eqtr2di ⊢ ( 𝐶 ∈ Cat → ⟨ ∅ , ∅ ⟩ = ( ∅ oppFunc ∅ ) )
51 40 50 fveq12d ⊢ ( 𝐶 ∈ Cat → ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) = ( ( ( oppCat ‘ ( oppCat ‘ 𝐶 ) ) Limit ( oppCat ‘ ∅ ) ) ‘ ( ∅ oppFunc ∅ ) ) )
52 df-ov ⊢ ( ∅ ( ( oppCat ‘ 𝐶 ) Colimit ∅ ) ∅ ) = ( ( ( oppCat ‘ 𝐶 ) Colimit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ )
53 eqid ⊢ ( oppCat ‘ ( oppCat ‘ 𝐶 ) ) = ( oppCat ‘ ( oppCat ‘ 𝐶 ) )
54 df-ov ⊢ ( ∅ oppFunc ∅ ) = ( oppFunc ‘ ⟨ ∅ , ∅ ⟩ )
55 fvexd ⊢ ( 𝐶 ∈ Cat → ( oppCat ‘ 𝐶 ) ∈ V )
56 53 25 54 55 38 cmddu ⊢ ( 𝐶 ∈ Cat → ( ( ( oppCat ‘ 𝐶 ) Colimit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) = ( ( ( oppCat ‘ ( oppCat ‘ 𝐶 ) ) Limit ( oppCat ‘ ∅ ) ) ‘ ( ∅ oppFunc ∅ ) ) )
57 52 56 eqtrid ⊢ ( 𝐶 ∈ Cat → ( ∅ ( ( oppCat ‘ 𝐶 ) Colimit ∅ ) ∅ ) = ( ( ( oppCat ‘ ( oppCat ‘ 𝐶 ) ) Limit ( oppCat ‘ ∅ ) ) ‘ ( ∅ oppFunc ∅ ) ) )
58 51 57 eqtr4d ⊢ ( 𝐶 ∈ Cat → ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) = ( ∅ ( ( oppCat ‘ 𝐶 ) Colimit ∅ ) ∅ ) )
59 58 dmeqd ⊢ ( 𝐶 ∈ Cat → dom ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) = dom ( ∅ ( ( oppCat ‘ 𝐶 ) Colimit ∅ ) ∅ ) )
60 11 14 59 3eqtr4a ⊢ ( 𝐶 ∈ Cat → ( TermO ‘ 𝐶 ) = dom ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) )
61 60 eleq2d ⊢ ( 𝐶 ∈ Cat → ( 𝑥 ∈ ( TermO ‘ 𝐶 ) ↔ 𝑥 ∈ dom ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) ) )
62 1 10 61 pm5.21nii ⊢ ( 𝑥 ∈ ( TermO ‘ 𝐶 ) ↔ 𝑥 ∈ dom ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ ) )
63 62 eqriv ⊢ ( TermO ‘ 𝐶 ) = dom ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ )
64 df-ov ⊢ ( ∅ ( 𝐶 Limit ∅ ) ∅ ) = ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ )
65 64 dmeqi ⊢ dom ( ∅ ( 𝐶 Limit ∅ ) ∅ ) = dom ( ( 𝐶 Limit ∅ ) ‘ ⟨ ∅ , ∅ ⟩ )
66 63 65 eqtr4i ⊢ ( TermO ‘ 𝐶 ) = dom ( ∅ ( 𝐶 Limit ∅ ) ∅ )