Metamath Proof Explorer

Theorem hashgval2

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

Ref Expression
Assertion hashgval2 ⊢ . ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω

Proof

Step Hyp Ref Expression
1 hashresfn ⊢ . ↾ ω Fn ω
2 frfnom ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω Fn ω
3 eqfnfv ⊢ . ↾ ω Fn ω ∧ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω Fn ω → . ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ↔ ∀ y ∈ ω . ↾ ω ⁡ y = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ y
4 1 2 3 mp2an ⊢ . ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ↔ ∀ y ∈ ω . ↾ ω ⁡ y = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ y
5 fvres ⊢ y ∈ ω → . ↾ ω ⁡ y = y
6 nnfi ⊢ y ∈ ω → y ∈ Fin
7 eqid ⊢ rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω
8 7 hashgval ⊢ y ∈ Fin → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ y = y
9 6 8 syl ⊢ y ∈ ω → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ y = y
10 cardnn ⊢ y ∈ ω → card ⁡ y = y
11 10 fveq2d ⊢ y ∈ ω → rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ card ⁡ y = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ y
12 5 9 11 3eqtr2d ⊢ y ∈ ω → . ↾ ω ⁡ y = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω ⁡ y
13 4 12 mprgbir ⊢ . ↾ ω = rec ⁡ x ∈ V ⟼ x + 1 0 ↾ ω