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