Metamath Proof Explorer

Theorem unbenlem

Description: Lemma for unben . (Contributed by NM, 5-May-2005) (Revised by Mario Carneiro, 15-Sep-2013)

Ref Expression
Hypothesis unbenlem.1 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
Assertion unbenlem ( ( 𝐴 ⊆ ℕ ∧ ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 ) → 𝐴 ≈ ω )

Proof

Step Hyp Ref Expression
1 unbenlem.1 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 1 ) ↾ ω )
2 nnex ⊢ ℕ ∈ V
3 2 ssex ⊢ ( 𝐴 ⊆ ℕ → 𝐴 ∈ V )
4 1z ⊢ 1 ∈ ℤ
5 4 1 om2uzf1oi ⊢ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 1 )
6 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
7 f1oeq3 ⊢ ( ℕ = ( ℤ≥ ‘ 1 ) → ( 𝐺 : ω –1-1-onto→ ℕ ↔ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 1 ) ) )
8 6 7 ax-mp ⊢ ( 𝐺 : ω –1-1-onto→ ℕ ↔ 𝐺 : ω –1-1-onto→ ( ℤ≥ ‘ 1 ) )
9 5 8 mpbir ⊢ 𝐺 : ω –1-1-onto→ ℕ
10 f1ocnv ⊢ ( 𝐺 : ω –1-1-onto→ ℕ → ◡ 𝐺 : ℕ –1-1-onto→ ω )
11 f1of1 ⊢ ( ◡ 𝐺 : ℕ –1-1-onto→ ω → ◡ 𝐺 : ℕ –1-1→ ω )
12 9 10 11 mp2b ⊢ ◡ 𝐺 : ℕ –1-1→ ω
13 f1ores ⊢ ( ( ◡ 𝐺 : ℕ –1-1→ ω ∧ 𝐴 ⊆ ℕ ) → ( ◡ 𝐺 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( ◡ 𝐺 “ 𝐴 ) )
14 12 13 mpan ⊢ ( 𝐴 ⊆ ℕ → ( ◡ 𝐺 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( ◡ 𝐺 “ 𝐴 ) )
15 f1oeng ⊢ ( ( 𝐴 ∈ V ∧ ( ◡ 𝐺 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( ◡ 𝐺 “ 𝐴 ) ) → 𝐴 ≈ ( ◡ 𝐺 “ 𝐴 ) )
16 3 14 15 syl2anc ⊢ ( 𝐴 ⊆ ℕ → 𝐴 ≈ ( ◡ 𝐺 “ 𝐴 ) )
17 16 adantr ⊢ ( ( 𝐴 ⊆ ℕ ∧ ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 ) → 𝐴 ≈ ( ◡ 𝐺 “ 𝐴 ) )
18 imassrn ⊢ ( ◡ 𝐺 “ 𝐴 ) ⊆ ran ◡ 𝐺
19 dfdm4 ⊢ dom 𝐺 = ran ◡ 𝐺
20 f1of ⊢ ( 𝐺 : ω –1-1-onto→ ℕ → 𝐺 : ω ⟶ ℕ )
21 9 20 ax-mp ⊢ 𝐺 : ω ⟶ ℕ
22 21 fdmi ⊢ dom 𝐺 = ω
23 19 22 eqtr3i ⊢ ran ◡ 𝐺 = ω
24 18 23 sseqtri ⊢ ( ◡ 𝐺 “ 𝐴 ) ⊆ ω
25 4 1 om2uzuzi ⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 1 ) )
26 25 6 eleqtrrdi ⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ 𝑦 ) ∈ ℕ )
27 breq1 ⊢ ( 𝑚 = ( 𝐺 ‘ 𝑦 ) → ( 𝑚 < 𝑛 ↔ ( 𝐺 ‘ 𝑦 ) < 𝑛 ) )
28 27 rexbidv ⊢ ( 𝑚 = ( 𝐺 ‘ 𝑦 ) → ( ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 ↔ ∃ 𝑛 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) < 𝑛 ) )
29 28 rspcv ⊢ ( ( 𝐺 ‘ 𝑦 ) ∈ ℕ → ( ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 → ∃ 𝑛 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) < 𝑛 ) )
30 26 29 syl ⊢ ( 𝑦 ∈ ω → ( ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 → ∃ 𝑛 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) < 𝑛 ) )
31 30 adantr ⊢ ( ( 𝑦 ∈ ω ∧ 𝐴 ⊆ ℕ ) → ( ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 → ∃ 𝑛 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) < 𝑛 ) )
32 f1ocnv ⊢ ( ( ◡ 𝐺 ↾ 𝐴 ) : 𝐴 –1-1-onto→ ( ◡ 𝐺 “ 𝐴 ) → ◡ ( ◡ 𝐺 ↾ 𝐴 ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 )
33 14 32 syl ⊢ ( 𝐴 ⊆ ℕ → ◡ ( ◡ 𝐺 ↾ 𝐴 ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 )
34 f1ofun ⊢ ( 𝐺 : ω –1-1-onto→ ℕ → Fun 𝐺 )
35 9 34 ax-mp ⊢ Fun 𝐺
36 funcnvres2 ⊢ ( Fun 𝐺 → ◡ ( ◡ 𝐺 ↾ 𝐴 ) = ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) )
37 f1oeq1 ⊢ ( ◡ ( ◡ 𝐺 ↾ 𝐴 ) = ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) → ( ◡ ( ◡ 𝐺 ↾ 𝐴 ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 ↔ ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 ) )
38 35 36 37 mp2b ⊢ ( ◡ ( ◡ 𝐺 ↾ 𝐴 ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 ↔ ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 )
39 33 38 sylib ⊢ ( 𝐴 ⊆ ℕ → ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 )
40 f1ofo ⊢ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 → ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) : ( ◡ 𝐺 “ 𝐴 ) –onto→ 𝐴 )
41 forn ⊢ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) : ( ◡ 𝐺 “ 𝐴 ) –onto→ 𝐴 → ran ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) = 𝐴 )
42 40 41 syl ⊢ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 → ran ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) = 𝐴 )
43 42 eleq2d ⊢ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 → ( 𝑛 ∈ ran ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ↔ 𝑛 ∈ 𝐴 ) )
44 f1ofn ⊢ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 → ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) Fn ( ◡ 𝐺 “ 𝐴 ) )
45 fvelrnb ⊢ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) Fn ( ◡ 𝐺 “ 𝐴 ) → ( 𝑛 ∈ ran ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ↔ ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 ) )
46 44 45 syl ⊢ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 → ( 𝑛 ∈ ran ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ↔ ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 ) )
47 43 46 bitr3d ⊢ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) : ( ◡ 𝐺 “ 𝐴 ) –1-1-onto→ 𝐴 → ( 𝑛 ∈ 𝐴 ↔ ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 ) )
48 39 47 syl ⊢ ( 𝐴 ⊆ ℕ → ( 𝑛 ∈ 𝐴 ↔ ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 ) )
49 48 biimpa ⊢ ( ( 𝐴 ⊆ ℕ ∧ 𝑛 ∈ 𝐴 ) → ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 )
50 fvres ⊢ ( 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) → ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = ( 𝐺 ‘ 𝑚 ) )
51 50 eqeq1d ⊢ ( 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) → ( ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 ↔ ( 𝐺 ‘ 𝑚 ) = 𝑛 ) )
52 51 biimpa ⊢ ( ( 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ∧ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 ) → ( 𝐺 ‘ 𝑚 ) = 𝑛 )
53 52 adantll ⊢ ( ( ( 𝑦 ∈ ω ∧ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ) ∧ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 ) → ( 𝐺 ‘ 𝑚 ) = 𝑛 )
54 24 sseli ⊢ ( 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) → 𝑚 ∈ ω )
55 4 1 om2uzlt2i ⊢ ( ( 𝑦 ∈ ω ∧ 𝑚 ∈ ω ) → ( 𝑦 ∈ 𝑚 ↔ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑚 ) ) )
56 54 55 sylan2 ⊢ ( ( 𝑦 ∈ ω ∧ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ) → ( 𝑦 ∈ 𝑚 ↔ ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑚 ) ) )
57 breq2 ⊢ ( ( 𝐺 ‘ 𝑚 ) = 𝑛 → ( ( 𝐺 ‘ 𝑦 ) < ( 𝐺 ‘ 𝑚 ) ↔ ( 𝐺 ‘ 𝑦 ) < 𝑛 ) )
58 56 57 sylan9bb ⊢ ( ( ( 𝑦 ∈ ω ∧ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ) ∧ ( 𝐺 ‘ 𝑚 ) = 𝑛 ) → ( 𝑦 ∈ 𝑚 ↔ ( 𝐺 ‘ 𝑦 ) < 𝑛 ) )
59 53 58 syldan ⊢ ( ( ( 𝑦 ∈ ω ∧ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ) ∧ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 ) → ( 𝑦 ∈ 𝑚 ↔ ( 𝐺 ‘ 𝑦 ) < 𝑛 ) )
60 59 biimparc ⊢ ( ( ( 𝐺 ‘ 𝑦 ) < 𝑛 ∧ ( ( 𝑦 ∈ ω ∧ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ) ∧ ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 ) ) → 𝑦 ∈ 𝑚 )
61 60 exp44 ⊢ ( ( 𝐺 ‘ 𝑦 ) < 𝑛 → ( 𝑦 ∈ ω → ( 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) → ( ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 → 𝑦 ∈ 𝑚 ) ) ) )
62 61 imp31 ⊢ ( ( ( ( 𝐺 ‘ 𝑦 ) < 𝑛 ∧ 𝑦 ∈ ω ) ∧ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ) → ( ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 → 𝑦 ∈ 𝑚 ) )
63 62 reximdva ⊢ ( ( ( 𝐺 ‘ 𝑦 ) < 𝑛 ∧ 𝑦 ∈ ω ) → ( ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) ( ( 𝐺 ↾ ( ◡ 𝐺 “ 𝐴 ) ) ‘ 𝑚 ) = 𝑛 → ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 ) )
64 49 63 syl5 ⊢ ( ( ( 𝐺 ‘ 𝑦 ) < 𝑛 ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ⊆ ℕ ∧ 𝑛 ∈ 𝐴 ) → ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 ) )
65 64 exp4b ⊢ ( ( 𝐺 ‘ 𝑦 ) < 𝑛 → ( 𝑦 ∈ ω → ( 𝐴 ⊆ ℕ → ( 𝑛 ∈ 𝐴 → ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 ) ) ) )
66 65 com4l ⊢ ( 𝑦 ∈ ω → ( 𝐴 ⊆ ℕ → ( 𝑛 ∈ 𝐴 → ( ( 𝐺 ‘ 𝑦 ) < 𝑛 → ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 ) ) ) )
67 66 imp ⊢ ( ( 𝑦 ∈ ω ∧ 𝐴 ⊆ ℕ ) → ( 𝑛 ∈ 𝐴 → ( ( 𝐺 ‘ 𝑦 ) < 𝑛 → ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 ) ) )
68 67 rexlimdv ⊢ ( ( 𝑦 ∈ ω ∧ 𝐴 ⊆ ℕ ) → ( ∃ 𝑛 ∈ 𝐴 ( 𝐺 ‘ 𝑦 ) < 𝑛 → ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 ) )
69 31 68 syld ⊢ ( ( 𝑦 ∈ ω ∧ 𝐴 ⊆ ℕ ) → ( ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 → ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 ) )
70 69 ex ⊢ ( 𝑦 ∈ ω → ( 𝐴 ⊆ ℕ → ( ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 → ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 ) ) )
71 70 com3l ⊢ ( 𝐴 ⊆ ℕ → ( ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 → ( 𝑦 ∈ ω → ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 ) ) )
72 71 imp ⊢ ( ( 𝐴 ⊆ ℕ ∧ ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 ) → ( 𝑦 ∈ ω → ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 ) )
73 72 ralrimiv ⊢ ( ( 𝐴 ⊆ ℕ ∧ ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 ) → ∀ 𝑦 ∈ ω ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 )
74 unbnn3 ⊢ ( ( ( ◡ 𝐺 “ 𝐴 ) ⊆ ω ∧ ∀ 𝑦 ∈ ω ∃ 𝑚 ∈ ( ◡ 𝐺 “ 𝐴 ) 𝑦 ∈ 𝑚 ) → ( ◡ 𝐺 “ 𝐴 ) ≈ ω )
75 24 73 74 sylancr ⊢ ( ( 𝐴 ⊆ ℕ ∧ ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 ) → ( ◡ 𝐺 “ 𝐴 ) ≈ ω )
76 entr ⊢ ( ( 𝐴 ≈ ( ◡ 𝐺 “ 𝐴 ) ∧ ( ◡ 𝐺 “ 𝐴 ) ≈ ω ) → 𝐴 ≈ ω )
77 17 75 76 syl2anc ⊢ ( ( 𝐴 ⊆ ℕ ∧ ∀ 𝑚 ∈ ℕ ∃ 𝑛 ∈ 𝐴 𝑚 < 𝑛 ) → 𝐴 ≈ ω )