This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )

Proof

Step Hyp Ref Expression
1 hashresfn ⊢ ( ♯ ↾ ω ) Fn ω
2 frfnom ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) Fn ω
3 eqfnfv ⊢ ( ( ( ♯ ↾ ω ) Fn ω ∧ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) Fn ω ) → ( ( ♯ ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ↔ ∀ 𝑦 ∈ ω ( ( ♯ ↾ ω ) ‘ 𝑦 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ 𝑦 ) ) )
4 1 2 3 mp2an ⊢ ( ( ♯ ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ↔ ∀ 𝑦 ∈ ω ( ( ♯ ↾ ω ) ‘ 𝑦 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ 𝑦 ) )
5 fvres ⊢ ( 𝑦 ∈ ω → ( ( ♯ ↾ ω ) ‘ 𝑦 ) = ( ♯ ‘ 𝑦 ) )
6 nnfi ⊢ ( 𝑦 ∈ ω → 𝑦 ∈ Fin )
7 eqid ⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
8 7 hashgval ⊢ ( 𝑦 ∈ Fin → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝑦 ) ) = ( ♯ ‘ 𝑦 ) )
9 6 8 syl ⊢ ( 𝑦 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝑦 ) ) = ( ♯ ‘ 𝑦 ) )
10 cardnn ⊢ ( 𝑦 ∈ ω → ( card ‘ 𝑦 ) = 𝑦 )
11 10 fveq2d ⊢ ( 𝑦 ∈ ω → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ ( card ‘ 𝑦 ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ 𝑦 ) )
12 5 9 11 3eqtr2d ⊢ ( 𝑦 ∈ ω → ( ( ♯ ↾ ω ) ‘ 𝑦 ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ‘ 𝑦 ) )
13 4 12 mprgbir ⊢ ( ♯ ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )