Description: Alternate definition of IV-finite sets: they lack a denumerable subset. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 17-May-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | isfin4-2 | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | isfin4 | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIV ↔ ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ) ) | |
2 | infpssr | ⊢ ( ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) → ω ≼ 𝐴 ) | |
3 | 2 | exlimiv | ⊢ ( ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) → ω ≼ 𝐴 ) |
4 | infpss | ⊢ ( ω ≼ 𝐴 → ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ) | |
5 | 3 4 | impbii | ⊢ ( ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ↔ ω ≼ 𝐴 ) |
6 | 5 | notbii | ⊢ ( ¬ ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ↔ ¬ ω ≼ 𝐴 ) |
7 | 1 6 | bitrdi | ⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ∈ FinIV ↔ ¬ ω ≼ 𝐴 ) ) |