Theorem isinito

Description: The predicate "is an initial object" of a category. (Contributed by AV, 3-Apr-2020)

	Ref	Expression
Hypotheses	isinito.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
	isinito.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
	isinito.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
	isinito.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
Assertion	isinito	⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝐼 𝐻 𝑏 ) ) )

Proof

Step	Hyp	Ref	Expression
1		isinito.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		isinito.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		isinito.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4		isinito.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐵 )
5	3 1 2	initoval	⊢ ( 𝜑 → ( InitO ‘ 𝐶 ) = { 𝑖 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑖 𝐻 𝑏 ) } )
6	5	eleq2d	⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ 𝐼 ∈ { 𝑖 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑖 𝐻 𝑏 ) } ) )
7		oveq1	⊢ ( 𝑖 = 𝐼 → ( 𝑖 𝐻 𝑏 ) = ( 𝐼 𝐻 𝑏 ) )
8	7	eleq2d	⊢ ( 𝑖 = 𝐼 → ( ℎ ∈ ( 𝑖 𝐻 𝑏 ) ↔ ℎ ∈ ( 𝐼 𝐻 𝑏 ) ) )
9	8	eubidv	⊢ ( 𝑖 = 𝐼 → ( ∃! ℎ ℎ ∈ ( 𝑖 𝐻 𝑏 ) ↔ ∃! ℎ ℎ ∈ ( 𝐼 𝐻 𝑏 ) ) )
10	9	ralbidv	⊢ ( 𝑖 = 𝐼 → ( ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑖 𝐻 𝑏 ) ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝐼 𝐻 𝑏 ) ) )
11	10	elrab3	⊢ ( 𝐼 ∈ 𝐵 → ( 𝐼 ∈ { 𝑖 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑖 𝐻 𝑏 ) } ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝐼 𝐻 𝑏 ) ) )
12	4 11	syl	⊢ ( 𝜑 → ( 𝐼 ∈ { 𝑖 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑖 𝐻 𝑏 ) } ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝐼 𝐻 𝑏 ) ) )
13	6 12	bitrd	⊢ ( 𝜑 → ( 𝐼 ∈ ( InitO ‘ 𝐶 ) ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝐼 𝐻 𝑏 ) ) )