Metamath Proof Explorer

Theorem 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 ( ¬ 𝐴 ∈ Fin → ∀ 𝑛 ∈ ℕ ∃ 𝑥 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑥 ) = 𝑛 )

Proof

Step Hyp Ref Expression
1 fzfid ⊢ ( 𝑛 ∈ ℕ → ( 1 ... 𝑛 ) ∈ Fin )
2 ficardom ⊢ ( ( 1 ... 𝑛 ) ∈ Fin → ( card ‘ ( 1 ... 𝑛 ) ) ∈ ω )
3 1 2 syl ⊢ ( 𝑛 ∈ ℕ → ( card ‘ ( 1 ... 𝑛 ) ) ∈ ω )
4 isinf ⊢ ( ¬ 𝐴 ∈ Fin → ∀ 𝑎 ∈ ω ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑎 ) )
5 breq2 ⊢ ( 𝑎 = ( card ‘ ( 1 ... 𝑛 ) ) → ( 𝑥 ≈ 𝑎 ↔ 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) ) )
6 5 anbi2d ⊢ ( 𝑎 = ( card ‘ ( 1 ... 𝑛 ) ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑎 ) ↔ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) ) ) )
7 6 exbidv ⊢ ( 𝑎 = ( card ‘ ( 1 ... 𝑛 ) ) → ( ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑎 ) ↔ ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) ) ) )
8 7 rspcva ⊢ ( ( ( card ‘ ( 1 ... 𝑛 ) ) ∈ ω ∧ ∀ 𝑎 ∈ ω ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝑎 ) ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) ) )
9 3 4 8 syl2anr ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑛 ∈ ℕ ) → ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) ) )
10 velpw ⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
11 10 biimpri ⊢ ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝒫 𝐴 )
12 11 a1i ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ⊆ 𝐴 → 𝑥 ∈ 𝒫 𝐴 ) )
13 hasheni ⊢ ( 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ( card ‘ ( 1 ... 𝑛 ) ) ) )
14 13 adantl ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) ) → ( ♯ ‘ 𝑥 ) = ( ♯ ‘ ( card ‘ ( 1 ... 𝑛 ) ) ) )
15 hashcard ⊢ ( ( 1 ... 𝑛 ) ∈ Fin → ( ♯ ‘ ( card ‘ ( 1 ... 𝑛 ) ) ) = ( ♯ ‘ ( 1 ... 𝑛 ) ) )
16 1 15 syl ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ ( card ‘ ( 1 ... 𝑛 ) ) ) = ( ♯ ‘ ( 1 ... 𝑛 ) ) )
17 nnnn0 ⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℕ0 )
18 hashfz1 ⊢ ( 𝑛 ∈ ℕ0 → ( ♯ ‘ ( 1 ... 𝑛 ) ) = 𝑛 )
19 17 18 syl ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ ( 1 ... 𝑛 ) ) = 𝑛 )
20 16 19 eqtrd ⊢ ( 𝑛 ∈ ℕ → ( ♯ ‘ ( card ‘ ( 1 ... 𝑛 ) ) ) = 𝑛 )
21 20 ad2antlr ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) ) → ( ♯ ‘ ( card ‘ ( 1 ... 𝑛 ) ) ) = 𝑛 )
22 14 21 eqtrd ⊢ ( ( ( ¬ 𝐴 ∈ Fin ∧ 𝑛 ∈ ℕ ) ∧ 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) ) → ( ♯ ‘ 𝑥 ) = 𝑛 )
23 22 ex ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑛 ∈ ℕ ) → ( 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) → ( ♯ ‘ 𝑥 ) = 𝑛 ) )
24 12 23 anim12d ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑛 ∈ ℕ ) → ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) ) → ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) ) )
25 24 eximdv ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑛 ∈ ℕ ) → ( ∃ 𝑥 ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ ( card ‘ ( 1 ... 𝑛 ) ) ) → ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) ) )
26 9 25 mpd ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑛 ∈ ℕ ) → ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) )
27 df-rex ⊢ ( ∃ 𝑥 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑥 ) = 𝑛 ↔ ∃ 𝑥 ( 𝑥 ∈ 𝒫 𝐴 ∧ ( ♯ ‘ 𝑥 ) = 𝑛 ) )
28 26 27 sylibr ⊢ ( ( ¬ 𝐴 ∈ Fin ∧ 𝑛 ∈ ℕ ) → ∃ 𝑥 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑥 ) = 𝑛 )
29 28 ralrimiva ⊢ ( ¬ 𝐴 ∈ Fin → ∀ 𝑛 ∈ ℕ ∃ 𝑥 ∈ 𝒫 𝐴 ( ♯ ‘ 𝑥 ) = 𝑛 )