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

Metamath Proof Explorer

Theorem dftermo3

Description: An alternate definition of df-termo depending on df-inito , without dummy variables. (Contributed by Zhi Wang, 29-Aug-2024)

Ref Expression
Assertion dftermo3 TermO = ( InitO ∘ ( oppCat ↾ Cat ) )

Proof

Step Hyp Ref Expression
1 fvres ⊢ ( 𝑐 ∈ Cat → ( ( oppCat ↾ Cat ) ‘ 𝑐 ) = ( oppCat ‘ 𝑐 ) )
2 1 fveq2d ⊢ ( 𝑐 ∈ Cat → ( InitO ‘ ( ( oppCat ↾ Cat ) ‘ 𝑐 ) ) = ( InitO ‘ ( oppCat ‘ 𝑐 ) ) )
3 2 mpteq2ia ⊢ ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( ( oppCat ↾ Cat ) ‘ 𝑐 ) ) ) = ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( oppCat ‘ 𝑐 ) ) )
4 initofn ⊢ InitO Fn Cat
5 dffn2 ⊢ ( InitO Fn Cat ↔ InitO : Cat ⟶ V )
6 4 5 mpbi ⊢ InitO : Cat ⟶ V
7 oppccatf ⊢ ( oppCat ↾ Cat ) : Cat ⟶ Cat
8 fcompt ⊢ ( ( InitO : Cat ⟶ V ∧ ( oppCat ↾ Cat ) : Cat ⟶ Cat ) → ( InitO ∘ ( oppCat ↾ Cat ) ) = ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( ( oppCat ↾ Cat ) ‘ 𝑐 ) ) ) )
9 6 7 8 mp2an ⊢ ( InitO ∘ ( oppCat ↾ Cat ) ) = ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( ( oppCat ↾ Cat ) ‘ 𝑐 ) ) )
10 dftermo2 ⊢ TermO = ( 𝑐 ∈ Cat ↦ ( InitO ‘ ( oppCat ‘ 𝑐 ) ) )
11 3 9 10 3eqtr4ri ⊢ TermO = ( InitO ∘ ( oppCat ↾ Cat ) )