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

Metamath Proof Explorer

Theorem dftermo4

Description: An alternate definition of df-termo using universal property. See also the "Equivalent formulations" section of https://en.wikipedia.org/wiki/Initial_and_terminal_objects . (Contributed by Zhi Wang, 23-Oct-2025)

Ref Expression
Assertion dftermo4 TermO = ( 𝑐 ∈ Cat ↦ ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1o ) / 𝑑 ⦌ ⦋ ( ( 1st ‘ ( 𝑑 Δfunc 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) )

Proof

Step Hyp Ref Expression
1 dftermo2 ⊢ TermO = ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( oppCat ‘ 𝑐 ) ) )
2 eqid ⊢ ( oppCat ‘ 𝑐 ) = ( oppCat ‘ 𝑐 )
3 2 oppccat ⊢ ( 𝑐 ∈ Cat → ( oppCat ‘ 𝑐 ) ∈ Cat )
4 ovex ⊢ ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) ∈ V
5 4 dmex ⊢ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) ∈ V
6 5 csbex ⊢ ⦋ ( ( 1st ‘ ( 𝑑 Δfunc 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) ∈ V
7 6 csbex ⊢ ⦋ ( SetCat ‘ 1o ) / 𝑑 ⦌ ⦋ ( ( 1st ‘ ( 𝑑 Δfunc 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) ∈ V
8 7 csbex ⊢ ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1o ) / 𝑑 ⦌ ⦋ ( ( 1st ‘ ( 𝑑 Δfunc 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) ∈ V
9 dfinito4 ⊢ InitO = ( 𝑜 ∈ Cat ↦ ⦋ ( SetCat ‘ 1o ) / 𝑑 ⦌ ⦋ ( ( 1st ‘ ( 𝑑 Δfunc 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) )
10 9 fvmpts ⊢ ( ( ( oppCat ‘ 𝑐 ) ∈ Cat ∧ ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1o ) / 𝑑 ⦌ ⦋ ( ( 1st ‘ ( 𝑑 Δfunc 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) ∈ V ) → ( InitO ‘ ( oppCat ‘ 𝑐 ) ) = ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1o ) / 𝑑 ⦌ ⦋ ( ( 1st ‘ ( 𝑑 Δfunc 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) )
11 3 8 10 sylancl ⊢ ( 𝑐 ∈ Cat → ( InitO ‘ ( oppCat ‘ 𝑐 ) ) = ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1o ) / 𝑑 ⦌ ⦋ ( ( 1st ‘ ( 𝑑 Δfunc 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) )
12 11 mpteq2ia ⊢ ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( oppCat ‘ 𝑐 ) ) ) = ( 𝑐 ∈ Cat ↦ ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1o ) / 𝑑 ⦌ ⦋ ( ( 1st ‘ ( 𝑑 Δfunc 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) )
13 1 12 eqtri ⊢ TermO = ( 𝑐 ∈ Cat ↦ ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1o ) / 𝑑 ⦌ ⦋ ( ( 1st ‘ ( 𝑑 Δfunc 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) )