Theorem uzenom

Description: An upper integer set is denumerable. (Contributed by Mario Carneiro, 15-Oct-2015)

	Ref	Expression
Hypothesis	uzinf.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
Assertion	uzenom	⊢ ( 𝑀 ∈ ℤ → 𝑍 ≈ ω )

Proof

Step	Hyp	Ref	Expression
1		uzinf.1	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2		fveq2	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( ℤ≥ ‘ 𝑀 ) = ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
3	1 2	eqtrid	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → 𝑍 = ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
4	3	breq1d	⊢ ( 𝑀 = if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) → ( 𝑍 ≈ ω ↔ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ≈ ω ) )
5		omex	⊢ ω ∈ V
6		fvex	⊢ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ∈ V
7		0z	⊢ 0 ∈ ℤ
8	7	elimel	⊢ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ∈ ℤ
9		eqid	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω ) = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω )
10	8 9	om2uzf1oi	⊢ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω ) : ω –1-1-onto→ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) )
11		f1oen2g	⊢ ( ( ω ∈ V ∧ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ∈ V ∧ ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ↾ ω ) : ω –1-1-onto→ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ) → ω ≈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) )
12	5 6 10 11	mp3an	⊢ ω ≈ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) )
13	12	ensymi	⊢ ( ℤ≥ ‘ if ( 𝑀 ∈ ℤ , 𝑀 , 0 ) ) ≈ ω
14	4 13	dedth	⊢ ( 𝑀 ∈ ℤ → 𝑍 ≈ ω )