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 ltsp1d ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ 𝐴 ) <s ( ( 𝐺 ‘ 𝐴 ) +s 1s ) )
27 nnon ⊢ ( 𝐴 ∈ ω → 𝐴 ∈ On )
28 oa1suc ⊢ ( 𝐴 ∈ On → ( 𝐴 +o 1o ) = suc 𝐴 )
29 27 28 syl ⊢ ( 𝐴 ∈ ω → ( 𝐴 +o 1o ) = suc 𝐴 )
30 29 fveq2d ⊢ ( 𝐴 ∈ ω → ( 𝐺 ‘ ( 𝐴 +o 1o ) ) = ( 𝐺 ‘ suc 𝐴 ) )
31 30 adantl ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ ( 𝐴 +o 1o ) ) = ( 𝐺 ‘ suc 𝐴 ) )
32 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → 𝐶 ∈ No )
33 2 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
34 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → 𝐴 ∈ ω )
35 32 33 34 om2noseqsuc ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ suc 𝐴 ) = ( ( 𝐺 ‘ 𝐴 ) +s 1s ) )
36 31 35 eqtrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ ( 𝐴 +o 1o ) ) = ( ( 𝐺 ‘ 𝐴 ) +s 1s ) )
37 26 36 breqtrrd ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o 1o ) ) )
38 25 adantr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ 𝐴 ) ∈ No )
39 24 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → 𝐺 : ω ⟶ No )
40 peano2 ⊢ ( 𝑧 ∈ ω → suc 𝑧 ∈ ω )
41 40 adantr ⊢ ( ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) → suc 𝑧 ∈ ω )
42 nnacl ⊢ ( ( 𝐴 ∈ ω ∧ suc 𝑧 ∈ ω ) → ( 𝐴 +o suc 𝑧 ) ∈ ω )
43 34 41 42 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐴 +o suc 𝑧 ) ∈ ω )
44 39 43 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ∈ No )
45 peano2 ⊢ ( suc 𝑧 ∈ ω → suc suc 𝑧 ∈ ω )
46 40 45 syl ⊢ ( 𝑧 ∈ ω → suc suc 𝑧 ∈ ω )
47 46 adantr ⊢ ( ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) → suc suc 𝑧 ∈ ω )
48 nnacl ⊢ ( ( 𝐴 ∈ ω ∧ suc suc 𝑧 ∈ ω ) → ( 𝐴 +o suc suc 𝑧 ) ∈ ω )
49 34 47 48 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐴 +o suc suc 𝑧 ) ∈ ω )
50 39 49 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) ∈ No )
51 simprr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) )
52 44 ltsp1d ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) <s ( ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) +s 1s ) )
53 nnasuc ⊢ ( ( 𝐴 ∈ ω ∧ suc 𝑧 ∈ ω ) → ( 𝐴 +o suc suc 𝑧 ) = suc ( 𝐴 +o suc 𝑧 ) )
54 53 fveq2d ⊢ ( ( 𝐴 ∈ ω ∧ suc 𝑧 ∈ ω ) → ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) = ( 𝐺 ‘ suc ( 𝐴 +o suc 𝑧 ) ) )
55 34 41 54 syl2an ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) = ( 𝐺 ‘ suc ( 𝐴 +o suc 𝑧 ) ) )
56 1 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → 𝐶 ∈ No )
57 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → 𝐺 = ( rec ( ( 𝑥 ∈ V ↦ ( 𝑥 +s 1s ) ) , 𝐶 ) ↾ ω ) )
58 56 57 43 om2noseqsuc ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ suc ( 𝐴 +o suc 𝑧 ) ) = ( ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) +s 1s ) )
59 55 58 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) = ( ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) +s 1s ) )
60 52 59 breqtrrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) <s ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) )
61 38 44 50 51 60 ltstrd ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ ( 𝑧 ∈ ω ∧ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) ) ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) )
62 61 expr ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ 𝑧 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) ) )
63 62 expcom ⊢ ( 𝑧 ∈ ω → ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑧 ) ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc suc 𝑧 ) ) ) ) )
64 11 15 19 37 63 finds2 ⊢ ( 𝑦 ∈ ω → ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) ) )
65 64 impcom ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) )
66 fveq2 ⊢ ( ( 𝐴 +o suc 𝑦 ) = 𝐵 → ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) = ( 𝐺 ‘ 𝐵 ) )
67 66 breq2d ⊢ ( ( 𝐴 +o suc 𝑦 ) = 𝐵 → ( ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ ( 𝐴 +o suc 𝑦 ) ) ↔ ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
68 65 67 syl5ibcom ⊢ ( ( ( 𝜑 ∧ 𝐴 ∈ ω ) ∧ 𝑦 ∈ ω ) → ( ( 𝐴 +o suc 𝑦 ) = 𝐵 → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
69 68 rexlimdva ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ω ) → ( ∃ 𝑦 ∈ ω ( 𝐴 +o suc 𝑦 ) = 𝐵 → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
70 69 adantrr ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( ∃ 𝑦 ∈ ω ( 𝐴 +o suc 𝑦 ) = 𝐵 → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )
71 5 70 sylbid ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) ) → ( 𝐴 ∈ 𝐵 → ( 𝐺 ‘ 𝐴 ) <s ( 𝐺 ‘ 𝐵 ) ) )