Theorem infinf

Description: Equivalence between two infiniteness criteria for sets. (Contributed by David Moews, 1-May-2017)

	Ref	Expression
Assertion	infinf	⊢ ( 𝐴 ∈ 𝐵 → ( ¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		omex	⊢ ω ∈ V
2		domtri	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ 𝐵 ) → ( ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω ) )
3	1 2	mpan	⊢ ( 𝐴 ∈ 𝐵 → ( ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω ) )
4		isfinite	⊢ ( 𝐴 ∈ Fin ↔ 𝐴 ≺ ω )
5	4	notbii	⊢ ( ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ≺ ω )
6	3 5	syl6rbbr	⊢ ( 𝐴 ∈ 𝐵 → ( ¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴 ) )