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