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		incom	⊢ ( ( V ∖ Fin ) ∩ Fin ) = ( Fin ∩ ( V ∖ Fin ) )
10		disjdif	⊢ ( Fin ∩ ( V ∖ Fin ) ) = ∅
11	9 10	eqtri	⊢ ( ( V ∖ Fin ) ∩ Fin ) = ∅
12		pnfex	⊢ +∞ ∈ V
13	12	fconst	⊢ ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ }
14		ffn	⊢ ( ( ( V ∖ Fin ) × { +∞ } ) : ( V ∖ Fin ) ⟶ { +∞ } → ( ( V ∖ Fin ) × { +∞ } ) Fn ( V ∖ Fin ) )
15		fnresdisj	⊢ ( ( ( V ∖ Fin ) × { +∞ } ) Fn ( V ∖ Fin ) → ( ( ( V ∖ Fin ) ∩ Fin ) = ∅ ↔ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅ ) )
16	13 14 15	mp2b	⊢ ( ( ( V ∖ Fin ) ∩ Fin ) = ∅ ↔ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅ )
17	11 16	mpbi	⊢ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) = ∅
18	8 17	uneq12i	⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) ) = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ∅ )
19		un0	⊢ ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ∅ ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
20	18 19	eqtri	⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ↾ Fin ) ∪ ( ( ( V ∖ Fin ) × { +∞ } ) ↾ Fin ) ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
21	2 20	eqtri	⊢ ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ Fin ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
22		df-hash	⊢ ♯ = ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) )
23	22	reseq1i	⊢ ( ♯ ↾ Fin ) = ( ( ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card ) ∪ ( ( V ∖ Fin ) × { +∞ } ) ) ↾ Fin )
24	1	coeq1i	⊢ ( 𝐺 ∘ card ) = ( ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) ∘ card )
25	21 23 24	3eqtr4i	⊢ ( ♯ ↾ Fin ) = ( 𝐺 ∘ card )
26	25	fveq1i	⊢ ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( ( 𝐺 ∘ card ) ‘ 𝐴 )
27		cardf2	⊢ card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On
28		ffun	⊢ ( card : { 𝑥 ∣ ∃ 𝑦 ∈ On 𝑦 ≈ 𝑥 } ⟶ On → Fun card )
29	27 28	ax-mp	⊢ Fun card
30		finnum	⊢ ( 𝐴 ∈ Fin → 𝐴 ∈ dom card )
31		fvco	⊢ ( ( Fun card ∧ 𝐴 ∈ dom card ) → ( ( 𝐺 ∘ card ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) )
32	29 30 31	sylancr	⊢ ( 𝐴 ∈ Fin → ( ( 𝐺 ∘ card ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) )
33	26 32	syl5eq	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( 𝐺 ‘ ( card ‘ 𝐴 ) ) )
34		fvres	⊢ ( 𝐴 ∈ Fin → ( ( ♯ ↾ Fin ) ‘ 𝐴 ) = ( ♯ ‘ 𝐴 ) )
35	33 34	eqtr3d	⊢ ( 𝐴 ∈ Fin → ( 𝐺 ‘ ( card ‘ 𝐴 ) ) = ( ♯ ‘ 𝐴 ) )

Metamath Proof Explorer

Theorem hashgval

Proof