Metamath Proof Explorer

Theorem om2noseqlt

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

Ref Expression
Hypotheses om2noseq.1 
|- ( ph -> C e. No )
om2noseq.2 
|- ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
om2noseq.3 
|- ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) )
Assertion om2noseqlt 
|- ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( A e. B -> ( G ` A )

Proof

Step Hyp Ref Expression
1 om2noseq.1 
 |-  ( ph -> C e. No )
2 om2noseq.2 
 |-  ( ph -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
3 om2noseq.3 
 |-  ( ph -> Z = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) " _om ) )
4 nnaordex2 
 |-  ( ( A e. _om /\ B e. _om ) -> ( A e. B <-> E. y e. _om ( A +o suc y ) = B ) )
5 4 adantl 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( A e. B <-> E. y e. _om ( A +o suc y ) = B ) )
6 suceq 
 |-  ( y = (/) -> suc y = suc (/) )
7 df-1o 
 |-  1o = suc (/)
8 6 7 eqtr4di 
 |-  ( y = (/) -> suc y = 1o )
9 8 oveq2d 
 |-  ( y = (/) -> ( A +o suc y ) = ( A +o 1o ) )
10 9 fveq2d 
 |-  ( y = (/) -> ( G ` ( A +o suc y ) ) = ( G ` ( A +o 1o ) ) )
11 10 breq2d 
 |-  ( y = (/) -> ( ( G ` A )  ( G ` A )
12 suceq 
 |-  ( y = z -> suc y = suc z )
13 12 oveq2d 
 |-  ( y = z -> ( A +o suc y ) = ( A +o suc z ) )
14 13 fveq2d 
 |-  ( y = z -> ( G ` ( A +o suc y ) ) = ( G ` ( A +o suc z ) ) )
15 14 breq2d 
 |-  ( y = z -> ( ( G ` A )  ( G ` A )
16 suceq 
 |-  ( y = suc z -> suc y = suc suc z )
17 16 oveq2d 
 |-  ( y = suc z -> ( A +o suc y ) = ( A +o suc suc z ) )
18 17 fveq2d 
 |-  ( y = suc z -> ( G ` ( A +o suc y ) ) = ( G ` ( A +o suc suc z ) ) )
19 18 breq2d 
 |-  ( y = suc z -> ( ( G ` A )  ( G ` A )
20 1 2 3 om2noseqfo 
 |-  ( ph -> G : _om -onto-> Z )
21 fof 
 |-  ( G : _om -onto-> Z -> G : _om --> Z )
22 20 21 syl 
 |-  ( ph -> G : _om --> Z )
23 3 1 noseqssno 
 |-  ( ph -> Z C_ No )
24 22 23 fssd 
 |-  ( ph -> G : _om --> No )
25 24 ffvelcdmda 
 |-  ( ( ph /\ A e. _om ) -> ( G ` A ) e. No )
26 25 addsridd 
 |-  ( ( ph /\ A e. _om ) -> ( ( G ` A ) +s 0s ) = ( G ` A ) )
27 0slt1s 
 |-  0s
28 0sno 
 |-  0s e. No
29 28 a1i 
 |-  ( ( ph /\ A e. _om ) -> 0s e. No )
30 1sno 
 |-  1s e. No
31 30 a1i 
 |-  ( ( ph /\ A e. _om ) -> 1s e. No )
32 29 31 25 sltadd2d 
 |-  ( ( ph /\ A e. _om ) -> ( 0s  ( ( G ` A ) +s 0s )
33 27 32 mpbii 
 |-  ( ( ph /\ A e. _om ) -> ( ( G ` A ) +s 0s )
34 26 33 eqbrtrrd 
 |-  ( ( ph /\ A e. _om ) -> ( G ` A )
35 nnon 
 |-  ( A e. _om -> A e. On )
36 oa1suc 
 |-  ( A e. On -> ( A +o 1o ) = suc A )
37 35 36 syl 
 |-  ( A e. _om -> ( A +o 1o ) = suc A )
38 37 fveq2d 
 |-  ( A e. _om -> ( G ` ( A +o 1o ) ) = ( G ` suc A ) )
39 38 adantl 
 |-  ( ( ph /\ A e. _om ) -> ( G ` ( A +o 1o ) ) = ( G ` suc A ) )
40 1 adantr 
 |-  ( ( ph /\ A e. _om ) -> C e. No )
41 2 adantr 
 |-  ( ( ph /\ A e. _om ) -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
42 simpr 
 |-  ( ( ph /\ A e. _om ) -> A e. _om )
43 40 41 42 om2noseqsuc 
 |-  ( ( ph /\ A e. _om ) -> ( G ` suc A ) = ( ( G ` A ) +s 1s ) )
44 39 43 eqtrd 
 |-  ( ( ph /\ A e. _om ) -> ( G ` ( A +o 1o ) ) = ( ( G ` A ) +s 1s ) )
45 34 44 breqtrrd 
 |-  ( ( ph /\ A e. _om ) -> ( G ` A )
46 25 adantr 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` A ) e. No )
47 24 ad2antrr 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  G : _om --> No )
48 peano2 
 |-  ( z e. _om -> suc z e. _om )
49 48 adantr 
 |-  ( ( z e. _om /\ ( G ` A )  suc z e. _om )
50 nnacl 
 |-  ( ( A e. _om /\ suc z e. _om ) -> ( A +o suc z ) e. _om )
51 42 49 50 syl2an 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( A +o suc z ) e. _om )
52 47 51 ffvelcdmd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc z ) ) e. No )
53 peano2 
 |-  ( suc z e. _om -> suc suc z e. _om )
54 48 53 syl 
 |-  ( z e. _om -> suc suc z e. _om )
55 54 adantr 
 |-  ( ( z e. _om /\ ( G ` A )  suc suc z e. _om )
56 nnacl 
 |-  ( ( A e. _om /\ suc suc z e. _om ) -> ( A +o suc suc z ) e. _om )
57 42 55 56 syl2an 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( A +o suc suc z ) e. _om )
58 47 57 ffvelcdmd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc suc z ) ) e. No )
59 simprr 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` A )
60 52 addsridd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( ( G ` ( A +o suc z ) ) +s 0s ) = ( G ` ( A +o suc z ) ) )
61 28 a1i 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  0s e. No )
62 30 a1i 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  1s e. No )
63 61 62 52 sltadd2d 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( 0s  ( ( G ` ( A +o suc z ) ) +s 0s )
64 27 63 mpbii 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( ( G ` ( A +o suc z ) ) +s 0s )
65 60 64 eqbrtrrd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc z ) )
66 nnasuc 
 |-  ( ( A e. _om /\ suc z e. _om ) -> ( A +o suc suc z ) = suc ( A +o suc z ) )
67 66 fveq2d 
 |-  ( ( A e. _om /\ suc z e. _om ) -> ( G ` ( A +o suc suc z ) ) = ( G ` suc ( A +o suc z ) ) )
68 42 49 67 syl2an 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc suc z ) ) = ( G ` suc ( A +o suc z ) ) )
69 1 ad2antrr 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  C e. No )
70 2 ad2antrr 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
71 69 70 51 om2noseqsuc 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` suc ( A +o suc z ) ) = ( ( G ` ( A +o suc z ) ) +s 1s ) )
72 68 71 eqtrd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc suc z ) ) = ( ( G ` ( A +o suc z ) ) +s 1s ) )
73 65 72 breqtrrd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc z ) )
74 46 52 58 59 73 slttrd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` A )
75 74 expr 
 |-  ( ( ( ph /\ A e. _om ) /\ z e. _om ) -> ( ( G ` A )  ( G ` A )
76 75 expcom 
 |-  ( z e. _om -> ( ( ph /\ A e. _om ) -> ( ( G ` A )  ( G ` A )
77 11 15 19 45 76 finds2 
 |-  ( y e. _om -> ( ( ph /\ A e. _om ) -> ( G ` A )
78 77 impcom 
 |-  ( ( ( ph /\ A e. _om ) /\ y e. _om ) -> ( G ` A )
79 fveq2 
 |-  ( ( A +o suc y ) = B -> ( G ` ( A +o suc y ) ) = ( G ` B ) )
80 79 breq2d 
 |-  ( ( A +o suc y ) = B -> ( ( G ` A )  ( G ` A )
81 78 80 syl5ibcom 
 |-  ( ( ( ph /\ A e. _om ) /\ y e. _om ) -> ( ( A +o suc y ) = B -> ( G ` A )
82 81 rexlimdva 
 |-  ( ( ph /\ A e. _om ) -> ( E. y e. _om ( A +o suc y ) = B -> ( G ` A )
83 82 adantrr 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( E. y e. _om ( A +o suc y ) = B -> ( G ` A )
84 5 83 sylbid 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( A e. B -> ( G ` A )