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 sltp1d 
 |-  ( ( ph /\ A e. _om ) -> ( G ` A )
27 nnon 
 |-  ( A e. _om -> A e. On )
28 oa1suc 
 |-  ( A e. On -> ( A +o 1o ) = suc A )
29 27 28 syl 
 |-  ( A e. _om -> ( A +o 1o ) = suc A )
30 29 fveq2d 
 |-  ( A e. _om -> ( G ` ( A +o 1o ) ) = ( G ` suc A ) )
31 30 adantl 
 |-  ( ( ph /\ A e. _om ) -> ( G ` ( A +o 1o ) ) = ( G ` suc A ) )
32 1 adantr 
 |-  ( ( ph /\ A e. _om ) -> C e. No )
33 2 adantr 
 |-  ( ( ph /\ A e. _om ) -> G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
34 simpr 
 |-  ( ( ph /\ A e. _om ) -> A e. _om )
35 32 33 34 om2noseqsuc 
 |-  ( ( ph /\ A e. _om ) -> ( G ` suc A ) = ( ( G ` A ) +s 1s ) )
36 31 35 eqtrd 
 |-  ( ( ph /\ A e. _om ) -> ( G ` ( A +o 1o ) ) = ( ( G ` A ) +s 1s ) )
37 26 36 breqtrrd 
 |-  ( ( ph /\ A e. _om ) -> ( G ` A )
38 25 adantr 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` A ) e. No )
39 24 ad2antrr 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  G : _om --> No )
40 peano2 
 |-  ( z e. _om -> suc z e. _om )
41 40 adantr 
 |-  ( ( z e. _om /\ ( G ` A )  suc z e. _om )
42 nnacl 
 |-  ( ( A e. _om /\ suc z e. _om ) -> ( A +o suc z ) e. _om )
43 34 41 42 syl2an 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( A +o suc z ) e. _om )
44 39 43 ffvelcdmd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc z ) ) e. No )
45 peano2 
 |-  ( suc z e. _om -> suc suc z e. _om )
46 40 45 syl 
 |-  ( z e. _om -> suc suc z e. _om )
47 46 adantr 
 |-  ( ( z e. _om /\ ( G ` A )  suc suc z e. _om )
48 nnacl 
 |-  ( ( A e. _om /\ suc suc z e. _om ) -> ( A +o suc suc z ) e. _om )
49 34 47 48 syl2an 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( A +o suc suc z ) e. _om )
50 39 49 ffvelcdmd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc suc z ) ) e. No )
51 simprr 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` A )
52 44 sltp1d 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc z ) )
53 nnasuc 
 |-  ( ( A e. _om /\ suc z e. _om ) -> ( A +o suc suc z ) = suc ( A +o suc z ) )
54 53 fveq2d 
 |-  ( ( A e. _om /\ suc z e. _om ) -> ( G ` ( A +o suc suc z ) ) = ( G ` suc ( A +o suc z ) ) )
55 34 41 54 syl2an 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc suc z ) ) = ( G ` suc ( A +o suc z ) ) )
56 1 ad2antrr 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  C e. No )
57 2 ad2antrr 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  G = ( rec ( ( x e. _V |-> ( x +s 1s ) ) , C ) |` _om ) )
58 56 57 43 om2noseqsuc 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` suc ( A +o suc z ) ) = ( ( G ` ( A +o suc z ) ) +s 1s ) )
59 55 58 eqtrd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc suc z ) ) = ( ( G ` ( A +o suc z ) ) +s 1s ) )
60 52 59 breqtrrd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` ( A +o suc z ) )
61 38 44 50 51 60 slttrd 
 |-  ( ( ( ph /\ A e. _om ) /\ ( z e. _om /\ ( G ` A )  ( G ` A )
62 61 expr 
 |-  ( ( ( ph /\ A e. _om ) /\ z e. _om ) -> ( ( G ` A )  ( G ` A )
63 62 expcom 
 |-  ( z e. _om -> ( ( ph /\ A e. _om ) -> ( ( G ` A )  ( G ` A )
64 11 15 19 37 63 finds2 
 |-  ( y e. _om -> ( ( ph /\ A e. _om ) -> ( G ` A )
65 64 impcom 
 |-  ( ( ( ph /\ A e. _om ) /\ y e. _om ) -> ( G ` A )
66 fveq2 
 |-  ( ( A +o suc y ) = B -> ( G ` ( A +o suc y ) ) = ( G ` B ) )
67 66 breq2d 
 |-  ( ( A +o suc y ) = B -> ( ( G ` A )  ( G ` A )
68 65 67 syl5ibcom 
 |-  ( ( ( ph /\ A e. _om ) /\ y e. _om ) -> ( ( A +o suc y ) = B -> ( G ` A )
69 68 rexlimdva 
 |-  ( ( ph /\ A e. _om ) -> ( E. y e. _om ( A +o suc y ) = B -> ( G ` A )
70 69 adantrr 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( E. y e. _om ( A +o suc y ) = B -> ( G ` A )
71 5 70 sylbid 
 |-  ( ( ph /\ ( A e. _om /\ B e. _om ) ) -> ( A e. B -> ( G ` A )