Theorem isinf2

Description: The converse of isinf . Any set that is not finite is literally infinite, in the sense that it contains subsets of arbitrarily large finite cardinality. (It cannot be proven that the set hascountably infinite subsets unless AC is invoked.) The proof does not require the Axiom of Infinity. (Contributed by ML, 14-Dec-2020)

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

Proof

Step	Hyp	Ref	Expression
1		ssdomg	|- ( A e. _V -> ( x C_ A -> x ~<_ A ) )
2	1	adantr	|- ( ( A e. _V /\ x ~~ n ) -> ( x C_ A -> x ~<_ A ) )
3		domen1	|- ( x ~~ n -> ( x ~<_ A <-> n ~<_ A ) )
4	3	adantl	|- ( ( A e. _V /\ x ~~ n ) -> ( x ~<_ A <-> n ~<_ A ) )
5	2 4	sylibd	|- ( ( A e. _V /\ x ~~ n ) -> ( x C_ A -> n ~<_ A ) )
6	5	expimpd	|- ( A e. _V -> ( ( x ~~ n /\ x C_ A ) -> n ~<_ A ) )
7	6	ancomsd	|- ( A e. _V -> ( ( x C_ A /\ x ~~ n ) -> n ~<_ A ) )
8	7	exlimdv	|- ( A e. _V -> ( E. x ( x C_ A /\ x ~~ n ) -> n ~<_ A ) )
9	8	ralimdv	|- ( A e. _V -> ( A. n e. _om E. x ( x C_ A /\ x ~~ n ) -> A. n e. _om n ~<_ A ) )
10		domalom	|- ( A. n e. _om n ~<_ A -> -. A e. Fin )
11	9 10	syl6	|- ( A e. _V -> ( A. n e. _om E. x ( x C_ A /\ x ~~ n ) -> -. A e. Fin ) )
12		prcnel	|- ( -. A e. _V -> -. A e. Fin )
13	12	a1d	|- ( -. A e. _V -> ( A. n e. _om E. x ( x C_ A /\ x ~~ n ) -> -. A e. Fin ) )
14	11 13	pm2.61i	|- ( A. n e. _om E. x ( x C_ A /\ x ~~ n ) -> -. A e. Fin )