ishashinf

Description: Any set that is not finite contains subsets of arbitrarily large finite cardinality. Cf. isinf . (Contributed by Thierry Arnoux, 5-Jul-2017)

		Ref	Expression
	Assertion	ishashinf	$⊢ \neg A \in Fin \to \forall n \in ℕ \exists x \in 𝒫 A \|x\| = n$

Proof

Step	Hyp	Ref	Expression
1		fzfid	$⊢ n \in ℕ \to (1 \dots n) \in Fin$
2		ficardom	$⊢ (1 \dots n) \in Fin \to card ((1 \dots n)) \in ω$
3	1 2	syl	$⊢ n \in ℕ \to card ((1 \dots n)) \in ω$
4		isinf	$⊢ \neg A \in Fin \to \forall a \in ω \exists x (x \subseteq A \land x \approx a)$
5		breq2	$⊢ a = card ((1 \dots n)) \to (x \approx a \leftrightarrow x \approx card ((1 \dots n)))$
6	5	anbi2d	$⊢ a = card ((1 \dots n)) \to ((x \subseteq A \land x \approx a) \leftrightarrow (x \subseteq A \land x \approx card ((1 \dots n))))$
7	6	exbidv	$⊢ a = card ((1 \dots n)) \to (\exists x (x \subseteq A \land x \approx a) \leftrightarrow \exists x (x \subseteq A \land x \approx card ((1 \dots n))))$
8	7	rspcva	$⊢ (card ((1 \dots n)) \in ω \land \forall a \in ω \exists x (x \subseteq A \land x \approx a)) \to \exists x (x \subseteq A \land x \approx card ((1 \dots n)))$
9	3 4 8	syl2anr	$⊢ (\neg A \in Fin \land n \in ℕ) \to \exists x (x \subseteq A \land x \approx card ((1 \dots n)))$
10		velpw	$⊢ x \in 𝒫 A \leftrightarrow x \subseteq A$
11	10	biimpri	$⊢ x \subseteq A \to x \in 𝒫 A$
12	11	a1i	$⊢ (\neg A \in Fin \land n \in ℕ) \to (x \subseteq A \to x \in 𝒫 A)$
13		hasheni	$⊢ x \approx card ((1 \dots n)) \to \|x\| = \|card ((1 \dots n))\|$
14	13	adantl	$⊢ ((\neg A \in Fin \land n \in ℕ) \land x \approx card ((1 \dots n))) \to \|x\| = \|card ((1 \dots n))\|$
15		hashcard	$⊢ (1 \dots n) \in Fin \to \|card ((1 \dots n))\| = \|(1 \dots n)\|$
16	1 15	syl	$⊢ n \in ℕ \to \|card ((1 \dots n))\| = \|(1 \dots n)\|$
17		nnnn0	$⊢ n \in ℕ \to n \in ℕ_{0}$
18		hashfz1	$⊢ n \in ℕ_{0} \to \|(1 \dots n)\| = n$
19	17 18	syl	$⊢ n \in ℕ \to \|(1 \dots n)\| = n$
20	16 19	eqtrd	$⊢ n \in ℕ \to \|card ((1 \dots n))\| = n$
21	20	ad2antlr	$⊢ ((\neg A \in Fin \land n \in ℕ) \land x \approx card ((1 \dots n))) \to \|card ((1 \dots n))\| = n$
22	14 21	eqtrd	$⊢ ((\neg A \in Fin \land n \in ℕ) \land x \approx card ((1 \dots n))) \to \|x\| = n$
23	22	ex	$⊢ (\neg A \in Fin \land n \in ℕ) \to (x \approx card ((1 \dots n)) \to \|x\| = n)$
24	12 23	anim12d	$⊢ (\neg A \in Fin \land n \in ℕ) \to ((x \subseteq A \land x \approx card ((1 \dots n))) \to (x \in 𝒫 A \land \|x\| = n))$
25	24	eximdv	$⊢ (\neg A \in Fin \land n \in ℕ) \to (\exists x (x \subseteq A \land x \approx card ((1 \dots n))) \to \exists x (x \in 𝒫 A \land \|x\| = n))$
26	9 25	mpd	$⊢ (\neg A \in Fin \land n \in ℕ) \to \exists x (x \in 𝒫 A \land \|x\| = n)$
27		df-rex	$⊢ \exists x \in 𝒫 A \|x\| = n \leftrightarrow \exists x (x \in 𝒫 A \land \|x\| = n)$
28	26 27	sylibr	$⊢ (\neg A \in Fin \land n \in ℕ) \to \exists x \in 𝒫 A \|x\| = n$
29	28	ralrimiva	$⊢ \neg A \in Fin \to \forall n \in ℕ \exists x \in 𝒫 A \|x\| = n$

Metamath Proof Explorer

Theorem ishashinf

Proof