hashgval

Description: The value of the # function in terms of the mapping G from _om to NN0 . The proof avoids the use of ax-ac . (Contributed by Paul Chapman, 22-Jun-2011) (Revised by Mario Carneiro, 26-Dec-2014)

		Ref	Expression
	Hypothesis	hashgval.1	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
	Assertion	hashgval	⊢ ( 𝐴 ∈ Fin → ( 𝐺 ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		hashgval.1	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
2		resundir	⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ Fin ) = ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) )
3		eqid	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
4		eqid	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
5	3 4	hashkf	⊢ ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) : Fin ⟶ ℕ₀
6		ffn	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) : Fin ⟶ ℕ₀ → ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) Fn Fin )
7		fnresdm	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) Fn Fin → ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) )
8	5 6 7	mp2b	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
9		disjdifr	⊢ ( ( V ∖ Fin ) ∩ Fin ) = ∅
10		pnfex	⊢ +∞ ∈ V
11	10	fconst	⊢ ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ }
12		ffn	⊢ ( ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ } → ( ( V ∖ Fin ) × { +∞ } ) Fn ( V ∖ Fin ) )
13		fnresdisj	⊢ ( ( ( V ∖ Fin ) × { +∞ } ) Fn ( V ∖ Fin ) → ( ( ( V ∖ Fin ) ∩ Fin ) = ∅ ↔ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅ ) )
14	11 12 13	mp2b	⊢ ( ( ( V ∖ Fin ) ∩ Fin ) = ∅ ↔ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅ )
15	9 14	mpbi	⊢ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅
16	8 15	uneq12i	⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ∅ )
17		un0	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ∅ ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
18	16 17	eqtri	⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
19	2 18	eqtri	⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ Fin ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
20		df-hash	⊢ ♯ = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) )
21	20	reseq1i	⊢ ( ♯ ↾ Fin ) = ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ Fin )
22	1	coeq1i	⊢ ( 𝐺 ∘ card ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
23	19 21 22	3eqtr4i	⊢ ( ♯ ↾ Fin ) = ( 𝐺 ∘ card )
24	23	fveq1i	⊢ ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( ( 𝐺 ∘ card ) ‘ 𝐴 )
25		cardf2	⊢ card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On
26		ffun	⊢ ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On → Fun card )
27	25 26	ax-mp	⊢ Fun card
28		finnum	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card )
29		fvco	⊢ ( ( Fun card ∧ 𝐴 ∈ dom card ) → ( ( 𝐺 ∘ card ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) )
30	27 28 29	sylancr	⊢ ( 𝐴 ∈ Fin → ( ( 𝐺 ∘ card ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) )
31	24 30	eqtrid	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) )
32		fvres	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) )
33	31 32	eqtr3d	⊢ ( 𝐴 ∈ Fin → ( 𝐺 ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )

Metamath Proof Explorer

Theorem hashgval

Proof