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	⊢ ( ω ≼ 𝐴 → ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		infn0	⊢ ( ω ≼ 𝐴 → 𝐴 ≠ ∅ )
2		n0	⊢ ( 𝐴 ≠ ∅ ↔ ∃ 𝑦 𝑦 ∈ 𝐴 )
3	1 2	sylib	⊢ ( ω ≼ 𝐴 → ∃ 𝑦 𝑦 ∈ 𝐴 )
4		reldom	⊢ Rel ≼
5	4	brrelex2i	⊢ ( ω ≼ 𝐴 → 𝐴 ∈ V )
6		difexg	⊢ ( 𝐴 ∈ V → ( 𝐴 ∖ { 𝑦 } ) ∈ V )
7	5 6	syl	⊢ ( ω ≼ 𝐴 → ( 𝐴 ∖ { 𝑦 } ) ∈ V )
8	7	adantr	⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ∈ V )
9		simpr	⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → 𝑦 ∈ 𝐴 )
10		difsnpss	⊢ ( 𝑦 ∈ 𝐴 ↔ ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 )
11	9 10	sylib	⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 )
12		infdifsn	⊢ ( ω ≼ 𝐴 → ( 𝐴 ∖ { 𝑦 } ) ≈ 𝐴 )
13	12	adantr	⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑦 } ) ≈ 𝐴 )
14	11 13	jca	⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 ∧ ( 𝐴 ∖ { 𝑦 } ) ≈ 𝐴 ) )
15		psseq1	⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( 𝑥 ⊊ 𝐴 ↔ ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 ) )
16		breq1	⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( 𝑥 ≈ 𝐴 ↔ ( 𝐴 ∖ { 𝑦 } ) ≈ 𝐴 ) )
17	15 16	anbi12d	⊢ ( 𝑥 = ( 𝐴 ∖ { 𝑦 } ) → ( ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) ↔ ( ( 𝐴 ∖ { 𝑦 } ) ⊊ 𝐴 ∧ ( 𝐴 ∖ { 𝑦 } ) ≈ 𝐴 ) ) )
18	8 14 17	spcedv	⊢ ( ( ω ≼ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) )
19	3 18	exlimddv	⊢ ( ω ≼ 𝐴 → ∃ 𝑥 ( 𝑥 ⊊ 𝐴 ∧ 𝑥 ≈ 𝐴 ) )