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+1C↾ω
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+1C↾ω
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