Theorem dfinito4 50743

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

Assertion

Ref	Expression
dfinito4	⊢ InitO = (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅))

Distinct variable group:   𝑐,𝑑,𝑓

Proof of Theorem dfinito4

Dummy variables 𝑒 𝑥 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		initofn 18169	. . 3 ⊢ InitO Fn Cat
2		ovex 7455	. . . . . . 7 ⊢ (𝑓(𝑐 UP 𝑑)∅) ∈ V
3	2	dmex 7923	. . . . . 6 ⊢ dom (𝑓(𝑐 UP 𝑑)∅) ∈ V
4	3	csbex 5264	. . . . 5 ⊢ ⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅) ∈ V
5	4	csbex 5264	. . . 4 ⊢ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅) ∈ V
6		eqid 2760	. . . 4 ⊢ (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅)) = (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅))
7	5, 6	fnmpti 6685	. . 3 ⊢ (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅)) Fn Cat
8		eqfnfv 7032	. . 3 ⊢ ((InitO Fn Cat ∧ (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅)) Fn Cat) → (InitO = (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅)) ↔ ∀𝑒 ∈ Cat (InitO‘𝑒) = ((𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅))‘𝑒)))
9	1, 7, 8	mp2an 705	. 2 ⊢ (InitO = (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅)) ↔ ∀𝑒 ∈ Cat (InitO‘𝑒) = ((𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅))‘𝑒))
10		eqid 2760	. . . . . 6 ⊢ (SetCat‘1o) = (SetCat‘1o)
11		eqid 2760	. . . . . 6 ⊢ ((1st ‘((SetCat‘1o)Δfunc𝑒))‘∅) = ((1st ‘((SetCat‘1o)Δfunc𝑒))‘∅)
12	10, 11	isinito3 50742	. . . . 5 ⊢ (𝑥 ∈ (InitO‘𝑒) ↔ 𝑥 ∈ dom (((1st ‘((SetCat‘1o)Δfunc𝑒))‘∅)(𝑒 UP (SetCat‘1o))∅))
13	12	eqriv 2757	. . . 4 ⊢ (InitO‘𝑒) = dom (((1st ‘((SetCat‘1o)Δfunc𝑒))‘∅)(𝑒 UP (SetCat‘1o))∅)
14		fvex 6901	. . . . 5 ⊢ (SetCat‘1o) ∈ V
15		fvexd 6903	. . . . . 6 ⊢ (𝑑 = (SetCat‘1o) → ((1st ‘(𝑑Δfunc𝑒))‘∅) ∈ V)
16		simpl 488	. . . . . . . . 9 ⊢ ((𝑑 = (SetCat‘1o) ∧ 𝑓 = ((1st ‘(𝑑Δfunc𝑒))‘∅)) → 𝑑 = (SetCat‘1o))
17	16	oveq2d 7438	. . . . . . . 8 ⊢ ((𝑑 = (SetCat‘1o) ∧ 𝑓 = ((1st ‘(𝑑Δfunc𝑒))‘∅)) → (𝑒 UP 𝑑) = (𝑒 UP (SetCat‘1o)))
18		simpr 490	. . . . . . . . 9 ⊢ ((𝑑 = (SetCat‘1o) ∧ 𝑓 = ((1st ‘(𝑑Δfunc𝑒))‘∅)) → 𝑓 = ((1st ‘(𝑑Δfunc𝑒))‘∅))
19	16	fvoveq1d 7444	. . . . . . . . . 10 ⊢ ((𝑑 = (SetCat‘1o) ∧ 𝑓 = ((1st ‘(𝑑Δfunc𝑒))‘∅)) → (1st ‘(𝑑Δfunc𝑒)) = (1st ‘((SetCat‘1o)Δfunc𝑒)))
20	19	fveq1d 6890	. . . . . . . . 9 ⊢ ((𝑑 = (SetCat‘1o) ∧ 𝑓 = ((1st ‘(𝑑Δfunc𝑒))‘∅)) → ((1st ‘(𝑑Δfunc𝑒))‘∅) = ((1st ‘((SetCat‘1o)Δfunc𝑒))‘∅))
21	18, 20	eqtrd 2795	. . . . . . . 8 ⊢ ((𝑑 = (SetCat‘1o) ∧ 𝑓 = ((1st ‘(𝑑Δfunc𝑒))‘∅)) → 𝑓 = ((1st ‘((SetCat‘1o)Δfunc𝑒))‘∅))
22		eqidd 2761	. . . . . . . 8 ⊢ ((𝑑 = (SetCat‘1o) ∧ 𝑓 = ((1st ‘(𝑑Δfunc𝑒))‘∅)) → ∅ = ∅)
23	17, 21, 22	oveq123d 7443	. . . . . . 7 ⊢ ((𝑑 = (SetCat‘1o) ∧ 𝑓 = ((1st ‘(𝑑Δfunc𝑒))‘∅)) → (𝑓(𝑒 UP 𝑑)∅) = (((1st ‘((SetCat‘1o)Δfunc𝑒))‘∅)(𝑒 UP (SetCat‘1o))∅))
24	23	dmeqd 5887	. . . . . 6 ⊢ ((𝑑 = (SetCat‘1o) ∧ 𝑓 = ((1st ‘(𝑑Δfunc𝑒))‘∅)) → dom (𝑓(𝑒 UP 𝑑)∅) = dom (((1st ‘((SetCat‘1o)Δfunc𝑒))‘∅)(𝑒 UP (SetCat‘1o))∅))
25	15, 24	csbied 3883	. . . . 5 ⊢ (𝑑 = (SetCat‘1o) → ⦋((1st ‘(𝑑Δfunc𝑒))‘∅) / 𝑓⦌dom (𝑓(𝑒 UP 𝑑)∅) = dom (((1st ‘((SetCat‘1o)Δfunc𝑒))‘∅)(𝑒 UP (SetCat‘1o))∅))
26	14, 25	csbie 3882	. . . 4 ⊢ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑒))‘∅) / 𝑓⦌dom (𝑓(𝑒 UP 𝑑)∅) = dom (((1st ‘((SetCat‘1o)Δfunc𝑒))‘∅)(𝑒 UP (SetCat‘1o))∅)
27	13, 26	eqtr4i 2786	. . 3 ⊢ (InitO‘𝑒) = ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑒))‘∅) / 𝑓⦌dom (𝑓(𝑒 UP 𝑑)∅)
28		oveq2 7430	. . . . . . . 8 ⊢ (𝑐 = 𝑒 → (𝑑Δfunc𝑐) = (𝑑Δfunc𝑒))
29	28	fveq2d 6892	. . . . . . 7 ⊢ (𝑐 = 𝑒 → (1st ‘(𝑑Δfunc𝑐)) = (1st ‘(𝑑Δfunc𝑒)))
30	29	fveq1d 6890	. . . . . 6 ⊢ (𝑐 = 𝑒 → ((1st ‘(𝑑Δfunc𝑐))‘∅) = ((1st ‘(𝑑Δfunc𝑒))‘∅))
31		oveq1 7429	. . . . . . . 8 ⊢ (𝑐 = 𝑒 → (𝑐 UP 𝑑) = (𝑒 UP 𝑑))
32	31	oveqd 7439	. . . . . . 7 ⊢ (𝑐 = 𝑒 → (𝑓(𝑐 UP 𝑑)∅) = (𝑓(𝑒 UP 𝑑)∅))
33	32	dmeqd 5887	. . . . . 6 ⊢ (𝑐 = 𝑒 → dom (𝑓(𝑐 UP 𝑑)∅) = dom (𝑓(𝑒 UP 𝑑)∅))
34	30, 33	csbeq12dv 3856	. . . . 5 ⊢ (𝑐 = 𝑒 → ⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅) = ⦋((1st ‘(𝑑Δfunc𝑒))‘∅) / 𝑓⦌dom (𝑓(𝑒 UP 𝑑)∅))
35	34	csbeq2dv 3854	. . . 4 ⊢ (𝑐 = 𝑒 → ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅) = ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑒))‘∅) / 𝑓⦌dom (𝑓(𝑒 UP 𝑑)∅))
36		ovex 7455	. . . . . . 7 ⊢ (𝑓(𝑒 UP 𝑑)∅) ∈ V
37	36	dmex 7923	. . . . . 6 ⊢ dom (𝑓(𝑒 UP 𝑑)∅) ∈ V
38	37	csbex 5264	. . . . 5 ⊢ ⦋((1st ‘(𝑑Δfunc𝑒))‘∅) / 𝑓⦌dom (𝑓(𝑒 UP 𝑑)∅) ∈ V
39	38	csbex 5264	. . . 4 ⊢ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑒))‘∅) / 𝑓⦌dom (𝑓(𝑒 UP 𝑑)∅) ∈ V
40	35, 6, 39	fvmpt 6996	. . 3 ⊢ (𝑒 ∈ Cat → ((𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅))‘𝑒) = ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑒))‘∅) / 𝑓⦌dom (𝑓(𝑒 UP 𝑑)∅))
41	27, 40	eqtr4id 2814	. 2 ⊢ (𝑒 ∈ Cat → (InitO‘𝑒) = ((𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅))‘𝑒))
42	9, 41	mprgbir 3083	1 ⊢ InitO = (𝑐 ∈ Cat ↦ ⦋(SetCat‘1o) / 𝑑⦌⦋((1st ‘(𝑑Δfunc𝑐))‘∅) / 𝑓⦌dom (𝑓(𝑐 UP 𝑑)∅))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401   = wceq 1569   ∈ wcel 2144  ∀wral 3076  Vcvv 3450  ⦋csb 3847  ∅c0 4277   ↦ cmpt 5185  dom cdm 5650   Fn wfn 6536  ‘cfv 6541  (class class class)co 7422  1^st c1st 8001  1_oc1o 8474  Catccat 17845  InitOcinito 18163  SetCatcsetc 18257  Δ_funccdiag 18393   UP cup 50396

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-10 2177  ax-11 2193  ax-12 2212  ax-ext 2732  ax-rep 5231  ax-sep 5248  ax-nul 5259  ax-pow 5326  ax-pr 5390  ax-un 7753  ax-cnex 11261  ax-resscn 11262  ax-1cn 11263  ax-icn 11264  ax-addcl 11265  ax-addrcl 11266  ax-mulcl 11267  ax-mulrcl 11268  ax-mulcom 11269  ax-addass 11270  ax-mulass 11271  ax-distr 11272  ax-i2m1 11273  ax-1ne0 11274  ax-1rid 11275  ax-rnegex 11276  ax-rrecex 11277  ax-cnre 11278  ax-pre-lttri 11279  ax-pre-lttrn 11280  ax-pre-ltadd 11281  ax-pre-mulgt0 11282

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-nf 1816  df-sb 2099  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-nel 3062  df-ral 3077  df-rex 3087  df-rmo 3365  df-reu 3366  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3848  df-ss 3897  df-pss 4013  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-pw 4558  df-sn 4585  df-pr 4587  df-tp 4589  df-op 4835  df-ot 4858  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-tr 5212  df-id 5545  df-eprel 5550  df-po 5558  df-so 5559  df-fr 5603  df-we 5605  df-xp 5656  df-rel 5657  df-cnv 5658  df-co 5659  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663  df-pred 6306  df-ord 6367  df-on 6368  df-lim 6369  df-suc 6370  df-iota 6496  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-riota 7379  df-ov 7425  df-oprab 7426  df-mpo 7427  df-om 7880  df-1st 8003  df-2nd 8004  df-frecs 8304  df-wrecs 8335  df-recs 8384  df-rdg 8423  df-1o 8481  df-er 8722  df-map 8854  df-ixp 8931  df-en 8979  df-dom 8980  df-sdom 8981  df-fin 8982  df-pnf 11350  df-mnf 11351  df-xr 11352  df-ltxr 11353  df-le 11354  df-sub 11548  df-neg 11549  df-nn 12341  df-2 12410  df-3 12411  df-4 12412  df-5 12413  df-6 12414  df-7 12415  df-8 12416  df-9 12417  df-n0 12612  df-z 12699  df-dec 12820  df-uz 12971  df-fz 13645  df-struct 17332  df-slot 17367  df-ndx 17379  df-base 17395  df-hom 17459  df-cco 17460  df-cat 17849  df-cid 17850  df-func 18040  df-nat 18128  df-fuc 18129  df-inito 18166  df-setc 18258  df-xpc 18353  df-1stf 18354  df-curf 18395  df-diag 18397  df-up 50397  df-thinc 50660  df-termc 50715

This theorem is used by:  dftermo4  50744