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		disjdifr	$⊢ (V ∖ Fin) \cap Fin = \emptyset$
10		pnfex	$⊢ +∞ \in V$
11	10	fconst	$⊢ ((V ∖ Fin) \times \{+∞\}) : V ∖ Fin ⟶ \{+∞\}$
12		ffn	$⊢ ((V ∖ Fin) \times \{+∞\}) : V ∖ Fin ⟶ \{+∞\} \to ((V ∖ Fin) \times \{+∞\}) Fn (V ∖ Fin)$
13		fnresdisj	$⊢ ((V ∖ Fin) \times \{+∞\}) Fn (V ∖ Fin) \to ((V ∖ Fin) \cap Fin = \emptyset \leftrightarrow {((V ∖ Fin) \times \{+∞\}) ↾}_{Fin} = \emptyset)$
14	11 12 13	mp2b	$⊢ (V ∖ Fin) \cap Fin = \emptyset \leftrightarrow {((V ∖ Fin) \times \{+∞\}) ↾}_{Fin} = \emptyset$
15	9 14	mpbi	$⊢ {((V ∖ Fin) \times \{+∞\}) ↾}_{Fin} = \emptyset$
16	8 15	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$
17		un0	$⊢ (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup \emptyset = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card$
18	16 17	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$
19	2 18	eqtri	$⊢ {((({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})) ↾}_{Fin} = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card$
20		df-hash	$⊢ \|.\| = (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})$
21	20	reseq1i	$⊢ {\|.\| ↾}_{Fin} = {((({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})) ↾}_{Fin}$
22	1	coeq1i	$⊢ G \circ card = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card$
23	19 21 22	3eqtr4i	$⊢ {\|.\| ↾}_{Fin} = G \circ card$
24	23	fveq1i	$⊢ ({\|.\| ↾}_{Fin}) (A) = (G \circ card) (A)$
25		cardf2	$⊢ card : \{x \| \exists y \in On y \approx x\} ⟶ On$
26		ffun	$⊢ card : \{x \| \exists y \in On y \approx x\} ⟶ On \to Fun card$
27	25 26	ax-mp	$⊢ Fun card$
28		finnum	$⊢ A \in Fin \to A \in dom card$
29		fvco	$⊢ (Fun card \land A \in dom card) \to (G \circ card) (A) = G (card (A))$
30	27 28 29	sylancr	$⊢ A \in Fin \to (G \circ card) (A) = G (card (A))$
31	24 30	eqtrid	$⊢ A \in Fin \to ({\|.\| ↾}_{Fin}) (A) = G (card (A))$
32		fvres	$⊢ A \in Fin \to ({\|.\| ↾}_{Fin}) (A) = \|A\|$
33	31 32	eqtr3d	$⊢ A \in Fin \to G (card (A)) = \|A\|$

Metamath Proof Explorer

Theorem hashgval

Proof