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

Proof

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