dfinito4

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

Proof

Step	Hyp	Ref	Expression
1		initofn	⊢ InitO Fn Cat
2		ovex	⊢ ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ∈ V
3	2	dmex	⊢ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ∈ V
4	3	csbex	⊢ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ∈ V
5	4	csbex	⊢ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ∈ V
6		eqid	⊢ ( 𝑐 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ) = ( 𝑐 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) )
7	5 6	fnmpti	⊢ ( 𝑐 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ) Fn Cat
8		eqfnfv	⊢ ( ( InitO Fn Cat ∧ ( 𝑐 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ) Fn Cat ) → ( InitO = ( 𝑐 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ) ↔ ∀ 𝑒 ∈ Cat ( InitO ‘ 𝑒 ) = ( ( 𝑐 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ) ‘ 𝑒 ) ) )
9	1 7 8	mp2an	⊢ ( InitO = ( 𝑐 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ) ↔ ∀ 𝑒 ∈ Cat ( InitO ‘ 𝑒 ) = ( ( 𝑐 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ) ‘ 𝑒 ) )
10		eqid	⊢ ( SetCat ‘ 1_o ) = ( SetCat ‘ 1_o )
11		eqid	⊢ ( ( 1^st ‘ ( ( SetCat ‘ 1_o ) Δ_func 𝑒 ) ) ‘ ∅ ) = ( ( 1^st ‘ ( ( SetCat ‘ 1_o ) Δ_func 𝑒 ) ) ‘ ∅ )
12	10 11	isinito3	⊢ ( 𝑥 ∈ ( InitO ‘ 𝑒 ) ↔ 𝑥 ∈ dom ( ( ( 1^st ‘ ( ( SetCat ‘ 1_o ) Δ_func 𝑒 ) ) ‘ ∅ ) ( 𝑒 UP ( SetCat ‘ 1_o ) ) ∅ ) )
13	12	eqriv	⊢ ( InitO ‘ 𝑒 ) = dom ( ( ( 1^st ‘ ( ( SetCat ‘ 1_o ) Δ_func 𝑒 ) ) ‘ ∅ ) ( 𝑒 UP ( SetCat ‘ 1_o ) ) ∅ )
14		fvex	⊢ ( SetCat ‘ 1_o ) ∈ V
15		fvexd	⊢ ( 𝑑 = ( SetCat ‘ 1_o ) → ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) ∈ V )
16		simpl	⊢ ( ( 𝑑 = ( SetCat ‘ 1_o ) ∧ 𝑓 = ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) ) → 𝑑 = ( SetCat ‘ 1_o ) )
17	16	oveq2d	⊢ ( ( 𝑑 = ( SetCat ‘ 1_o ) ∧ 𝑓 = ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) ) → ( 𝑒 UP 𝑑 ) = ( 𝑒 UP ( SetCat ‘ 1_o ) ) )
18		simpr	⊢ ( ( 𝑑 = ( SetCat ‘ 1_o ) ∧ 𝑓 = ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) ) → 𝑓 = ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) )
19	16	fvoveq1d	⊢ ( ( 𝑑 = ( SetCat ‘ 1_o ) ∧ 𝑓 = ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) ) → ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) = ( 1^st ‘ ( ( SetCat ‘ 1_o ) Δ_func 𝑒 ) ) )
20	19	fveq1d	⊢ ( ( 𝑑 = ( SetCat ‘ 1_o ) ∧ 𝑓 = ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) ) → ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) = ( ( 1^st ‘ ( ( SetCat ‘ 1_o ) Δ_func 𝑒 ) ) ‘ ∅ ) )
21	18 20	eqtrd	⊢ ( ( 𝑑 = ( SetCat ‘ 1_o ) ∧ 𝑓 = ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) ) → 𝑓 = ( ( 1^st ‘ ( ( SetCat ‘ 1_o ) Δ_func 𝑒 ) ) ‘ ∅ ) )
22		eqidd	⊢ ( ( 𝑑 = ( SetCat ‘ 1_o ) ∧ 𝑓 = ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) ) → ∅ = ∅ )
23	17 21 22	oveq123d	⊢ ( ( 𝑑 = ( SetCat ‘ 1_o ) ∧ 𝑓 = ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) ) → ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) = ( ( ( 1^st ‘ ( ( SetCat ‘ 1_o ) Δ_func 𝑒 ) ) ‘ ∅ ) ( 𝑒 UP ( SetCat ‘ 1_o ) ) ∅ ) )
24	23	dmeqd	⊢ ( ( 𝑑 = ( SetCat ‘ 1_o ) ∧ 𝑓 = ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) ) → dom ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) = dom ( ( ( 1^st ‘ ( ( SetCat ‘ 1_o ) Δ_func 𝑒 ) ) ‘ ∅ ) ( 𝑒 UP ( SetCat ‘ 1_o ) ) ∅ ) )
25	15 24	csbied	⊢ ( 𝑑 = ( SetCat ‘ 1_o ) → ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) = dom ( ( ( 1^st ‘ ( ( SetCat ‘ 1_o ) Δ_func 𝑒 ) ) ‘ ∅ ) ( 𝑒 UP ( SetCat ‘ 1_o ) ) ∅ ) )
26	14 25	csbie	⊢ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) = dom ( ( ( 1^st ‘ ( ( SetCat ‘ 1_o ) Δ_func 𝑒 ) ) ‘ ∅ ) ( 𝑒 UP ( SetCat ‘ 1_o ) ) ∅ )
27	13 26	eqtr4i	⊢ ( InitO ‘ 𝑒 ) = ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ )
28		oveq2	⊢ ( 𝑐 = 𝑒 → ( 𝑑 Δ_func 𝑐 ) = ( 𝑑 Δ_func 𝑒 ) )
29	28	fveq2d	⊢ ( 𝑐 = 𝑒 → ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) = ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) )
30	29	fveq1d	⊢ ( 𝑐 = 𝑒 → ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) = ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) )
31		oveq1	⊢ ( 𝑐 = 𝑒 → ( 𝑐 UP 𝑑 ) = ( 𝑒 UP 𝑑 ) )
32	31	oveqd	⊢ ( 𝑐 = 𝑒 → ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) = ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) )
33	32	dmeqd	⊢ ( 𝑐 = 𝑒 → dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) = dom ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) )
34	30 33	csbeq12dv	⊢ ( 𝑐 = 𝑒 → ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) = ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) )
35	34	csbeq2dv	⊢ ( 𝑐 = 𝑒 → ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) = ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) )
36		ovex	⊢ ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) ∈ V
37	36	dmex	⊢ dom ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) ∈ V
38	37	csbex	⊢ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) ∈ V
39	38	csbex	⊢ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) ∈ V
40	35 6 39	fvmpt	⊢ ( 𝑒 ∈ Cat → ( ( 𝑐 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ) ‘ 𝑒 ) = ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑒 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑒 UP 𝑑 ) ∅ ) )
41	27 40	eqtr4id	⊢ ( 𝑒 ∈ Cat → ( InitO ‘ 𝑒 ) = ( ( 𝑐 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) ) ‘ 𝑒 ) )
42	9 41	mprgbir	⊢ InitO = ( 𝑐 ∈ Cat ↦ ⦋ ( SetCat ‘ 1_o ) / 𝑑 ⦌ ⦋ ( ( 1^st ‘ ( 𝑑 Δ_func 𝑐 ) ) ‘ ∅ ) / 𝑓 ⦌ dom ( 𝑓 ( 𝑐 UP 𝑑 ) ∅ ) )

Metamath Proof Explorer

Theorem dfinito4

Proof