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 ( ( 𝑋𝐴𝑋𝐴 ) → ω ≼ 𝐴 )

Proof

Step Hyp Ref Expression
1 pssnel ( 𝑋𝐴 → ∃ 𝑦 ( 𝑦𝐴 ∧ ¬ 𝑦𝑋 ) )
2 1 adantr ( ( 𝑋𝐴𝑋𝐴 ) → ∃ 𝑦 ( 𝑦𝐴 ∧ ¬ 𝑦𝑋 ) )
3 eldif ( 𝑦 ∈ ( 𝐴𝑋 ) ↔ ( 𝑦𝐴 ∧ ¬ 𝑦𝑋 ) )
4 pssss ( 𝑋𝐴𝑋𝐴 )
5 bren ( 𝑋𝐴 ↔ ∃ 𝑓 𝑓 : 𝑋1-1-onto𝐴 )
6 simpr ( ( ( 𝑦 ∈ ( 𝐴𝑋 ) ∧ 𝑋𝐴 ) ∧ 𝑓 : 𝑋1-1-onto𝐴 ) → 𝑓 : 𝑋1-1-onto𝐴 )
7 f1ofo ( 𝑓 : 𝑋1-1-onto𝐴𝑓 : 𝑋onto𝐴 )
8 forn ( 𝑓 : 𝑋onto𝐴 → ran 𝑓 = 𝐴 )
9 6 7 8 3syl ( ( ( 𝑦 ∈ ( 𝐴𝑋 ) ∧ 𝑋𝐴 ) ∧ 𝑓 : 𝑋1-1-onto𝐴 ) → ran 𝑓 = 𝐴 )
10 vex 𝑓 ∈ V
11 10 rnex ran 𝑓 ∈ V
12 9 11 eqeltrrdi ( ( ( 𝑦 ∈ ( 𝐴𝑋 ) ∧ 𝑋𝐴 ) ∧ 𝑓 : 𝑋1-1-onto𝐴 ) → 𝐴 ∈ V )
13 simplr ( ( ( 𝑦 ∈ ( 𝐴𝑋 ) ∧ 𝑋𝐴 ) ∧ 𝑓 : 𝑋1-1-onto𝐴 ) → 𝑋𝐴 )
14 simpll ( ( ( 𝑦 ∈ ( 𝐴𝑋 ) ∧ 𝑋𝐴 ) ∧ 𝑓 : 𝑋1-1-onto𝐴 ) → 𝑦 ∈ ( 𝐴𝑋 ) )
15 eqid ( rec ( 𝑓 , 𝑦 ) ↾ ω ) = ( rec ( 𝑓 , 𝑦 ) ↾ ω )
16 13 6 14 15 infpssrlem5 ( ( ( 𝑦 ∈ ( 𝐴𝑋 ) ∧ 𝑋𝐴 ) ∧ 𝑓 : 𝑋1-1-onto𝐴 ) → ( 𝐴 ∈ V → ω ≼ 𝐴 ) )
17 12 16 mpd ( ( ( 𝑦 ∈ ( 𝐴𝑋 ) ∧ 𝑋𝐴 ) ∧ 𝑓 : 𝑋1-1-onto𝐴 ) → ω ≼ 𝐴 )
18 17 ex ( ( 𝑦 ∈ ( 𝐴𝑋 ) ∧ 𝑋𝐴 ) → ( 𝑓 : 𝑋1-1-onto𝐴 → ω ≼ 𝐴 ) )
19 18 exlimdv ( ( 𝑦 ∈ ( 𝐴𝑋 ) ∧ 𝑋𝐴 ) → ( ∃ 𝑓 𝑓 : 𝑋1-1-onto𝐴 → ω ≼ 𝐴 ) )
20 5 19 syl5bi ( ( 𝑦 ∈ ( 𝐴𝑋 ) ∧ 𝑋𝐴 ) → ( 𝑋𝐴 → ω ≼ 𝐴 ) )
21 20 ex ( 𝑦 ∈ ( 𝐴𝑋 ) → ( 𝑋𝐴 → ( 𝑋𝐴 → ω ≼ 𝐴 ) ) )
22 4 21 syl5 ( 𝑦 ∈ ( 𝐴𝑋 ) → ( 𝑋𝐴 → ( 𝑋𝐴 → ω ≼ 𝐴 ) ) )
23 22 impd ( 𝑦 ∈ ( 𝐴𝑋 ) → ( ( 𝑋𝐴𝑋𝐴 ) → ω ≼ 𝐴 ) )
24 3 23 sylbir ( ( 𝑦𝐴 ∧ ¬ 𝑦𝑋 ) → ( ( 𝑋𝐴𝑋𝐴 ) → ω ≼ 𝐴 ) )
25 24 exlimiv ( ∃ 𝑦 ( 𝑦𝐴 ∧ ¬ 𝑦𝑋 ) → ( ( 𝑋𝐴𝑋𝐴 ) → ω ≼ 𝐴 ) )
26 2 25 mpcom ( ( 𝑋𝐴𝑋𝐴 ) → ω ≼ 𝐴 )