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 ⊢ c ∈ Cat → oppCat ↾ Cat ⁡ c = oppCat ⁡ c
2 1 fveq2d ⊢ c ∈ Cat → InitO ⁡ oppCat ↾ Cat ⁡ c = InitO ⁡ oppCat ⁡ c
3 2 mpteq2ia ⊢ c ∈ Cat ⟼ InitO ⁡ oppCat ↾ Cat ⁡ c = c ∈ Cat ⟼ InitO ⁡ oppCat ⁡ c
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 = c ∈ Cat ⟼ InitO ⁡ oppCat ↾ Cat ⁡ c
9 6 7 8 mp2an ⊢ InitO ∘ oppCat ↾ Cat = c ∈ Cat ⟼ InitO ⁡ oppCat ↾ Cat ⁡ c
10 dftermo2 ⊢ TermO = c ∈ Cat ⟼ InitO ⁡ oppCat ⁡ c
11 3 9 10 3eqtr4ri ⊢ TermO = InitO ∘ oppCat ↾ Cat