Metamath Proof Explorer

Theorem isinf2

Description: The converse of isinf . Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set hascountably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by ML, 14-Dec-2020)

Ref Expression
Assertion isinf2 ⊢ ∀ n ∈ ω ∃ x x ⊆ A ∧ x ≈ n → ¬ A ∈ Fin

Proof

Step Hyp Ref Expression
1 ssdomg ⊢ A ∈ V → x ⊆ A → x ≼ A
2 1 adantr ⊢ A ∈ V ∧ x ≈ n → x ⊆ A → x ≼ A
3 domen1 ⊢ x ≈ n → x ≼ A ↔ n ≼ A
4 3 adantl ⊢ A ∈ V ∧ x ≈ n → x ≼ A ↔ n ≼ A
5 2 4 sylibd ⊢ A ∈ V ∧ x ≈ n → x ⊆ A → n ≼ A
6 5 expimpd ⊢ A ∈ V → x ≈ n ∧ x ⊆ A → n ≼ A
7 6 ancomsd ⊢ A ∈ V → x ⊆ A ∧ x ≈ n → n ≼ A
8 7 exlimdv ⊢ A ∈ V → ∃ x x ⊆ A ∧ x ≈ n → n ≼ A
9 8 ralimdv ⊢ A ∈ V → ∀ n ∈ ω ∃ x x ⊆ A ∧ x ≈ n → ∀ n ∈ ω n ≼ A
10 domalom ⊢ ∀ n ∈ ω n ≼ A → ¬ A ∈ Fin
11 9 10 syl6 ⊢ A ∈ V → ∀ n ∈ ω ∃ x x ⊆ A ∧ x ≈ n → ¬ A ∈ Fin
12 prcnel ⊢ ¬ A ∈ V → ¬ A ∈ Fin
13 12 a1d ⊢ ¬ A ∈ V → ∀ n ∈ ω ∃ x x ⊆ A ∧ x ≈ n → ¬ A ∈ Fin
14 11 13 pm2.61i ⊢ ∀ n ∈ ω ∃ x x ⊆ A ∧ x ≈ n → ¬ A ∈ Fin