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	|- ( ( _om e. _V /\ A e. B ) -> ( -. A e. Fin <-> _om ~<_ A ) )

Proof

Step	Hyp	Ref	Expression
1		isfiniteg	|- ( _om e. _V -> ( A e. Fin <-> A ~< _om ) )
2	1	adantr	|- ( ( _om e. _V /\ A e. B ) -> ( A e. Fin <-> A ~< _om ) )
3	2	notbid	|- ( ( _om e. _V /\ A e. B ) -> ( -. A e. Fin <-> -. A ~< _om ) )
4		domtri	|- ( ( _om e. _V /\ A e. B ) -> ( _om ~<_ A <-> -. A ~< _om ) )
5	3 4	bitr4d	|- ( ( _om e. _V /\ A e. B ) -> ( -. A e. Fin <-> _om ~<_ A ) )