Theorem prcinf

Description: Any proper class is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. This proof holds regardless of whether the Axiom of Infinity is accepted or negated. (Contributed by BTernaryTau, 22-Jun-2025)

	Ref	Expression
Assertion	prcinf	|- ( -. A e. _V -> A. n e. _om E. x ( x C_ A /\ x ~~ n ) )

Proof

Step	Hyp	Ref	Expression
1		elex	|- ( A e. Fin -> A e. _V )
2		isinf	|- ( -. A e. Fin -> A. n e. _om E. x ( x C_ A /\ x ~~ n ) )
3	1 2	nsyl5	|- ( -. A e. _V -> A. n e. _om E. x ( x C_ A /\ x ~~ n ) )