Metamath Proof Explorer

Theorem isercolllem1

Description: Lemma for isercoll . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses isercoll.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
isercoll.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
isercoll.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ 𝑍 )
isercoll.i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
Assertion isercolllem1 ( ( 𝜑 ∧ 𝑆 ⊆ ℕ ) → ( 𝐺 ↾ 𝑆 ) Isom < , < ( 𝑆 , ( 𝐺 “ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 isercoll.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 isercoll.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 isercoll.g ⊢ ( 𝜑 → 𝐺 : ℕ ⟶ 𝑍 )
4 isercoll.i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
5 uzssz ⊢ ( ℤ≥ ‘ 𝑀 ) ⊆ ℤ
6 1 5 eqsstri ⊢ 𝑍 ⊆ ℤ
7 zssre ⊢ ℤ ⊆ ℝ
8 6 7 sstri ⊢ 𝑍 ⊆ ℝ
9 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → 𝐺 : ℕ ⟶ 𝑍 )
10 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℕ )
11 9 10 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑍 )
12 8 11 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐺 ‘ 𝑥 ) ∈ ℝ )
13 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℕ )
14 13 nnred ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℝ )
15 12 14 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐺 ‘ 𝑥 ) − 𝑦 ) ∈ ℝ )
16 10 nnred ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℝ )
17 12 16 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐺 ‘ 𝑥 ) − 𝑥 ) ∈ ℝ )
18 9 13 ffvelrnd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐺 ‘ 𝑦 ) ∈ 𝑍 )
19 8 18 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐺 ‘ 𝑦 ) ∈ ℝ )
20 19 14 resubcld ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐺 ‘ 𝑦 ) − 𝑦 ) ∈ ℝ )
21 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 < 𝑦 )
22 16 14 12 21 ltsub2dd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐺 ‘ 𝑥 ) − 𝑦 ) < ( ( 𝐺 ‘ 𝑥 ) − 𝑥 ) )
23 10 nnzd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ∈ ℤ )
24 13 nnzd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ℤ )
25 16 14 21 ltled ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → 𝑥 ≤ 𝑦 )
26 eluz2 ⊢ ( 𝑦 ∈ ( ℤ≥ ‘ 𝑥 ) ↔ ( 𝑥 ∈ ℤ ∧ 𝑦 ∈ ℤ ∧ 𝑥 ≤ 𝑦 ) )
27 23 24 25 26 syl3anbrc ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → 𝑦 ∈ ( ℤ≥ ‘ 𝑥 ) )
28 elfzuz ⊢ ( 𝑘 ∈ ( 𝑥 ... 𝑦 ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑥 ) )
29 eluznn ⊢ ( ( 𝑥 ∈ ℕ ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑥 ) ) → 𝑘 ∈ ℕ )
30 10 29 sylan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑥 ) ) → 𝑘 ∈ ℕ )
31 fveq2 ⊢ ( 𝑛 = 𝑘 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑘 ) )
32 id ⊢ ( 𝑛 = 𝑘 → 𝑛 = 𝑘 )
33 31 32 oveq12d ⊢ ( 𝑛 = 𝑘 → ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) = ( ( 𝐺 ‘ 𝑘 ) − 𝑘 ) )
34 eqid ⊢ ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) = ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) )
35 ovex ⊢ ( ( 𝐺 ‘ 𝑘 ) − 𝑘 ) ∈ V
36 33 34 35 fvmpt ⊢ ( 𝑘 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) − 𝑘 ) )
37 36 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑘 ) = ( ( 𝐺 ‘ 𝑘 ) − 𝑘 ) )
38 9 ffvelrnda ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ 𝑍 )
39 8 38 sselid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℝ )
40 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
41 40 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℝ )
42 39 41 resubcld ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑘 ) − 𝑘 ) ∈ ℝ )
43 37 42 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑘 ) ∈ ℝ )
44 30 43 syldan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑥 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑘 ) ∈ ℝ )
45 28 44 sylan2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ( 𝑥 ... 𝑦 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑘 ) ∈ ℝ )
46 elfzuz ⊢ ( 𝑘 ∈ ( 𝑥 ... ( 𝑦 − 1 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑥 ) )
47 peano2nn ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 + 1 ) ∈ ℕ )
48 ffvelrn ⊢ ( ( 𝐺 : ℕ ⟶ 𝑍 ∧ ( 𝑘 + 1 ) ∈ ℕ ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ 𝑍 )
49 9 47 48 syl2an ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ 𝑍 )
50 8 49 sselid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ ℝ )
51 peano2rem ⊢ ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ ℝ → ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − 1 ) ∈ ℝ )
52 50 51 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − 1 ) ∈ ℝ )
53 4 ad4ant14 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
54 6 38 sselid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ∈ ℤ )
55 6 49 sselid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ ℤ )
56 zltlem1 ⊢ ( ( ( 𝐺 ‘ 𝑘 ) ∈ ℤ ∧ ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ ℤ ) → ( ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝐺 ‘ 𝑘 ) ≤ ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − 1 ) ) )
57 54 55 56 syl2anc ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑘 ) < ( 𝐺 ‘ ( 𝑘 + 1 ) ) ↔ ( 𝐺 ‘ 𝑘 ) ≤ ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − 1 ) ) )
58 53 57 mpbid ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ 𝑘 ) ≤ ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − 1 ) )
59 39 52 41 58 lesub1dd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑘 ) − 𝑘 ) ≤ ( ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − 1 ) − 𝑘 ) )
60 50 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( 𝐺 ‘ ( 𝑘 + 1 ) ) ∈ ℂ )
61 1cnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → 1 ∈ ℂ )
62 41 recnd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → 𝑘 ∈ ℂ )
63 60 61 62 sub32d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − 1 ) − 𝑘 ) = ( ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − 𝑘 ) − 1 ) )
64 60 62 61 subsub4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − 𝑘 ) − 1 ) = ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − ( 𝑘 + 1 ) ) )
65 63 64 eqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − 1 ) − 𝑘 ) = ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − ( 𝑘 + 1 ) ) )
66 59 65 breqtrd ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝐺 ‘ 𝑘 ) − 𝑘 ) ≤ ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − ( 𝑘 + 1 ) ) )
67 47 adantl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( 𝑘 + 1 ) ∈ ℕ )
68 fveq2 ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ ( 𝑘 + 1 ) ) )
69 id ⊢ ( 𝑛 = ( 𝑘 + 1 ) → 𝑛 = ( 𝑘 + 1 ) )
70 68 69 oveq12d ⊢ ( 𝑛 = ( 𝑘 + 1 ) → ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) = ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − ( 𝑘 + 1 ) ) )
71 ovex ⊢ ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − ( 𝑘 + 1 ) ) ∈ V
72 70 34 71 fvmpt ⊢ ( ( 𝑘 + 1 ) ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − ( 𝑘 + 1 ) ) )
73 67 72 syl ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ ( 𝑘 + 1 ) ) = ( ( 𝐺 ‘ ( 𝑘 + 1 ) ) − ( 𝑘 + 1 ) ) )
74 66 37 73 3brtr4d ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ℕ ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ ( 𝑘 + 1 ) ) )
75 30 74 syldan ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ( ℤ≥ ‘ 𝑥 ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ ( 𝑘 + 1 ) ) )
76 46 75 sylan2 ⊢ ( ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) ∧ 𝑘 ∈ ( 𝑥 ... ( 𝑦 − 1 ) ) ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑘 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ ( 𝑘 + 1 ) ) )
77 27 45 76 monoord ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑥 ) ≤ ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑦 ) )
78 fveq2 ⊢ ( 𝑛 = 𝑥 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑥 ) )
79 id ⊢ ( 𝑛 = 𝑥 → 𝑛 = 𝑥 )
80 78 79 oveq12d ⊢ ( 𝑛 = 𝑥 → ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) = ( ( 𝐺 ‘ 𝑥 ) − 𝑥 ) )
81 ovex ⊢ ( ( 𝐺 ‘ 𝑥 ) − 𝑥 ) ∈ V
82 80 34 81 fvmpt ⊢ ( 𝑥 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) − 𝑥 ) )
83 10 82 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑥 ) = ( ( 𝐺 ‘ 𝑥 ) − 𝑥 ) )
84 fveq2 ⊢ ( 𝑛 = 𝑦 → ( 𝐺 ‘ 𝑛 ) = ( 𝐺 ‘ 𝑦 ) )
85 id ⊢ ( 𝑛 = 𝑦 → 𝑛 = 𝑦 )
86 84 85 oveq12d ⊢ ( 𝑛 = 𝑦 → ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) = ( ( 𝐺 ‘ 𝑦 ) − 𝑦 ) )
87 ovex ⊢ ( ( 𝐺 ‘ 𝑦 ) − 𝑦 ) ∈ V
88 86 34 87 fvmpt ⊢ ( 𝑦 ∈ ℕ → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ 𝑦 ) − 𝑦 ) )
89 13 88 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝑛 ∈ ℕ ↦ ( ( 𝐺 ‘ 𝑛 ) − 𝑛 ) ) ‘ 𝑦 ) = ( ( 𝐺 ‘ 𝑦 ) − 𝑦 ) )
90 77 83 89 3brtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐺 ‘ 𝑥 ) − 𝑥 ) ≤ ( ( 𝐺 ‘ 𝑦 ) − 𝑦 ) )
91 15 17 20 22 90 ltletrd ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐺 ‘ 𝑥 ) − 𝑦 ) < ( ( 𝐺 ‘ 𝑦 ) − 𝑦 ) )
92 12 19 14 ltsub1d ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( ( 𝐺 ‘ 𝑥 ) < ( 𝐺 ‘ 𝑦 ) ↔ ( ( 𝐺 ‘ 𝑥 ) − 𝑦 ) < ( ( 𝐺 ‘ 𝑦 ) − 𝑦 ) ) )
93 91 92 mpbird ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) ∧ 𝑥 < 𝑦 ) → ( 𝐺 ‘ 𝑥 ) < ( 𝐺 ‘ 𝑦 ) )
94 93 ex ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ℕ ∧ 𝑦 ∈ ℕ ) ) → ( 𝑥 < 𝑦 → ( 𝐺 ‘ 𝑥 ) < ( 𝐺 ‘ 𝑦 ) ) )
95 94 ralrimivva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ℕ ∀ 𝑦 ∈ ℕ ( 𝑥 < 𝑦 → ( 𝐺 ‘ 𝑥 ) < ( 𝐺 ‘ 𝑦 ) ) )
96 ss2ralv ⊢ ( 𝑆 ⊆ ℕ → ( ∀ 𝑥 ∈ ℕ ∀ 𝑦 ∈ ℕ ( 𝑥 < 𝑦 → ( 𝐺 ‘ 𝑥 ) < ( 𝐺 ‘ 𝑦 ) ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 < 𝑦 → ( 𝐺 ‘ 𝑥 ) < ( 𝐺 ‘ 𝑦 ) ) ) )
97 95 96 mpan9 ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ ℕ ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 < 𝑦 → ( 𝐺 ‘ 𝑥 ) < ( 𝐺 ‘ 𝑦 ) ) )
98 nnssre ⊢ ℕ ⊆ ℝ
99 ltso ⊢ < Or ℝ
100 soss ⊢ ( ℕ ⊆ ℝ → ( < Or ℝ → < Or ℕ ) )
101 98 99 100 mp2 ⊢ < Or ℕ
102 101 a1i ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ ℕ ) → < Or ℕ )
103 soss ⊢ ( 𝑍 ⊆ ℝ → ( < Or ℝ → < Or 𝑍 ) )
104 8 99 103 mp2 ⊢ < Or 𝑍
105 104 a1i ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ ℕ ) → < Or 𝑍 )
106 3 adantr ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ ℕ ) → 𝐺 : ℕ ⟶ 𝑍 )
107 simpr ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ ℕ ) → 𝑆 ⊆ ℕ )
108 soisores ⊢ ( ( ( < Or ℕ ∧ < Or 𝑍 ) ∧ ( 𝐺 : ℕ ⟶ 𝑍 ∧ 𝑆 ⊆ ℕ ) ) → ( ( 𝐺 ↾ 𝑆 ) Isom < , < ( 𝑆 , ( 𝐺 “ 𝑆 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 < 𝑦 → ( 𝐺 ‘ 𝑥 ) < ( 𝐺 ‘ 𝑦 ) ) ) )
109 102 105 106 107 108 syl22anc ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ ℕ ) → ( ( 𝐺 ↾ 𝑆 ) Isom < , < ( 𝑆 , ( 𝐺 “ 𝑆 ) ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 < 𝑦 → ( 𝐺 ‘ 𝑥 ) < ( 𝐺 ‘ 𝑦 ) ) ) )
110 97 109 mpbird ⊢ ( ( 𝜑 ∧ 𝑆 ⊆ ℕ ) → ( 𝐺 ↾ 𝑆 ) Isom < , < ( 𝑆 , ( 𝐺 “ 𝑆 ) ) )