This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 biimtrid ⊢ ( ( 𝑦 ∈ ( 𝐴 ∖ 𝑋 ) ∧ 𝑋 ⊆ 𝐴 ) → ( 𝑋 ≈ 𝐴 → ω ≼ 𝐴 ) )
21 20 ex ⊢ ( 𝑦 ∈ ( 𝐴 ∖ 𝑋 ) → ( 𝑋 ⊆ 𝐴 → ( 𝑋 ≈ 𝐴 → ω ≼ 𝐴 ) ) )
22 4 21 syl5 ⊢ ( 𝑦 ∈ ( 𝐴 ∖ 𝑋 ) → ( 𝑋 ⊊ 𝐴 → ( 𝑋 ≈ 𝐴 → ω ≼ 𝐴 ) ) )
23 22 impd ⊢ ( 𝑦 ∈ ( 𝐴 ∖ 𝑋 ) → ( ( 𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴 ) → ω ≼ 𝐴 ) )
24 3 23 sylbir ⊢ ( ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝑋 ) → ( ( 𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴 ) → ω ≼ 𝐴 ) )
25 24 exlimiv ⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ ¬ 𝑦 ∈ 𝑋 ) → ( ( 𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴 ) → ω ≼ 𝐴 ) )
26 2 25 mpcom ⊢ ( ( 𝑋 ⊊ 𝐴 ∧ 𝑋 ≈ 𝐴 ) → ω ≼ 𝐴 )