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