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 ) ↾ ω )