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		fndm	⊢ ( 𝐺 Fn ω → dom 𝐺 = ω )
15	5 14	ax-mp	⊢ dom 𝐺 = ω
16	15	imaeq2i	⊢ ( ◡ card “ dom 𝐺 ) = ( ◡ card “ ω )
17		funfn	⊢ ( Fun card ↔ card Fn dom card )
18	10 17	mpbi	⊢ card Fn dom card
19		elpreima	⊢ ( card Fn dom card → ( 𝑦 ∈ ( ◡ card “ ω ) ↔ ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) ) )
20	18 19	ax-mp	⊢ ( 𝑦 ∈ ( ◡ card “ ω ) ↔ ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) )
21		id	⊢ ( ( card ‘ 𝑦 ) ∈ ω → ( card ‘ 𝑦 ) ∈ ω )
22		cardid2	⊢ ( 𝑦 ∈ dom card → ( card ‘ 𝑦 ) ≈ 𝑦 )
23	22	ensymd	⊢ ( 𝑦 ∈ dom card → 𝑦 ≈ ( card ‘ 𝑦 ) )
24		breq2	⊢ ( 𝑥 = ( card ‘ 𝑦 ) → ( 𝑦 ≈ 𝑥 ↔ 𝑦 ≈ ( card ‘ 𝑦 ) ) )
25	24	rspcev	⊢ ( ( ( card ‘ 𝑦 ) ∈ ω ∧ 𝑦 ≈ ( card ‘ 𝑦 ) ) → ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 )
26	21 23 25	syl2anr	⊢ ( ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) → ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 )
27		isfi	⊢ ( 𝑦 ∈ Fin ↔ ∃ 𝑥 ∈ ω 𝑦 ≈ 𝑥 )
28	26 27	sylibr	⊢ ( ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) → 𝑦 ∈ Fin )
29		finnum	⊢ ( 𝑦 ∈ Fin → 𝑦 ∈ dom card )
30		ficardom	⊢ ( 𝑦 ∈ Fin → ( card ‘ 𝑦 ) ∈ ω )
31	29 30	jca	⊢ ( 𝑦 ∈ Fin → ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) )
32	28 31	impbii	⊢ ( ( 𝑦 ∈ dom card ∧ ( card ‘ 𝑦 ) ∈ ω ) ↔ 𝑦 ∈ Fin )
33	20 32	bitri	⊢ ( 𝑦 ∈ ( ◡ card “ ω ) ↔ 𝑦 ∈ Fin )
34	33	eqriv	⊢ ( ◡ card “ ω ) = Fin
35	13 16 34	3eqtri	⊢ dom ( 𝐺 ∘ card ) = Fin
36		df-fn	⊢ ( ( 𝐺 ∘ card ) Fn Fin ↔ ( Fun ( 𝐺 ∘ card ) ∧ dom ( 𝐺 ∘ card ) = Fin ) )
37	12 35 36	mpbir2an	⊢ ( 𝐺 ∘ card ) Fn Fin
38	2	fneq1i	⊢ ( 𝐾 Fn Fin ↔ ( 𝐺 ∘ card ) Fn Fin )
39	37 38	mpbir	⊢ 𝐾 Fn Fin
40	2	fveq1i	⊢ ( 𝐾 ‘ 𝑦 ) = ( ( 𝐺 ∘ card ) ‘ 𝑦 )
41		fvco	⊢ ( ( Fun card ∧ 𝑦 ∈ dom card ) → ( ( 𝐺 ∘ card ) ‘ 𝑦 ) = ( 𝐺 ‘ ( card ‘ 𝑦 ) ) )
42	10 29 41	sylancr	⊢ ( 𝑦 ∈ Fin → ( ( 𝐺 ∘ card ) ‘ 𝑦 ) = ( 𝐺 ‘ ( card ‘ 𝑦 ) ) )
43	40 42	syl5eq	⊢ ( 𝑦 ∈ Fin → ( 𝐾 ‘ 𝑦 ) = ( 𝐺 ‘ ( card ‘ 𝑦 ) ) )
44	1	hashgf1o	⊢ 𝐺 : ω –1-1-onto→ ℕ0
45		f1of	⊢ ( 𝐺 : ω –1-1-onto→ ℕ0 → 𝐺 : ω ⟶ ℕ0 )
46	44 45	ax-mp	⊢ 𝐺 : ω ⟶ ℕ0
47	46	ffvelrni	⊢ ( ( card ‘ 𝑦 ) ∈ ω → ( 𝐺 ‘ ( card ‘ 𝑦 ) ) ∈ ℕ0 )
48	30 47	syl	⊢ ( 𝑦 ∈ Fin → ( 𝐺 ‘ ( card ‘ 𝑦 ) ) ∈ ℕ0 )
49	43 48	eqeltrd	⊢ ( 𝑦 ∈ Fin → ( 𝐾 ‘ 𝑦 ) ∈ ℕ0 )
50	49	rgen	⊢ ∀ 𝑦 ∈ Fin ( 𝐾 ‘ 𝑦 ) ∈ ℕ0
51		ffnfv	⊢ ( 𝐾 : Fin ⟶ ℕ0 ↔ ( 𝐾 Fn Fin ∧ ∀ 𝑦 ∈ Fin ( 𝐾 ‘ 𝑦 ) ∈ ℕ0 ) )
52	39 50 51	mpbir2an	⊢ 𝐾 : Fin ⟶ ℕ0