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 ⊢ 𝐶 ∈ ℤ
om2uz.2 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
Assertion om2uzlt2i ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 om2uz.1 ⊢ 𝐶 ∈ ℤ
2 om2uz.2 ⊢ 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 + 1 ) ) , 𝐶 ) ↾ ω )
3 1 2 om2uzlti ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) )
4 1 2 om2uzlti ⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) → ( 𝐵 ∈ 𝐴 → ( 𝐺 ‘ 𝐵 ) < ( 𝐺 ‘ 𝐴 ) ) )
5 fveq2 ⊢ ( 𝐵 = 𝐴 → ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) )
6 5 a1i ⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) → ( 𝐵 = 𝐴 → ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) ) )
7 4 6 orim12d ⊢ ( ( 𝐵 ∈ ω ∧ 𝐴 ∈ ω ) → ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) → ( ( 𝐺 ‘ 𝐵 ) < ( 𝐺 ‘ 𝐴 ) ∨ ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) ) ) )
8 7 ancoms ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) → ( ( 𝐺 ‘ 𝐵 ) < ( 𝐺 ‘ 𝐴 ) ∨ ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) ) ) )
9 nnon ⊢ ( 𝐵 ∈ ω → 𝐵 ∈ On )
10 nnon ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
11 onsseleq ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ) )
12 ontri1 ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵 ⊆ 𝐴 ↔ ¬ 𝐴 ∈ 𝐵 ) )
13 11 12 bitr3d ⊢ ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ¬ 𝐴 ∈ 𝐵 ) )
14 9 10 13 syl2anr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 𝐵 ∈ 𝐴 ∨ 𝐵 = 𝐴 ) ↔ ¬ 𝐴 ∈ 𝐵 ) )
15 1 2 om2uzuzi ⊢ ( 𝐵 ∈ ω → ( 𝐺 ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
16 eluzelre ⊢ ( ( 𝐺 ‘ 𝐵 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ 𝐵 ) ∈ ℝ )
17 15 16 syl ⊢ ( 𝐵 ∈ ω → ( 𝐺 ‘ 𝐵 ) ∈ ℝ )
18 1 2 om2uzuzi ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) )
19 eluzelre ⊢ ( ( 𝐺 ‘ 𝐴 ) ∈ ( ℤ≥ ‘ 𝐶 ) → ( 𝐺 ‘ 𝐴 ) ∈ ℝ )
20 18 19 syl ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ 𝐴 ) ∈ ℝ )
21 leloe ⊢ ( ( ( 𝐺 ‘ 𝐵 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝐴 ) ∈ ℝ ) → ( ( 𝐺 ‘ 𝐵 ) ≤ ( 𝐺 ‘ 𝐴 ) ↔ ( ( 𝐺 ‘ 𝐵 ) < ( 𝐺 ‘ 𝐴 ) ∨ ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) ) ) )
22 lenlt ⊢ ( ( ( 𝐺 ‘ 𝐵 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝐴 ) ∈ ℝ ) → ( ( 𝐺 ‘ 𝐵 ) ≤ ( 𝐺 ‘ 𝐴 ) ↔ ¬ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) )
23 21 22 bitr3d ⊢ ( ( ( 𝐺 ‘ 𝐵 ) ∈ ℝ ∧ ( 𝐺 ‘ 𝐴 ) ∈ ℝ ) → ( ( ( 𝐺 ‘ 𝐵 ) < ( 𝐺 ‘ 𝐴 ) ∨ ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) ) ↔ ¬ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) )
24 17 20 23 syl2anr ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( ( 𝐺 ‘ 𝐵 ) < ( 𝐺 ‘ 𝐴 ) ∨ ( 𝐺 ‘ 𝐵 ) = ( 𝐺 ‘ 𝐴 ) ) ↔ ¬ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) )
25 8 14 24 3imtr3d ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ¬ 𝐴 ∈ 𝐵 → ¬ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) )
26 3 25 impcon4bid ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ( 𝐺 ‘ 𝐴 ) < ( 𝐺 ‘ 𝐵 ) ) )