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	$⊢ G = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
	hashkf.2	$⊢ K = G \circ card$
Assertion	hashkf	$⊢ K : Fin ⟶ ℕ_{0}$

Proof

Step	Hyp	Ref	Expression
1		hashgval.1	$⊢ G = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
2		hashkf.2	$⊢ K = G \circ card$
3		frfnom	$⊢ ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) Fn ω$
4	1	fneq1i	$⊢ G Fn ω \leftrightarrow ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) Fn ω$
5	3 4	mpbir	$⊢ G Fn ω$
6		fnfun	$⊢ G Fn ω \to Fun G$
7	5 6	ax-mp	$⊢ Fun G$
8		cardf2	$⊢ card : \{y \| \exists x \in On x \approx y\} ⟶ On$
9		ffun	$⊢ card : \{y \| \exists x \in On x \approx y\} ⟶ On \to Fun card$
10	8 9	ax-mp	$⊢ Fun card$
11		funco	$⊢ (Fun G \land Fun card) \to Fun (G \circ card)$
12	7 10 11	mp2an	$⊢ Fun (G \circ card)$
13		dmco	$⊢ dom (G \circ card) = {card}^{-1} [dom G]$
14	5	fndmi	$⊢ dom G = ω$
15	14	imaeq2i	$⊢ {card}^{-1} [dom G] = {card}^{-1} [ω]$
16		funfn	$⊢ Fun card \leftrightarrow card Fn dom card$
17	10 16	mpbi	$⊢ card Fn dom card$
18		elpreima	$⊢ card Fn dom card \to (y \in {card}^{-1} [ω] \leftrightarrow (y \in dom card \land card (y) \in ω))$
19	17 18	ax-mp	$⊢ y \in {card}^{-1} [ω] \leftrightarrow (y \in dom card \land card (y) \in ω)$
20		id	$⊢ card (y) \in ω \to card (y) \in ω$
21		cardid2	$⊢ y \in dom card \to card (y) \approx y$
22	21	ensymd	$⊢ y \in dom card \to y \approx card (y)$
23		breq2	$⊢ x = card (y) \to (y \approx x \leftrightarrow y \approx card (y))$
24	23	rspcev	$⊢ (card (y) \in ω \land y \approx card (y)) \to \exists x \in ω y \approx x$
25	20 22 24	syl2anr	$⊢ (y \in dom card \land card (y) \in ω) \to \exists x \in ω y \approx x$
26		isfi	$⊢ y \in Fin \leftrightarrow \exists x \in ω y \approx x$
27	25 26	sylibr	$⊢ (y \in dom card \land card (y) \in ω) \to y \in Fin$
28		finnum	$⊢ y \in Fin \to y \in dom card$
29		ficardom	$⊢ y \in Fin \to card (y) \in ω$
30	28 29	jca	$⊢ y \in Fin \to (y \in dom card \land card (y) \in ω)$
31	27 30	impbii	$⊢ (y \in dom card \land card (y) \in ω) \leftrightarrow y \in Fin$
32	19 31	bitri	$⊢ y \in {card}^{-1} [ω] \leftrightarrow y \in Fin$
33	32	eqriv	$⊢ {card}^{-1} [ω] = Fin$
34	13 15 33	3eqtri	$⊢ dom (G \circ card) = Fin$
35		df-fn	$⊢ (G \circ card) Fn Fin \leftrightarrow (Fun (G \circ card) \land dom (G \circ card) = Fin)$
36	12 34 35	mpbir2an	$⊢ (G \circ card) Fn Fin$
37	2	fneq1i	$⊢ K Fn Fin \leftrightarrow (G \circ card) Fn Fin$
38	36 37	mpbir	$⊢ K Fn Fin$
39	2	fveq1i	$⊢ K (y) = (G \circ card) (y)$
40		fvco	$⊢ (Fun card \land y \in dom card) \to (G \circ card) (y) = G (card (y))$
41	10 28 40	sylancr	$⊢ y \in Fin \to (G \circ card) (y) = G (card (y))$
42	39 41	eqtrid	$⊢ y \in Fin \to K (y) = G (card (y))$
43	1	hashgf1o	$⊢ G : ω \underset{1-1 onto}{⟶} ℕ_{0}$
44		f1of	$⊢ G : ω \underset{1-1 onto}{⟶} ℕ_{0} \to G : ω ⟶ ℕ_{0}$
45	43 44	ax-mp	$⊢ G : ω ⟶ ℕ_{0}$
46	45	ffvelrni	$⊢ card (y) \in ω \to G (card (y)) \in ℕ_{0}$
47	29 46	syl	$⊢ y \in Fin \to G (card (y)) \in ℕ_{0}$
48	42 47	eqeltrd	$⊢ y \in Fin \to K (y) \in ℕ_{0}$
49	48	rgen	$⊢ \forall y \in Fin K (y) \in ℕ_{0}$
50		ffnfv	$⊢ K : Fin ⟶ ℕ_{0} \leftrightarrow (K Fn Fin \land \forall y \in Fin K (y) \in ℕ_{0})$
51	38 49 50	mpbir2an	$⊢ K : Fin ⟶ ℕ_{0}$

Metamath Proof Explorer

Theorem hashkf

Proof