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