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 syl5ib ( ( 𝐴 ∈ ω ∧ 𝑦 ∈ ω ) → ( ( 𝐴𝑦 → ( 𝐺𝐴 ) < ( 𝐺𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐺𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) )
52 51 expcom ( 𝑦 ∈ ω → ( 𝐴 ∈ ω → ( ( 𝐴𝑦 → ( 𝐺𝐴 ) < ( 𝐺𝑦 ) ) → ( 𝐴 ∈ suc 𝑦 → ( 𝐺𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) ) )
53 52 a2d ( 𝑦 ∈ ω → ( ( 𝐴 ∈ ω → ( 𝐴𝑦 → ( 𝐺𝐴 ) < ( 𝐺𝑦 ) ) ) → ( 𝐴 ∈ ω → ( 𝐴 ∈ suc 𝑦 → ( 𝐺𝐴 ) < ( 𝐺 ‘ suc 𝑦 ) ) ) ) )
54 7 12 17 22 25 53 finds ( 𝐵 ∈ ω → ( 𝐴 ∈ ω → ( 𝐴𝐵 → ( 𝐺𝐴 ) < ( 𝐺𝐵 ) ) ) )
55 54 impcom ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴𝐵 → ( 𝐺𝐴 ) < ( 𝐺𝐵 ) ) )