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 ⊢ C ∈ ℤ
om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
Assertion om2uzlti ⊢ A ∈ ω ∧ B ∈ ω → A ∈ B → G ⁡ A < G ⁡ B

Proof

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