Theorem isinitoi

Description: Implication of a class being an initial object. (Contributed by AV, 6-Apr-2020)

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

Proof

Step	Hyp	Ref	Expression
1		isinitoi.b	⊢ 𝐵 = ( Base ‘ 𝐶 )
2		isinitoi.h	⊢ 𝐻 = ( Hom ‘ 𝐶 )
3		isinitoi.c	⊢ ( 𝜑 → 𝐶 ∈ Cat )
4	3 1 2	initoval	⊢ ( 𝜑 → ( InitO ‘ 𝐶 ) = { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } )
5	4	eleq2d	⊢ ( 𝜑 → ( 𝑂 ∈ ( InitO ‘ 𝐶 ) ↔ 𝑂 ∈ { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } ) )
6		elrabi	⊢ ( 𝑂 ∈ { 𝑎 ∈ 𝐵 ∣ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑎 𝐻 𝑏 ) } → 𝑂 ∈ 𝐵 )
7	5 6	syl6bi	⊢ ( 𝜑 → ( 𝑂 ∈ ( InitO ‘ 𝐶 ) → 𝑂 ∈ 𝐵 ) )
8	7	imp	⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → 𝑂 ∈ 𝐵 )
9	3	adantr	⊢ ( ( 𝜑 ∧ 𝑂 ∈ 𝐵 ) → 𝐶 ∈ Cat )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑂 ∈ 𝐵 ) → 𝑂 ∈ 𝐵 )
11	1 2 9 10	isinito	⊢ ( ( 𝜑 ∧ 𝑂 ∈ 𝐵 ) → ( 𝑂 ∈ ( InitO ‘ 𝐶 ) ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑏 ) ) )
12	11	biimpd	⊢ ( ( 𝜑 ∧ 𝑂 ∈ 𝐵 ) → ( 𝑂 ∈ ( InitO ‘ 𝐶 ) → ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑏 ) ) )
13	12	impancom	⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝑂 ∈ 𝐵 → ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑏 ) ) )
14	8 13	jcai	⊢ ( ( 𝜑 ∧ 𝑂 ∈ ( InitO ‘ 𝐶 ) ) → ( 𝑂 ∈ 𝐵 ∧ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑂 𝐻 𝑏 ) ) )