Theorem istermo

Description: The predicate "is a terminal 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	istermo	⊢ ( 𝜑 → ( 𝐼 ∈ ( TermO ‘ 𝐶 ) ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝐼 ) ) )

Proof

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