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