Metamath Proof Explorer

Theorem om2uzlti

Description: Less-than relation for G (see om2uz0i ). (Contributed by NM, 3-Oct-2004) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Hypotheses om2uz.1 ⊢ 𝐶 ∈ ℤ
om2uz.2 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
Assertion om2uzlti ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 om2uz.1 ⊢ 𝐶 ∈ ℤ
2 om2uz.2 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3 eleq2 ⊢ ( 𝑧 = ∅ → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ ∅ ) )
4 fveq2 ⊢ ( 𝑧 = ∅ → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ ∅ ) )
5 4 breq2d ⊢ ( 𝑧 = ∅ → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ ∅ ) ) )
6 3 5 imbi12d ⊢ ( 𝑧 = ∅ → ( ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ↔ ( 𝐴 ∈ ∅ → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ ∅ ) ) ) )
7 6 imbi2d ⊢ ( 𝑧 = ∅ → ( ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐴 ∈ ∅ → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ ∅ ) ) ) ) )
8 eleq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝑦 ) )
9 fveq2 ⊢ ( 𝑧 = 𝑦 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝑦 ) )
10 9 breq2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) )
11 8 10 imbi12d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ↔ ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) ) )
12 11 imbi2d ⊢ ( 𝑧 = 𝑦 → ( ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) ) ) )
13 eleq2 ⊢ ( 𝑧 = suc 𝑦 → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ suc 𝑦 ) )
14 fveq2 ⊢ ( 𝑧 = suc 𝑦 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ suc 𝑦 ) )
15 14 breq2d ⊢ ( 𝑧 = suc 𝑦 → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) )
16 13 15 imbi12d ⊢ ( 𝑧 = suc 𝑦 → ( ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ↔ ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) )
17 16 imbi2d ⊢ ( 𝑧 = suc 𝑦 → ( ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) ) )
18 eleq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐴 ∈ 𝑧 ↔ 𝐴 ∈ 𝐵 ) )
19 fveq2 ⊢ ( 𝑧 = 𝐵 → ( 𝐺 ‘ 𝑧 ) = ( 𝐺 ‘ 𝐵 ) )
20 19 breq2d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) )
21 18 20 imbi12d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ↔ ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) ) )
22 21 imbi2d ⊢ ( 𝑧 = 𝐵 → ( ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑧 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑧 ) ) ) ↔ ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) ) ) )
23 noel ⊢ ¬ 𝐴 ∈ ∅
24 23 pm2.21i ⊢ ( 𝐴 ∈ ∅ → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ ∅ ) )
25 24 a1i ⊢ ( 𝐴 ∈ ω → ( 𝐴 ∈ ∅ → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ ∅ ) ) )
26 id ⊢ ( ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) → ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) )
27 fveq2 ⊢ ( 𝐴 = 𝑦 → ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) )
28 27 a1i ⊢ ( ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) → ( 𝐴 = 𝑦 → ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) )
29 26 28 orim12d ⊢ ( ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ∨ ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) ) )
30 elsuc2g ⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ suc 𝑦 ↔ ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) ) )
31 30 bicomd ⊢ ( 𝑦 ∈ ω → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) ↔ 𝐴 ∈ suc 𝑦 ) )
32 31 adantl ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) ↔ 𝐴 ∈ suc 𝑦 ) )
33 1 2 om2uzsuci ⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ suc 𝑦 ) = ( ( 𝐺 ‘ 𝑦 ) + 1 ) )
34 33 breq2d ⊢ ( 𝑦 ∈ ω → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( ( 𝐺 ‘ 𝑦 ) + 1 ) ) )
35 34 adantl ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( ( 𝐺 ‘ 𝑦 ) + 1 ) ) )
36 1 2 om2uzuzi ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
37 1 2 om2uzuzi ⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
38 eluzelz ⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ 𝐴 ) ∈ ℤ )
39 eluzelz ⊢ ( ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ 𝑦 ) ∈ ℤ )
40 zleltp1 ⊢ ( ( ( 𝐺 ‘ 𝐴 ) ∈ ℤ ∧ ( 𝐺 ‘ 𝑦 ) ∈ ℤ ) → ( ( 𝐺 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( ( 𝐺 ‘ 𝑦 ) + 1 ) ) )
41 38 39 40 syl2an ⊢ ( ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) ∧ ( 𝐺 ‘ 𝑦 ) ∈ ( ℤ≥ ‘ 𝐶 ) ) → ( ( 𝐺 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( ( 𝐺 ‘ 𝑦 ) + 1 ) ) )
42 36 37 41 syl2an ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( 𝐺 ‘ 𝐴 ) < ( ( 𝐺 ‘ 𝑦 ) + 1 ) ) )
43 36 38 syl ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ℤ )
44 43 zred ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ℝ )
45 37 39 syl ⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ 𝑦 ) ∈ ℤ )
46 45 zred ⊢ ( 𝑦 ∈ ω → ( 𝐺 ‘ 𝑦 ) ∈ ℝ )
47 leloe ⊢ ( ( ( 𝐺 ‘ 𝐴 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝑦 ) ∈ ℝ ) → ( ( 𝐺 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ∨ ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) ) )
48 44 46 47 syl2an ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) ≤ ( 𝐺 ‘ 𝑦 ) ↔ ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ∨ ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) ) )
49 35 42 48 3bitr2rd ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ∨ ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) )
50 32 49 imbi12d ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( ( 𝐴 ∈ 𝑦 ∨ 𝐴 = 𝑦 ) → ( ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ∨ ( 𝐺 ‘ 𝐴 ) = ( 𝐺 ‘ 𝑦 ) ) ) ↔ ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) )
51 29 50 imbitrid ⊢ ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) )
52 51 expcom ⊢ ( 𝑦 ∈ ω → ( 𝐴 ∈ ω → ( ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) ) )
53 52 a2d ⊢ ( 𝑦 ∈ ω → ( ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝑦 ) ) ) → ( 𝐴 ∈ ω → ( 𝐴 ∈ suc 𝑦 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) ) )
54 7 12 17 22 25 53 finds ⊢ ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) ) )
55 54 impcom ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) )