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	$⊢ G = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
	Assertion	hashgval	$⊢ A \in Fin \to G (card (A)) = \|A\|$

Proof

Step	Hyp	Ref	Expression
1		hashgval.1	$⊢ G = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
2		resundir	$⊢ {((({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})) ↾}_{Fin} = ({(({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) ↾}_{Fin}) \cup ({((V ∖ Fin) \times \{+∞\}) ↾}_{Fin})$
3		eqid	$⊢ {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
4		eqid	$⊢ ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card$
5	3 4	hashkf	$⊢ (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) : Fin ⟶ ℕ_{0}$
6		ffn	$⊢ (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) : Fin ⟶ ℕ_{0} \to (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) Fn Fin$
7		fnresdm	$⊢ (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) Fn Fin \to {(({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) ↾}_{Fin} = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card$
8	5 6 7	mp2b	$⊢ {(({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) ↾}_{Fin} = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card$
9		incom	$⊢ (V ∖ Fin) \cap Fin = Fin \cap (V ∖ Fin)$
10		disjdif	$⊢ Fin \cap (V ∖ Fin) = \emptyset$
11	9 10	eqtri	$⊢ (V ∖ Fin) \cap Fin = \emptyset$
12		pnfex	$⊢ +∞ \in V$
13	12	fconst	$⊢ ((V ∖ Fin) \times \{+∞\}) : V ∖ Fin ⟶ \{+∞\}$
14		ffn	$⊢ ((V ∖ Fin) \times \{+∞\}) : V ∖ Fin ⟶ \{+∞\} \to ((V ∖ Fin) \times \{+∞\}) Fn (V ∖ Fin)$
15		fnresdisj	$⊢ ((V ∖ Fin) \times \{+∞\}) Fn (V ∖ Fin) \to ((V ∖ Fin) \cap Fin = \emptyset \leftrightarrow {((V ∖ Fin) \times \{+∞\}) ↾}_{Fin} = \emptyset)$
16	13 14 15	mp2b	$⊢ (V ∖ Fin) \cap Fin = \emptyset \leftrightarrow {((V ∖ Fin) \times \{+∞\}) ↾}_{Fin} = \emptyset$
17	11 16	mpbi	$⊢ {((V ∖ Fin) \times \{+∞\}) ↾}_{Fin} = \emptyset$
18	8 17	uneq12i	$⊢ ({(({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) ↾}_{Fin}) \cup ({((V ∖ Fin) \times \{+∞\}) ↾}_{Fin}) = (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup \emptyset$
19		un0	$⊢ (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup \emptyset = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card$
20	18 19	eqtri	$⊢ ({(({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) ↾}_{Fin}) \cup ({((V ∖ Fin) \times \{+∞\}) ↾}_{Fin}) = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card$
21	2 20	eqtri	$⊢ {((({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})) ↾}_{Fin} = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card$
22		df-hash	$⊢ \|.\| = (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})$
23	22	reseq1i	$⊢ {\|.\| ↾}_{Fin} = {((({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})) ↾}_{Fin}$
24	1	coeq1i	$⊢ G \circ card = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card$
25	21 23 24	3eqtr4i	$⊢ {\|.\| ↾}_{Fin} = G \circ card$
26	25	fveq1i	$⊢ ({\|.\| ↾}_{Fin}) (A) = (G \circ card) (A)$
27		cardf2	$⊢ card : \{x \| \exists y \in On y \approx x\} ⟶ On$
28		ffun	$⊢ card : \{x \| \exists y \in On y \approx x\} ⟶ On \to Fun card$
29	27 28	ax-mp	$⊢ Fun card$
30		finnum	$⊢ A \in Fin \to A \in dom card$
31		fvco	$⊢ (Fun card \land A \in dom card) \to (G \circ card) (A) = G (card (A))$
32	29 30 31	sylancr	$⊢ A \in Fin \to (G \circ card) (A) = G (card (A))$
33	26 32	syl5eq	$⊢ A \in Fin \to ({\|.\| ↾}_{Fin}) (A) = G (card (A))$
34		fvres	$⊢ A \in Fin \to ({\|.\| ↾}_{Fin}) (A) = \|A\|$
35	33 34	eqtr3d	$⊢ A \in Fin \to G (card (A)) = \|A\|$

Metamath Proof Explorer

Theorem hashgval

Proof