Theorem infinfg

Description: Equivalence between two infiniteness criteria for sets. To avoid the axiom of infinity, we include it as a hypothesis. (Contributed by Scott Fenton, 20-Feb-2026)

	Ref	Expression
Assertion	infinfg	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ 𝐵 ) → ( ¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		isfiniteg	⊢ ( ω ∈ V → ( 𝐴 ∈ Fin ↔ 𝐴 ≺ ω ) )
2	1	adantr	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ 𝐵 ) → ( 𝐴 ∈ Fin ↔ 𝐴 ≺ ω ) )
3	2	notbid	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ 𝐵 ) → ( ¬ 𝐴 ∈ Fin ↔ ¬ 𝐴 ≺ ω ) )
4		domtri	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ 𝐵 ) → ( ω ≼ 𝐴 ↔ ¬ 𝐴 ≺ ω ) )
5	3 4	bitr4d	⊢ ( ( ω ∈ V ∧ 𝐴 ∈ 𝐵 ) → ( ¬ 𝐴 ∈ Fin ↔ ω ≼ 𝐴 ) )