This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐶 ) ↔ ∀ 𝑏 ∈ 𝐵 ∃! ℎ ℎ ∈ ( 𝑏 𝐻 𝐼 ) ) )