Theorem initoval

Description: The value of the initial object function, i.e. the set of all initial objects of a category. (Contributed by AV, 3-Apr-2020)

	Ref	Expression
Hypotheses	initoval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	initoval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	initoval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
Assertion	initoval	⊢ ( 𝜑 → ( InitO ‘ 𝐶 ) = { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } )

Proof

Step	Hyp	Ref	Expression
1		initoval.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
2		initoval.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
3		initoval.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
4		df-inito	⊢ InitO = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )
5		fveq2	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = ( Base ‘ 𝐶 ) )
6	5 2	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Base ‘ 𝑐 ) = 𝐵 )
7		fveq2	⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝐶 ) )
8	7 3	eqtr4di	⊢ ( 𝑐 = 𝐶 → ( Hom ‘ 𝑐 ) = 𝐻 )
9	8	oveqd	⊢ ( 𝑐 = 𝐶 → ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) = ( 𝑎 𝐻 𝑏 ) )
10	9	eleq2d	⊢ ( 𝑐 = 𝐶 → ( ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) ↔ ℎ ∈ ( 𝑎 𝐻 𝑏 ) ) )
11	10	eubidv	⊢ ( 𝑐 = 𝐶 → ( ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) ↔ ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) ) )
12	6 11	raleqbidv	⊢ ( 𝑐 = 𝐶 → ( ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) ) )
13	6 12	rabeqbidv	⊢ ( 𝑐 = 𝐶 → { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } = { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } )
14	2	fvexi	⊢ 𝐵 ∈ V
15	14	rabex	⊢ { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } ∈ V
16	15	a1i	⊢ ( 𝜑 → { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } ∈ V )
17	4 13 1 16	fvmptd3	⊢ ( 𝜑 → ( InitO ‘ 𝐶 ) = { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } )