This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 5 difexd 
 |-  ( _om ~<_ A -> ( A \ { y } ) e. _V )
7 6 adantr 
 |-  ( ( _om ~<_ A /\ y e. A ) -> ( A \ { y } ) e. _V )
8 simpr 
 |-  ( ( _om ~<_ A /\ y e. A ) -> y e. A )
9 difsnpss 
 |-  ( y e. A <-> ( A \ { y } ) C. A )
10 8 9 sylib 
 |-  ( ( _om ~<_ A /\ y e. A ) -> ( A \ { y } ) C. A )
11 infdifsn 
 |-  ( _om ~<_ A -> ( A \ { y } ) ~~ A )
12 11 adantr 
 |-  ( ( _om ~<_ A /\ y e. A ) -> ( A \ { y } ) ~~ A )
13 10 12 jca 
 |-  ( ( _om ~<_ A /\ y e. A ) -> ( ( A \ { y } ) C. A /\ ( A \ { y } ) ~~ A ) )
14 psseq1 
 |-  ( x = ( A \ { y } ) -> ( x C. A <-> ( A \ { y } ) C. A ) )
15 breq1 
 |-  ( x = ( A \ { y } ) -> ( x ~~ A <-> ( A \ { y } ) ~~ A ) )
16 14 15 anbi12d 
 |-  ( x = ( A \ { y } ) -> ( ( x C. A /\ x ~~ A ) <-> ( ( A \ { y } ) C. A /\ ( A \ { y } ) ~~ A ) ) )
17 7 13 16 spcedv 
 |-  ( ( _om ~<_ A /\ y e. A ) -> E. x ( x C. A /\ x ~~ A ) )
18 3 17 exlimddv 
 |-  ( _om ~<_ A -> E. x ( x C. A /\ x ~~ A ) )