hashinf

Description: The value of the # function on an infinite set. (Contributed by Mario Carneiro, 13-Jul-2014)

		Ref	Expression
	Assertion	hashinf	$⊢ (A \in V \land \neg A \in Fin) \to \|A\| = +∞$

Proof

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in V \to A \in V$
2		eldif	$⊢ A \in (V ∖ Fin) \leftrightarrow (A \in V \land \neg A \in Fin)$
3		df-hash	$⊢ \|.\| = (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})$
4	3	reseq1i	$⊢ {\|.\| ↾}_{(V ∖ Fin)} = {((({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})) ↾}_{(V ∖ Fin)}$
5		resundir	$⊢ {((({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) \cup ((V ∖ Fin) \times \{+∞\})) ↾}_{(V ∖ Fin)} = ({(({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) ↾}_{(V ∖ Fin)}) \cup ({((V ∖ Fin) \times \{+∞\}) ↾}_{(V ∖ Fin)})$
6		disjdif	$⊢ Fin \cap (V ∖ Fin) = \emptyset$
7		eqid	$⊢ {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω} = {rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}$
8		eqid	$⊢ ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card = ({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card$
9	7 8	hashkf	$⊢ (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) : Fin ⟶ ℕ_{0}$
10		ffn	$⊢ (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) : Fin ⟶ ℕ_{0} \to (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) Fn Fin$
11		fnresdisj	$⊢ (({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) Fn Fin \to (Fin \cap (V ∖ Fin) = \emptyset \leftrightarrow {(({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) ↾}_{(V ∖ Fin)} = \emptyset)$
12	9 10 11	mp2b	$⊢ Fin \cap (V ∖ Fin) = \emptyset \leftrightarrow {(({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) ↾}_{(V ∖ Fin)} = \emptyset$
13	6 12	mpbi	$⊢ {(({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) ↾}_{(V ∖ Fin)} = \emptyset$
14		pnfex	$⊢ +∞ \in V$
15	14	fconst	$⊢ ((V ∖ Fin) \times \{+∞\}) : V ∖ Fin ⟶ \{+∞\}$
16		ffn	$⊢ ((V ∖ Fin) \times \{+∞\}) : V ∖ Fin ⟶ \{+∞\} \to ((V ∖ Fin) \times \{+∞\}) Fn (V ∖ Fin)$
17		fnresdm	$⊢ ((V ∖ Fin) \times \{+∞\}) Fn (V ∖ Fin) \to {((V ∖ Fin) \times \{+∞\}) ↾}_{(V ∖ Fin)} = (V ∖ Fin) \times \{+∞\}$
18	15 16 17	mp2b	$⊢ {((V ∖ Fin) \times \{+∞\}) ↾}_{(V ∖ Fin)} = (V ∖ Fin) \times \{+∞\}$
19	13 18	uneq12i	$⊢ ({(({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) ↾}_{(V ∖ Fin)}) \cup ({((V ∖ Fin) \times \{+∞\}) ↾}_{(V ∖ Fin)}) = \emptyset \cup ((V ∖ Fin) \times \{+∞\})$
20		uncom	$⊢ \emptyset \cup ((V ∖ Fin) \times \{+∞\}) = ((V ∖ Fin) \times \{+∞\}) \cup \emptyset$
21		un0	$⊢ ((V ∖ Fin) \times \{+∞\}) \cup \emptyset = (V ∖ Fin) \times \{+∞\}$
22	19 20 21	3eqtri	$⊢ ({(({rec ((x \in V ⟼ x + 1), 0) ↾}_{ω}) \circ card) ↾}_{(V ∖ Fin)}) \cup ({((V ∖ Fin) \times \{+∞\}) ↾}_{(V ∖ Fin)}) = (V ∖ Fin) \times \{+∞\}$
23	4 5 22	3eqtri	$⊢ {\|.\| ↾}_{(V ∖ Fin)} = (V ∖ Fin) \times \{+∞\}$
24	23	fveq1i	$⊢ ({\|.\| ↾}_{(V ∖ Fin)}) (A) = ((V ∖ Fin) \times \{+∞\}) (A)$
25		fvres	$⊢ A \in (V ∖ Fin) \to ({\|.\| ↾}_{(V ∖ Fin)}) (A) = \|A\|$
26	14	fvconst2	$⊢ A \in (V ∖ Fin) \to ((V ∖ Fin) \times \{+∞\}) (A) = +∞$
27	24 25 26	3eqtr3a	$⊢ A \in (V ∖ Fin) \to \|A\| = +∞$
28	2 27	sylbir	$⊢ (A \in V \land \neg A \in Fin) \to \|A\| = +∞$
29	1 28	sylan	$⊢ (A \in V \land \neg A \in Fin) \to \|A\| = +∞$

Metamath Proof Explorer

Theorem hashinf

Proof