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 ‘ 𝑐 ) ) )