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 \circ ({oppCat ↾}_{Cat})$

Step	Hyp	Ref	Expression
1		fvres	$⊢ c \in Cat \to ({oppCat ↾}_{Cat}) (c) = oppCat (c)$
2	1	fveq2d	$⊢ c \in Cat \to TermO (({oppCat ↾}_{Cat}) (c)) = TermO (oppCat (c))$
3	2	mpteq2ia	$⊢ (c \in Cat ⟼ TermO (({oppCat ↾}_{Cat}) (c))) = (c \in Cat ⟼ TermO (oppCat (c)))$
4		termofn	$⊢ TermO Fn Cat$
5		dffn2	$⊢ TermO Fn Cat \leftrightarrow TermO : Cat ⟶ V$
6	4 5	mpbi	$⊢ TermO : Cat ⟶ V$
7		oppccatf	$⊢ ({oppCat ↾}_{Cat}) : Cat ⟶ Cat$
8		fcompt	$⊢ (TermO : Cat ⟶ V \land ({oppCat ↾}_{Cat}) : Cat ⟶ Cat) \to TermO \circ ({oppCat ↾}_{Cat}) = (c \in Cat ⟼ TermO (({oppCat ↾}_{Cat}) (c)))$
9	6 7 8	mp2an	$⊢ TermO \circ ({oppCat ↾}_{Cat}) = (c \in Cat ⟼ TermO (({oppCat ↾}_{Cat}) (c)))$
10		dfinito2	$⊢ InitO = (c \in Cat ⟼ TermO (oppCat (c)))$
11	3 9 10	3eqtr4ri	$⊢ InitO = TermO \circ ({oppCat ↾}_{Cat})$

Metamath Proof Explorer