Theorem infpss

Description: Every infinite set has an equinumerous proper subset, proved without AC or Infinity. Exercise 7 of TakeutiZaring p. 91. See also infpssALT . (Contributed by NM, 23-Oct-2004) (Revised by Mario Carneiro, 30-Apr-2015)

	Ref	Expression
Assertion	infpss	|- ( _om ~<_ A -> E. x ( x C. A /\ x ~~ A ) )

Proof

Step	Hyp	Ref	Expression
1		infn0	|- ( _om ~<_ A -> A =/= (/) )
2		n0	|- ( A =/= (/) <-> E. y y e. A )
3	1 2	sylib	|- ( _om ~<_ A -> E. y y e. A )
4		reldom	|- Rel ~<_
5	4	brrelex2i	|- ( _om ~<_ A -> A e. _V )
6		difexg	|- ( A e. _V -> ( A \ { y } ) e. _V )
7	5 6	syl	|- ( _om ~<_ A -> ( A \ { y } ) e. _V )
8	7	adantr	|- ( ( _om ~<_ A /\ y e. A ) -> ( A \ { y } ) e. _V )
9		simpr	|- ( ( _om ~<_ A /\ y e. A ) -> y e. A )
10		difsnpss	|- ( y e. A <-> ( A \ { y } ) C. A )
11	9 10	sylib	|- ( ( _om ~<_ A /\ y e. A ) -> ( A \ { y } ) C. A )
12		infdifsn	|- ( _om ~<_ A -> ( A \ { y } ) ~~ A )
13	12	adantr	|- ( ( _om ~<_ A /\ y e. A ) -> ( A \ { y } ) ~~ A )
14	11 13	jca	|- ( ( _om ~<_ A /\ y e. A ) -> ( ( A \ { y } ) C. A /\ ( A \ { y } ) ~~ A ) )
15		psseq1	|- ( x = ( A \ { y } ) -> ( x C. A <-> ( A \ { y } ) C. A ) )
16		breq1	|- ( x = ( A \ { y } ) -> ( x ~~ A <-> ( A \ { y } ) ~~ A ) )
17	15 16	anbi12d	|- ( x = ( A \ { y } ) -> ( ( x C. A /\ x ~~ A ) <-> ( ( A \ { y } ) C. A /\ ( A \ { y } ) ~~ A ) ) )
18	8 14 17	spcedv	|- ( ( _om ~<_ A /\ y e. A ) -> E. x ( x C. A /\ x ~~ A ) )
19	3 18	exlimddv	|- ( _om ~<_ A -> E. x ( x C. A /\ x ~~ A ) )