Metamath Proof Explorer


Theorem dftermo2

Description: A terminal object is an initial object in the opposite category. An alternate definition of df-termo depending on df-inito . (Contributed by Zhi Wang, 29-Aug-2024)

Ref Expression
Assertion dftermo2 TermO = ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( oppCat ‘ 𝑐 ) ) )

Proof

Step Hyp Ref Expression
1 df-termo TermO = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ∈ ( 𝑏 ( Hom ‘ 𝑐 ) 𝑎 ) } )
2 eqid ( oppCat ‘ 𝑐 ) = ( oppCat ‘ 𝑐 )
3 2 oppccat ( 𝑐 ∈ Cat → ( oppCat ‘ 𝑐 ) ∈ Cat )
4 eqid ( Base ‘ 𝑐 ) = ( Base ‘ 𝑐 )
5 2 4 oppcbas ( Base ‘ 𝑐 ) = ( Base ‘ ( oppCat ‘ 𝑐 ) )
6 eqid ( Hom ‘ ( oppCat ‘ 𝑐 ) ) = ( Hom ‘ ( oppCat ‘ 𝑐 ) )
7 3 5 6 initoval ( 𝑐 ∈ Cat → ( InitO ‘ ( oppCat ‘ 𝑐 ) ) = { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ∈ ( 𝑎 ( Hom ‘ ( oppCat ‘ 𝑐 ) ) 𝑏 ) } )
8 eqid ( Hom ‘ 𝑐 ) = ( Hom ‘ 𝑐 )
9 8 2 oppchom ( 𝑎 ( Hom ‘ ( oppCat ‘ 𝑐 ) ) 𝑏 ) = ( 𝑏 ( Hom ‘ 𝑐 ) 𝑎 )
10 9 eleq2i ( ∈ ( 𝑎 ( Hom ‘ ( oppCat ‘ 𝑐 ) ) 𝑏 ) ↔ ∈ ( 𝑏 ( Hom ‘ 𝑐 ) 𝑎 ) )
11 10 eubii ( ∃! ∈ ( 𝑎 ( Hom ‘ ( oppCat ‘ 𝑐 ) ) 𝑏 ) ↔ ∃! ∈ ( 𝑏 ( Hom ‘ 𝑐 ) 𝑎 ) )
12 11 ralbii ( ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ∈ ( 𝑎 ( Hom ‘ ( oppCat ‘ 𝑐 ) ) 𝑏 ) ↔ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ∈ ( 𝑏 ( Hom ‘ 𝑐 ) 𝑎 ) )
13 12 rabbii { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ∈ ( 𝑎 ( Hom ‘ ( oppCat ‘ 𝑐 ) ) 𝑏 ) } = { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ∈ ( 𝑏 ( Hom ‘ 𝑐 ) 𝑎 ) }
14 7 13 eqtrdi ( 𝑐 ∈ Cat → ( InitO ‘ ( oppCat ‘ 𝑐 ) ) = { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ∈ ( 𝑏 ( Hom ‘ 𝑐 ) 𝑎 ) } )
15 14 mpteq2ia ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( oppCat ‘ 𝑐 ) ) ) = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ∈ ( 𝑏 ( Hom ‘ 𝑐 ) 𝑎 ) } )
16 1 15 eqtr4i TermO = ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( oppCat ‘ 𝑐 ) ) )