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 ⊢ ω ≼ A → ∃ x x ⊂ A ∧ x ≈ A

Proof

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