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

Metamath Proof Explorer

Theorem istermoi

Description: Implication of a class being a terminal object. (Contributed by AV, 18-Apr-2020)

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

Proof

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