Metamath Proof Explorer

Theorem infpssr

Description: Dedekind infinity implies existence of a denumerable subset: take a single point witnessing the proper subset relation and iterate the embedding. (Contributed by Stefan O'Rear, 30-Oct-2014) (Revised by Mario Carneiro, 16-May-2015)

Ref Expression
Assertion infpssr ⊢ X ⊂ A ∧ X ≈ A → ω ≼ A

Proof

Step Hyp Ref Expression
1 pssnel ⊢ X ⊂ A → ∃ y y ∈ A ∧ ¬ y ∈ X
2 1 adantr ⊢ X ⊂ A ∧ X ≈ A → ∃ y y ∈ A ∧ ¬ y ∈ X
3 eldif ⊢ y ∈ A ∖ X ↔ y ∈ A ∧ ¬ y ∈ X
4 pssss ⊢ X ⊂ A → X ⊆ A
5 bren ⊢ X ≈ A ↔ ∃ f f : X ⟶ 1-1 onto A
6 simpr ⊢ y ∈ A ∖ X ∧ X ⊆ A ∧ f : X ⟶ 1-1 onto A → f : X ⟶ 1-1 onto A
7 f1ofo ⊢ f : X ⟶ 1-1 onto A → f : X ⟶ onto A
8 forn ⊢ f : X ⟶ onto A → ran ⁡ f = A
9 6 7 8 3syl ⊢ y ∈ A ∖ X ∧ X ⊆ A ∧ f : X ⟶ 1-1 onto A → ran ⁡ f = A
10 vex ⊢ f ∈ V
11 10 rnex ⊢ ran ⁡ f ∈ V
12 9 11 eqeltrrdi ⊢ y ∈ A ∖ X ∧ X ⊆ A ∧ f : X ⟶ 1-1 onto A → A ∈ V
13 simplr ⊢ y ∈ A ∖ X ∧ X ⊆ A ∧ f : X ⟶ 1-1 onto A → X ⊆ A
14 simpll ⊢ y ∈ A ∖ X ∧ X ⊆ A ∧ f : X ⟶ 1-1 onto A → y ∈ A ∖ X
15 eqid ⊢ rec ⁡ f -1 y ↾ ω = rec ⁡ f -1 y ↾ ω
16 13 6 14 15 infpssrlem5 ⊢ y ∈ A ∖ X ∧ X ⊆ A ∧ f : X ⟶ 1-1 onto A → A ∈ V → ω ≼ A
17 12 16 mpd ⊢ y ∈ A ∖ X ∧ X ⊆ A ∧ f : X ⟶ 1-1 onto A → ω ≼ A
18 17 ex ⊢ y ∈ A ∖ X ∧ X ⊆ A → f : X ⟶ 1-1 onto A → ω ≼ A
19 18 exlimdv ⊢ y ∈ A ∖ X ∧ X ⊆ A → ∃ f f : X ⟶ 1-1 onto A → ω ≼ A
20 5 19 syl5bi ⊢ y ∈ A ∖ X ∧ X ⊆ A → X ≈ A → ω ≼ A
21 20 ex ⊢ y ∈ A ∖ X → X ⊆ A → X ≈ A → ω ≼ A
22 4 21 syl5 ⊢ y ∈ A ∖ X → X ⊂ A → X ≈ A → ω ≼ A
23 22 impd ⊢ y ∈ A ∖ X → X ⊂ A ∧ X ≈ A → ω ≼ A
24 3 23 sylbir ⊢ y ∈ A ∧ ¬ y ∈ X → X ⊂ A ∧ X ≈ A → ω ≼ A
25 24 exlimiv ⊢ ∃ y y ∈ A ∧ ¬ y ∈ X → X ⊂ A ∧ X ≈ A → ω ≼ A
26 2 25 mpcom ⊢ X ⊂ A ∧ X ≈ A → ω ≼ A