hashgval2

Description: A short expression for the G function of hashgf1o . (Contributed by Mario Carneiro, 24-Jan-2015)

		Ref	Expression
	Assertion	hashgval2	$⊢ {\|.\| ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$

Step	Hyp	Ref	Expression
1		hashresfn	$⊢ ({\|.\| ↾}_{ω}) Fn ω$
2		frfnom	$⊢ ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) Fn ω$
3		eqfnfv	$⊢ (({\|.\| ↾}_{ω}) Fn ω \land ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) Fn ω) \to ({\|.\| ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω} \leftrightarrow \forall y \in ω ({\|.\| ↾}_{ω}) (y) = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (y))$
4	1 2 3	mp2an	$⊢ {\|.\| ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω} \leftrightarrow \forall y \in ω ({\|.\| ↾}_{ω}) (y) = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (y)$
5		fvres	$⊢ y \in ω \to ({\|.\| ↾}_{ω}) (y) = \|y\|$
6		nnfi	$⊢ y \in ω \to y \in Fin$
7		eqid	$⊢ {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
8	7	hashgval	$⊢ y \in Fin \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (card (y)) = \|y\|$
9	6 8	syl	$⊢ y \in ω \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (card (y)) = \|y\|$
10		cardnn	$⊢ y \in ω \to card (y) = y$
11	10	fveq2d	$⊢ y \in ω \to ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (card (y)) = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (y)$
12	5 9 11	3eqtr2d	$⊢ y \in ω \to ({\|.\| ↾}_{ω}) (y) = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) (y)$
13	4 12	mprgbir	$⊢ {\|.\| ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$

Metamath Proof Explorer