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

Metamath Proof Explorer

Theorem dfinito3

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

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

Proof

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