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 \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 InitO (({oppCat ↾}_{Cat}) (c)) = InitO (oppCat (c))$
3	2	mpteq2ia	$⊢ (c \in Cat ⟼ InitO (({oppCat ↾}_{Cat}) (c))) = (c \in Cat ⟼ InitO (oppCat (c)))$
4		initofn	$⊢ InitO Fn Cat$
5		dffn2	$⊢ InitO Fn Cat \leftrightarrow InitO : Cat ⟶ V$
6	4 5	mpbi	$⊢ InitO : Cat ⟶ V$
7		oppccatf	$⊢ ({oppCat ↾}_{Cat}) : Cat ⟶ Cat$
8		fcompt	$⊢ (InitO : Cat ⟶ V \land ({oppCat ↾}_{Cat}) : Cat ⟶ Cat) \to InitO \circ ({oppCat ↾}_{Cat}) = (c \in Cat ⟼ InitO (({oppCat ↾}_{Cat}) (c)))$
9	6 7 8	mp2an	$⊢ InitO \circ ({oppCat ↾}_{Cat}) = (c \in Cat ⟼ InitO (({oppCat ↾}_{Cat}) (c)))$
10		dftermo2	$⊢ TermO = (c \in Cat ⟼ InitO (oppCat (c)))$
11	3 9 10	3eqtr4ri	$⊢ TermO = InitO \circ ({oppCat ↾}_{Cat})$

Metamath Proof Explorer