Metamath Proof Explorer


Theorem isfin4-2

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 ↔ ¬ ω ≼ 𝐴 ) )

Proof

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 ↔ ¬ ω ≼ 𝐴 ) )