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 ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_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	⊢ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) ∈ V
7	6	csbex	⊢ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) ∈ V
8	7	csbex	⊢ ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) ∈ V
9		dfinito4	⊢ InitO = ( 𝑜 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) )
10	9	fvmpts	⊢ ( ( ( oppCat ‘ 𝑐 ) ∈ Cat ∧ ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) ∈ V ) → ( InitO ‘ ( oppCat ‘ 𝑐 ) ) = ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) )
11	3 8 10	sylancl	⊢ ( 𝑐 ∈ Cat → ( InitO ‘ ( oppCat ‘ 𝑐 ) ) = ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) )
12	11	mpteq2ia	⊢ ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( oppCat ‘ 𝑐 ) ) ) = ( 𝑐 ∈ Cat ↦ ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) )
13	1 12	eqtri	⊢ TermO = ( 𝑐 ∈ Cat ↦ ⦋ ( oppCat ‘ 𝑐 ) / 𝑜 ⦌ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑜 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑜 UP 𝑑 ) ∅ ) )