Theorem hashkf

Description: The finite part of the size function maps all finite sets to their cardinality, as members of NN0 . (Contributed by Mario Carneiro, 13-Sep-2013) (Revised by Mario Carneiro, 26-Dec-2014)

	Ref	Expression
Hypotheses	hashgval.1	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
	hashkf.2	⊢ 𝐾 = ( 𝐺 ∘ card )
Assertion	hashkf	⊢ 𝐾 : Fin ⟶ ℕ0

Proof

Step	Hyp	Ref	Expression
1		hashgval.1	⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω )
2		hashkf.2	⊢ 𝐾 = ( 𝐺 ∘ card )
3		frfnom	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) Fn ω
4	1	fneq1i	⊢ ( 𝐺 Fn ω ↔ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 0 ) ↾ ω ) Fn ω )
5	3 4	mpbir	⊢ 𝐺 Fn ω
6		fnfun	⊢ ( 𝐺 Fn ω → Fun 𝐺 )
7	5 6	ax-mp	⊢ Fun 𝐺
8		cardf2	⊢ card : { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑥 ≈ 𝑦 } ⟶ On
9		ffun	⊢ ( card : { 𝑦 ∣ ∃ 𝑥 ∈ On 𝑥 ≈ 𝑦 } ⟶ On → Fun card )
10	8 9	ax-mp	⊢ Fun card
11		funco	⊢ ( ( Fun 𝐺 ∧ Fun card ) → Fun ( 𝐺 ∘ card ) )
12	7 10 11	mp2an	⊢ Fun ( 𝐺 ∘ card )
13		dmco	⊢ dom ( 𝐺 ∘ card ) = ( ◡ card “ dom 𝐺 )
14	5	fndmi	⊢ dom 𝐺 = ω
15	14	imaeq2i	⊢ ( ◡ card “ dom 𝐺 ) = ( ◡ card “ ω )
16		funfn	⊢ ( Fun card ↔ card Fn dom card )
17	10 16	mpbi	⊢ card Fn dom card
18		elpreima	⊢ ( card Fn dom card → ( 𝑦 ∈ ( ◡ card “ ω ) ↔ ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) ) )
19	17 18	ax-mp	⊢ ( 𝑦 ∈ ( ◡ card “ ω ) ↔ ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) )
20		id	⊢ ( ( card ‘ 𝑦 ) ∈ ω → ( card ‘ 𝑦 ) ∈ ω )
21		cardid2	⊢ ( 𝑦 ∈ dom card → ( card ‘ 𝑦 ) ≈ 𝑦 )
22	21	ensymd	⊢ ( 𝑦 ∈ dom card → 𝑦 ≈ ( card ‘ 𝑦 ) )
23		breq2	⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( 𝑦 ≈ 𝑥 ↔ 𝑦 ≈ ( card ‘ 𝑦 ) ) )
24	23	rspcev	⊢ ( ( ( card ‘ 𝑦 ) ∈ ω ∧ 𝑦 ≈ ( card ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 )
25	20 22 24	syl2anr	⊢ ( ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) → ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 )
26		isfi	⊢ ( 𝑦 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 )
27	25 26	sylibr	⊢ ( ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) → 𝑦 ∈ Fin )
28		finnum	⊢ ( 𝑦 ∈ Fin → 𝑦 ∈ dom card )
29		ficardom	⊢ ( 𝑦 ∈ Fin → ( card ‘ 𝑦 ) ∈ ω )
30	28 29	jca	⊢ ( 𝑦 ∈ Fin → ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) )
31	27 30	impbii	⊢ ( ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) ↔ 𝑦 ∈ Fin )
32	19 31	bitri	⊢ ( 𝑦 ∈ ( ◡ card “ ω ) ↔ 𝑦 ∈ Fin )
33	32	eqriv	⊢ ( ◡ card “ ω ) = Fin
34	13 15 33	3eqtri	⊢ dom ( 𝐺 ∘ card ) = Fin
35		df-fn	⊢ ( ( 𝐺 ∘ card ) Fn Fin ↔ ( Fun ( 𝐺 ∘ card ) ∧ dom ( 𝐺 ∘ card ) = Fin ) )
36	12 34 35	mpbir2an	⊢ ( 𝐺 ∘ card ) Fn Fin
37	2	fneq1i	⊢ ( 𝐾 Fn Fin ↔ ( 𝐺 ∘ card ) Fn Fin )
38	36 37	mpbir	⊢ 𝐾 Fn Fin
39	2	fveq1i	⊢ ( 𝐾 ‘ 𝑦 ) = ( ( 𝐺 ∘ card ) ‘ 𝑦 )
40		fvco	⊢ ( ( Fun card ∧ 𝑦 ∈ dom card ) → ( ( 𝐺 ∘ card ) ‘ 𝑦 ) = ( 𝐺 ‘ ( card ‘ 𝑦 ) ) )
41	10 28 40	sylancr	⊢ ( 𝑦 ∈ Fin → ( ( 𝐺 ∘ card ) ‘ 𝑦 ) = ( 𝐺 ‘ ( card ‘ 𝑦 ) ) )
42	39 41	eqtrid	⊢ ( 𝑦 ∈ Fin → ( 𝐾 ‘ 𝑦 ) = ( 𝐺 ‘ ( card ‘ 𝑦 ) ) )
43	1	hashgf1o	⊢ 𝐺 : ω –1-1-onto→ ℕ0
44		f1of	⊢ ( 𝐺 : ω –1-1-onto→ ℕ0 → 𝐺 : ω ⟶ ℕ0 )
45	43 44	ax-mp	⊢ 𝐺 : ω ⟶ ℕ0
46	45	ffvelcdmi	⊢ ( ( card ‘ 𝑦 ) ∈ ω → ( 𝐺 ‘ ( card ‘ 𝑦 ) ) ∈ ℕ0 )
47	29 46	syl	⊢ ( 𝑦 ∈ Fin → ( 𝐺 ‘ ( card ‘ 𝑦 ) ) ∈ ℕ0 )
48	42 47	eqeltrd	⊢ ( 𝑦 ∈ Fin → ( 𝐾 ‘ 𝑦 ) ∈ ℕ0 )
49	48	rgen	⊢ ∀ 𝑦 ∈ Fin ( 𝐾 ‘ 𝑦 ) ∈ ℕ0
50		ffnfv	⊢ ( 𝐾 : Fin ⟶ ℕ0 ↔ ( 𝐾 Fn Fin ∧ ∀ 𝑦 ∈ Fin ( 𝐾 ‘ 𝑦 ) ∈ ℕ0 ) )
51	38 49 50	mpbir2an	⊢ 𝐾 : Fin ⟶ ℕ0