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

Metamath Proof Explorer

Theorem dfinito2

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

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

Proof

Step Hyp Ref Expression
1 df-inito ⊢ InitO = ( 𝑐 ∈ 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 termoval ⊢ ( 𝑐 ∈ Cat → ( TermO ‘ ( 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 → ( TermO ‘ ( oppCat ‘ 𝑐 ) ) = { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )
15 14 mpteq2ia ⊢ ( 𝑐 ∈ Cat ↦ ( TermO ‘ ( oppCat ‘ 𝑐 ) ) ) = ( 𝑐 ∈ Cat ↦ { 𝑎 ∈ ( Base ‘ 𝑐 ) ∣ ∀ 𝑏 ∈ ( Base ‘ 𝑐 ) ∃! ℎ ℎ ∈ ( 𝑎 ( Hom ‘ 𝑐 ) 𝑏 ) } )
16 1 15 eqtr4i ⊢ InitO = ( 𝑐 ∈ Cat ↦ ( TermO ‘ ( oppCat ‘ 𝑐 ) ) )