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 Could not format assertion : No typesetting found for |- TermO = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 dftermo2 ⊢ TermO = c ∈ Cat ⟼ InitO ⁡ oppCat ⁡ c
2 eqid ⊢ oppCat ⁡ c = oppCat ⁡ c
3 2 oppccat ⊢ c ∈ Cat → oppCat ⁡ c ∈ Cat
4 ovex Could not format ( f ( o UP d ) (/) ) e. _V : No typesetting found for |- ( f ( o UP d ) (/) ) e. _V with typecode |-
5 4 dmex Could not format dom ( f ( o UP d ) (/) ) e. _V : No typesetting found for |- dom ( f ( o UP d ) (/) ) e. _V with typecode |-
6 5 csbex Could not format [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V : No typesetting found for |- [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V with typecode |-
7 6 csbex Could not format [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V : No typesetting found for |- [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V with typecode |-
8 7 csbex Could not format [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V : No typesetting found for |- [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V with typecode |-
9 dfinito4 Could not format InitO = ( o e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) : No typesetting found for |- InitO = ( o e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-
10 9 fvmpts Could not format ( ( ( oppCat ` c ) e. Cat /\ [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V ) -> ( InitO ` ( oppCat ` c ) ) = [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) : No typesetting found for |- ( ( ( oppCat ` c ) e. Cat /\ [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) e. _V ) -> ( InitO ` ( oppCat ` c ) ) = [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-
11 3 8 10 sylancl Could not format ( c e. Cat -> ( InitO ` ( oppCat ` c ) ) = [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) : No typesetting found for |- ( c e. Cat -> ( InitO ` ( oppCat ` c ) ) = [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-
12 11 mpteq2ia Could not format ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) ) = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) : No typesetting found for |- ( c e. Cat |-> ( InitO ` ( oppCat ` c ) ) ) = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-
13 1 12 eqtri Could not format TermO = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) : No typesetting found for |- TermO = ( c e. Cat |-> [_ ( oppCat ` c ) / o ]_ [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc o ) ) ` (/) ) / f ]_ dom ( f ( o UP d ) (/) ) ) with typecode |-