Metamath Proof Explorer

Theorem om2uzlt2i

Description: The mapping G (see om2uz0i ) preserves order. (Contributed by NM, 4-May-2005) (Revised by Mario Carneiro, 13-Sep-2013)

Ref Expression
Hypotheses om2uz.1 ⊢ C ∈ ℤ
om2uz.2 ⊢ G = rec ⁡ x ∈ V ⟼ x + 1 C ↾ ω
Assertion om2uzlt2i ⊢ 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 1 2 om2uzlti ⊢ A ∈ ω ∧ B ∈ ω → A ∈ B → G ⁡ A < G ⁡ B
4 1 2 om2uzlti ⊢ B ∈ ω ∧ A ∈ ω → B ∈ A → G ⁡ B < G ⁡ A
5 fveq2 ⊢ B = A → G ⁡ B = G ⁡ A
6 5 a1i ⊢ B ∈ ω ∧ A ∈ ω → B = A → G ⁡ B = G ⁡ A
7 4 6 orim12d ⊢ B ∈ ω ∧ A ∈ ω → B ∈ A ∨ B = A → G ⁡ B < G ⁡ A ∨ G ⁡ B = G ⁡ A
8 7 ancoms ⊢ A ∈ ω ∧ B ∈ ω → B ∈ A ∨ B = A → G ⁡ B < G ⁡ A ∨ G ⁡ B = G ⁡ A
9 nnon ⊢ B ∈ ω → B ∈ On
10 nnon ⊢ A ∈ ω → A ∈ On
11 onsseleq ⊢ B ∈ On ∧ A ∈ On → B ⊆ A ↔ B ∈ A ∨ B = A
12 ontri1 ⊢ B ∈ On ∧ A ∈ On → B ⊆ A ↔ ¬ A ∈ B
13 11 12 bitr3d ⊢ B ∈ On ∧ A ∈ On → B ∈ A ∨ B = A ↔ ¬ A ∈ B
14 9 10 13 syl2anr ⊢ A ∈ ω ∧ B ∈ ω → B ∈ A ∨ B = A ↔ ¬ A ∈ B
15 1 2 om2uzuzi ⊢ B ∈ ω → G ⁡ B ∈ ℤ ≥ C
16 eluzelre ⊢ G ⁡ B ∈ ℤ ≥ C → G ⁡ B ∈ ℝ
17 15 16 syl ⊢ B ∈ ω → G ⁡ B ∈ ℝ
18 1 2 om2uzuzi ⊢ A ∈ ω → G ⁡ A ∈ ℤ ≥ C
19 eluzelre ⊢ G ⁡ A ∈ ℤ ≥ C → G ⁡ A ∈ ℝ
20 18 19 syl ⊢ A ∈ ω → G ⁡ A ∈ ℝ
21 leloe ⊢ G ⁡ B ∈ ℝ ∧ G ⁡ A ∈ ℝ → G ⁡ B ≤ G ⁡ A ↔ G ⁡ B < G ⁡ A ∨ G ⁡ B = G ⁡ A
22 lenlt ⊢ G ⁡ B ∈ ℝ ∧ G ⁡ A ∈ ℝ → G ⁡ B ≤ G ⁡ A ↔ ¬ G ⁡ A < G ⁡ B
23 21 22 bitr3d ⊢ G ⁡ B ∈ ℝ ∧ G ⁡ A ∈ ℝ → G ⁡ B < G ⁡ A ∨ G ⁡ B = G ⁡ A ↔ ¬ G ⁡ A < G ⁡ B
24 17 20 23 syl2anr ⊢ A ∈ ω ∧ B ∈ ω → G ⁡ B < G ⁡ A ∨ G ⁡ B = G ⁡ A ↔ ¬ G ⁡ A < G ⁡ B
25 8 14 24 3imtr3d ⊢ A ∈ ω ∧ B ∈ ω → ¬ A ∈ B → ¬ G ⁡ A < G ⁡ B
26 3 25 impcon4bid ⊢ A ∈ ω ∧ B ∈ ω → A ∈ B ↔ G ⁡ A < G ⁡ B