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	$$⊢\left(\mathrm{\omega }\in \mathrm{V}\wedge A\in B\right)\to \left(\neg A\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\preccurlyeq A\right)$$

Proof

Step	Hyp	Ref	Expression
1		isfiniteg	$$⊢\mathrm{\omega }\in \mathrm{V}\to \left(A\in \mathrm{Fin}\leftrightarrow A\prec \mathrm{\omega }\right)$$
2	1	adantr	$$⊢\left(\mathrm{\omega }\in \mathrm{V}\wedge A\in B\right)\to \left(A\in \mathrm{Fin}\leftrightarrow A\prec \mathrm{\omega }\right)$$
3	2	notbid	$$⊢\left(\mathrm{\omega }\in \mathrm{V}\wedge A\in B\right)\to \left(\neg A\in \mathrm{Fin}\leftrightarrow \neg A\prec \mathrm{\omega }\right)$$
4		domtri	$$⊢\left(\mathrm{\omega }\in \mathrm{V}\wedge A\in B\right)\to \left(\mathrm{\omega }\preccurlyeq A\leftrightarrow \neg A\prec \mathrm{\omega }\right)$$
5	3 4	bitr4d	$$⊢\left(\mathrm{\omega }\in \mathrm{V}\wedge A\in B\right)\to \left(\neg A\in \mathrm{Fin}\leftrightarrow \mathrm{\omega }\preccurlyeq A\right)$$