Metamath Proof Explorer

Theorem om2noseqlt

Description: Surreal less-than relation for G . (Contributed by Scott Fenton, 18-Apr-2025)

Ref Expression
Hypotheses om2noseq.1 ⊢ ( 𝜑 → 𝐶 ∈ No )
om2noseq.2 ⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
om2noseq.3 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
Assertion om2noseqlt ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 om2noseq.1 ⊢ ( 𝜑 → 𝐶 ∈ No )
2 om2noseq.2 ⊢ ( 𝜑 → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
3 om2noseq.3 ⊢ ( 𝜑 → 𝑍 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) “ ω ) )
4 nnaordex2 ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑦 ∈ ω ( 𝐴 +o suc 𝑦 ) = 𝐵 ) )
5 4 adantl ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴 ∈ 𝐵 ↔ ∃ 𝑦 ∈ ω ( 𝐴 +o suc 𝑦 ) = 𝐵 ) )
6 suceq ⊢ ( 𝑦 = ∅ → suc 𝑦 = suc ∅ )
7 df-1o ⊢ 1o = suc ∅
8 6 7 eqtr4di ⊢ ( 𝑦 = ∅ → suc 𝑦 = 1o )
9 8 oveq2d ⊢ ( 𝑦 = ∅ → ( 𝐴 +o suc 𝑦 ) = ( 𝐴 +o 1o ) )
10 9 fveq2d ⊢ ( 𝑦 = ∅ → ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) = ( 𝐺 ‘ ( 𝐴 +o 1o ) ) )
11 10 breq2d ⊢ ( 𝑦 = ∅ → ( ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) ↔ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o 1o ) ) ) )
12 suceq ⊢ ( 𝑦 = 𝑧 → suc 𝑦 = suc 𝑧 )
13 12 oveq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐴 +o suc 𝑦 ) = ( 𝐴 +o suc 𝑧 ) )
14 13 fveq2d ⊢ ( 𝑦 = 𝑧 → ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) = ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) )
15 14 breq2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) ↔ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) )
16 suceq ⊢ ( 𝑦 = suc 𝑧 → suc 𝑦 = suc suc 𝑧 )
17 16 oveq2d ⊢ ( 𝑦 = suc 𝑧 → ( 𝐴 +o suc 𝑦 ) = ( 𝐴 +o suc suc 𝑧 ) )
18 17 fveq2d ⊢ ( 𝑦 = suc 𝑧 → ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) = ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) )
19 18 breq2d ⊢ ( 𝑦 = suc 𝑧 → ( ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) ↔ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) ) )
20 1 2 3 om2noseqfo ⊢ ( 𝜑 → 𝐺 : ω –onto→ 𝑍 )
21 fof ⊢ ( 𝐺 : ω –onto→ 𝑍 → 𝐺 : ω ⟶ 𝑍 )
22 20 21 syl ⊢ ( 𝜑 → 𝐺 : ω ⟶ 𝑍 )
23 3 1 noseqssno ⊢ ( 𝜑 → 𝑍 ⊆ No )
24 22 23 fssd ⊢ ( 𝜑 → 𝐺 : ω ⟶ No )
25 24 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ 𝐴 ) ∈ No )
26 25 addsridd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) +s 0s ) = ( 𝐺 ‘ 𝐴 ) )
27 0slt1s ⊢ 0s <s 1s
28 0sno ⊢ 0s ∈ No
29 28 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → 0s ∈ No )
30 1sno ⊢ 1s ∈ No
31 30 a1i ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → 1s ∈ No )
32 29 31 25 sltadd2d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 0s <s 1s ↔ ( ( 𝐺 ‘ 𝐴 ) +s 0s ) <s ( ( 𝐺 ‘ 𝐴 ) +s 1s ) ) )
33 27 32 mpbii ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) +s 0s ) <s ( ( 𝐺 ‘ 𝐴 ) +s 1s ) )
34 26 33 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ 𝐴 ) <s ( ( 𝐺 ‘ 𝐴 ) +s 1s ) )
35 nnon ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
36 oa1suc ⊢ ( 𝐴 ∈ On → ( 𝐴 +o 1o ) = suc 𝐴 )
37 35 36 syl ⊢ ( 𝐴 ∈ ω → ( 𝐴 +o 1o ) = suc 𝐴 )
38 37 fveq2d ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o 1o ) ) = ( 𝐺 ‘ suc 𝐴 ) )
39 38 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ ( 𝐴 +o 1o ) ) = ( 𝐺 ‘ suc 𝐴 ) )
40 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → 𝐶 ∈ No )
41 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
42 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → 𝐴 ∈ ω )
43 40 41 42 om2noseqsuc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ suc 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) +s 1s ) )
44 39 43 eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ ( 𝐴 +o 1o ) ) = ( ( 𝐺 ‘ 𝐴 ) +s 1s ) )
45 34 44 breqtrrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o 1o ) ) )
46 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ 𝐴 ) ∈ No )
47 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → 𝐺 : ω ⟶ No )
48 peano2 ⊢ ( 𝑧 ∈ ω → suc 𝑧 ∈ ω )
49 48 adantr ⊢ ( ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) → suc 𝑧 ∈ ω )
50 nnacl ⊢ ( ( 𝐴 ∈ ω ∧ suc 𝑧 ∈ ω ) → ( 𝐴 +o suc 𝑧 ) ∈ ω )
51 42 49 50 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐴 +o suc 𝑧 ) ∈ ω )
52 47 51 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ∈ No )
53 peano2 ⊢ ( suc 𝑧 ∈ ω → suc suc 𝑧 ∈ ω )
54 48 53 syl ⊢ ( 𝑧 ∈ ω → suc suc 𝑧 ∈ ω )
55 54 adantr ⊢ ( ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) → suc suc 𝑧 ∈ ω )
56 nnacl ⊢ ( ( 𝐴 ∈ ω ∧ suc suc 𝑧 ∈ ω ) → ( 𝐴 +o suc suc 𝑧 ) ∈ ω )
57 42 55 56 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐴 +o suc suc 𝑧 ) ∈ ω )
58 47 57 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) ∈ No )
59 simprr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) )
60 52 addsridd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) +s 0s ) = ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) )
61 28 a1i ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → 0s ∈ No )
62 30 a1i ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → 1s ∈ No )
63 61 62 52 sltadd2d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 0s <s 1s ↔ ( ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) +s 0s ) <s ( ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) +s 1s ) ) )
64 27 63 mpbii ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) +s 0s ) <s ( ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) +s 1s ) )
65 60 64 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) <s ( ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) +s 1s ) )
66 nnasuc ⊢ ( ( 𝐴 ∈ ω ∧ suc 𝑧 ∈ ω ) → ( 𝐴 +o suc suc 𝑧 ) = suc ( 𝐴 +o suc 𝑧 ) )
67 66 fveq2d ⊢ ( ( 𝐴 ∈ ω ∧ suc 𝑧 ∈ ω ) → ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) = ( 𝐺 ‘ suc ( 𝐴 +o suc 𝑧 ) ) )
68 42 49 67 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) = ( 𝐺 ‘ suc ( 𝐴 +o suc 𝑧 ) ) )
69 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → 𝐶 ∈ No )
70 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
71 69 70 51 om2noseqsuc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ suc ( 𝐴 +o suc 𝑧 ) ) = ( ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) +s 1s ) )
72 68 71 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) = ( ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) +s 1s ) )
73 65 72 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) <s ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) )
74 46 52 58 59 73 slttrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) )
75 74 expr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ 𝑧 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) ) )
76 75 expcom ⊢ ( 𝑧 ∈ ω → ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) ) ) )
77 11 15 19 45 76 finds2 ⊢ ( 𝑦 ∈ ω → ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) ) )
78 77 impcom ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) )
79 fveq2 ⊢ ( ( 𝐴 +o suc 𝑦 ) = 𝐵 → ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) = ( 𝐺 ‘ 𝐵 ) )
80 79 breq2d ⊢ ( ( 𝐴 +o suc 𝑦 ) = 𝐵 → ( ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) ↔ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
81 78 80 syl5ibcom ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( ( 𝐴 +o suc 𝑦 ) = 𝐵 → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
82 81 rexlimdva ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ∃ 𝑦 ∈ ω ( 𝐴 +o suc 𝑦 ) = 𝐵 → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
83 82 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ∃ 𝑦 ∈ ω ( 𝐴 +o suc 𝑦 ) = 𝐵 → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
84 5 83 sylbid ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )