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

Metamath Proof Explorer

Theorem dfinito4

Description: An alternate definition of df-inito 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 dfinito4 Could not format assertion : No typesetting found for |- InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) with typecode |-

Proof

Step Hyp Ref Expression
1 initofn ⊢ InitO Fn Cat
2 ovex Could not format ( f ( c UP d ) (/) ) e. _V : No typesetting found for |- ( f ( c UP d ) (/) ) e. _V with typecode |-
3 2 dmex Could not format dom ( f ( c UP d ) (/) ) e. _V : No typesetting found for |- dom ( f ( c UP d ) (/) ) e. _V with typecode |-
4 3 csbex Could not format [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) e. _V : No typesetting found for |- [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) e. _V with typecode |-
5 4 csbex Could not format [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) e. _V : No typesetting found for |- [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) e. _V with typecode |-
6 eqid Could not format ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) : No typesetting found for |- ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) with typecode |-
7 5 6 fnmpti Could not format ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) Fn Cat : No typesetting found for |- ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) Fn Cat with typecode |-
8 eqfnfv Could not format ( ( InitO Fn Cat /\ ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) Fn Cat ) -> ( InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) <-> A. e e. Cat ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) ) : No typesetting found for |- ( ( InitO Fn Cat /\ ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) Fn Cat ) -> ( InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) <-> A. e e. Cat ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) ) with typecode |-
9 1 7 8 mp2an Could not format ( InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) <-> A. e e. Cat ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) : No typesetting found for |- ( InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) <-> A. e e. Cat ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) with typecode |-
10 eqid ⊢ SetCat ⁡ 1 𝑜 = SetCat ⁡ 1 𝑜
11 eqid ⊢ 1 st ⁡ SetCat ⁡ 1 𝑜 Δ func e ⁡ ∅ = 1 st ⁡ SetCat ⁡ 1 𝑜 Δ func e ⁡ ∅
12 10 11 isinito3 Could not format ( x e. ( InitO ` e ) <-> x e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) : No typesetting found for |- ( x e. ( InitO ` e ) <-> x e. dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) with typecode |-
13 12 eqriv Could not format ( InitO ` e ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) : No typesetting found for |- ( InitO ` e ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) with typecode |-
14 fvex ⊢ SetCat ⁡ 1 𝑜 ∈ V
15 fvexd ⊢ d = SetCat ⁡ 1 𝑜 → 1 st ⁡ d Δ func e ⁡ ∅ ∈ V
16 simpl ⊢ d = SetCat ⁡ 1 𝑜 ∧ f = 1 st ⁡ d Δ func e ⁡ ∅ → d = SetCat ⁡ 1 𝑜
17 16 oveq2d Could not format ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( e UP d ) = ( e UP ( SetCat ` 1o ) ) ) : No typesetting found for |- ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( e UP d ) = ( e UP ( SetCat ` 1o ) ) ) with typecode |-
18 simpr ⊢ d = SetCat ⁡ 1 𝑜 ∧ f = 1 st ⁡ d Δ func e ⁡ ∅ → f = 1 st ⁡ d Δ func e ⁡ ∅
19 16 fvoveq1d ⊢ d = SetCat ⁡ 1 𝑜 ∧ f = 1 st ⁡ d Δ func e ⁡ ∅ → 1 st ⁡ d Δ func e = 1 st ⁡ SetCat ⁡ 1 𝑜 Δ func e
20 19 fveq1d ⊢ d = SetCat ⁡ 1 𝑜 ∧ f = 1 st ⁡ d Δ func e ⁡ ∅ → 1 st ⁡ d Δ func e ⁡ ∅ = 1 st ⁡ SetCat ⁡ 1 𝑜 Δ func e ⁡ ∅
21 18 20 eqtrd ⊢ d = SetCat ⁡ 1 𝑜 ∧ f = 1 st ⁡ d Δ func e ⁡ ∅ → f = 1 st ⁡ SetCat ⁡ 1 𝑜 Δ func e ⁡ ∅
22 eqidd ⊢ d = SetCat ⁡ 1 𝑜 ∧ f = 1 st ⁡ d Δ func e ⁡ ∅ → ∅ = ∅
23 17 21 22 oveq123d Could not format ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( f ( e UP d ) (/) ) = ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) : No typesetting found for |- ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> ( f ( e UP d ) (/) ) = ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) with typecode |-
24 23 dmeqd Could not format ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) : No typesetting found for |- ( ( d = ( SetCat ` 1o ) /\ f = ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) ) -> dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) with typecode |-
25 15 24 csbied Could not format ( d = ( SetCat ` 1o ) -> [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) : No typesetting found for |- ( d = ( SetCat ` 1o ) -> [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) ) with typecode |-
26 14 25 csbie Could not format [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) : No typesetting found for |- [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) = dom ( ( ( 1st ` ( ( SetCat ` 1o ) DiagFunc e ) ) ` (/) ) ( e UP ( SetCat ` 1o ) ) (/) ) with typecode |-
27 13 26 eqtr4i Could not format ( InitO ` e ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) : No typesetting found for |- ( InitO ` e ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) with typecode |-
28 oveq2 ⊢ c = e → d Δ func c = d Δ func e
29 28 fveq2d ⊢ c = e → 1 st ⁡ d Δ func c = 1 st ⁡ d Δ func e
30 29 fveq1d ⊢ c = e → 1 st ⁡ d Δ func c ⁡ ∅ = 1 st ⁡ d Δ func e ⁡ ∅
31 oveq1 Could not format ( c = e -> ( c UP d ) = ( e UP d ) ) : No typesetting found for |- ( c = e -> ( c UP d ) = ( e UP d ) ) with typecode |-
32 31 oveqd Could not format ( c = e -> ( f ( c UP d ) (/) ) = ( f ( e UP d ) (/) ) ) : No typesetting found for |- ( c = e -> ( f ( c UP d ) (/) ) = ( f ( e UP d ) (/) ) ) with typecode |-
33 32 dmeqd Could not format ( c = e -> dom ( f ( c UP d ) (/) ) = dom ( f ( e UP d ) (/) ) ) : No typesetting found for |- ( c = e -> dom ( f ( c UP d ) (/) ) = dom ( f ( e UP d ) (/) ) ) with typecode |-
34 30 33 csbeq12dv Could not format ( c = e -> [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) = [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) : No typesetting found for |- ( c = e -> [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) = [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) with typecode |-
35 34 csbeq2dv Could not format ( c = e -> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) : No typesetting found for |- ( c = e -> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) with typecode |-
36 ovex Could not format ( f ( e UP d ) (/) ) e. _V : No typesetting found for |- ( f ( e UP d ) (/) ) e. _V with typecode |-
37 36 dmex Could not format dom ( f ( e UP d ) (/) ) e. _V : No typesetting found for |- dom ( f ( e UP d ) (/) ) e. _V with typecode |-
38 37 csbex Could not format [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) e. _V : No typesetting found for |- [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) e. _V with typecode |-
39 38 csbex Could not format [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) e. _V : No typesetting found for |- [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) e. _V with typecode |-
40 35 6 39 fvmpt Could not format ( e e. Cat -> ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) : No typesetting found for |- ( e e. Cat -> ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) = [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc e ) ) ` (/) ) / f ]_ dom ( f ( e UP d ) (/) ) ) with typecode |-
41 27 40 eqtr4id Could not format ( e e. Cat -> ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) : No typesetting found for |- ( e e. Cat -> ( InitO ` e ) = ( ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) ` e ) ) with typecode |-
42 9 41 mprgbir Could not format InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) : No typesetting found for |- InitO = ( c e. Cat |-> [_ ( SetCat ` 1o ) / d ]_ [_ ( ( 1st ` ( d DiagFunc c ) ) ` (/) ) / f ]_ dom ( f ( c UP d ) (/) ) ) with typecode |-