Metamath Proof Explorer

Theorem noresle

Description: Restriction law for surreals. Lemma 2.1.4 of Lipparini p. 3. (Contributed by Scott Fenton, 5-Dec-2021)

Ref Expression
Assertion noresle 
|- ( ( ( U e. No /\ S e. No ) /\ ( dom U C_ A /\ dom S C_ A /\ A. g e. A -. ( S |` suc g )  -. S

Proof

Step Hyp Ref Expression
1 unss 
 |-  ( ( dom U C_ A /\ dom S C_ A ) <-> ( dom U u. dom S ) C_ A )
2 ssralv 
 |-  ( ( dom U u. dom S ) C_ A -> ( A. g e. A -. ( S |` suc g )  A. g e. ( dom U u. dom S ) -. ( S |` suc g )
3 1 2 sylbi 
 |-  ( ( dom U C_ A /\ dom S C_ A ) -> ( A. g e. A -. ( S |` suc g )  A. g e. ( dom U u. dom S ) -. ( S |` suc g )
4 3 3impia 
 |-  ( ( dom U C_ A /\ dom S C_ A /\ A. g e. A -. ( S |` suc g )  A. g e. ( dom U u. dom S ) -. ( S |` suc g )
5 breq1 
 |-  ( U = S -> ( U  S
6 5 notbid 
 |-  ( U = S -> ( -. U  -. S
7 6 biimpd 
 |-  ( U = S -> ( -. U  -. S
8 sltso 
 |-
9 sonr 
 |-  ( (  -. U
10 8 9 mpan 
 |-  ( U e. No -> -. U
11 10 adantr 
 |-  ( ( U e. No /\ S e. No ) -> -. U
12 7 11 impel 
 |-  ( ( U = S /\ ( U e. No /\ S e. No ) ) -> -. S
13 12 adantrr 
 |-  ( ( U = S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  -. S
14 13 ex 
 |-  ( U = S -> ( ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  -. S
15 simprl 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  ( U e. No /\ S e. No ) )
16 simprll 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  U e. No )
17 simprlr 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  S e. No )
18 simpl 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  U =/= S )
19 nosepne 
 |-  ( ( U e. No /\ S e. No /\ U =/= S ) -> ( U ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) =/= ( S ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) )
20 16 17 18 19 syl3anc 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  ( U ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) =/= ( S ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) )
21 nosepon 
 |-  ( ( U e. No /\ S e. No /\ U =/= S ) -> |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. On )
22 16 17 18 21 syl3anc 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. On )
23 sucidg 
 |-  ( |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. On -> |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )
24 22 23 syl 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )
25 24 fvresd 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  ( ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) = ( U ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) )
26 24 fvresd 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  ( ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) = ( S ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) )
27 20 25 26 3netr4d 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  ( ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) =/= ( ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) )
28 27 neneqd 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  -. ( ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) = ( ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) )
29 fveq1 
 |-  ( ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) = ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) -> ( ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) = ( ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) ` |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) )
30 28 29 nsyl 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  -. ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) = ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) )
31 nosepdm 
 |-  ( ( U e. No /\ S e. No /\ U =/= S ) -> |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. ( dom U u. dom S ) )
32 16 17 18 31 syl3anc 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. ( dom U u. dom S ) )
33 simprr 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  A. g e. ( dom U u. dom S ) -. ( S |` suc g )
34 suceq 
 |-  ( g = |^| { x e. On | ( U ` x ) =/= ( S ` x ) } -> suc g = suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )
35 34 reseq2d 
 |-  ( g = |^| { x e. On | ( U ` x ) =/= ( S ` x ) } -> ( S |` suc g ) = ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) )
36 34 reseq2d 
 |-  ( g = |^| { x e. On | ( U ` x ) =/= ( S ` x ) } -> ( U |` suc g ) = ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) )
37 35 36 breq12d 
 |-  ( g = |^| { x e. On | ( U ` x ) =/= ( S ` x ) } -> ( ( S |` suc g )  ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )
38 37 notbid 
 |-  ( g = |^| { x e. On | ( U ` x ) =/= ( S ` x ) } -> ( -. ( S |` suc g )  -. ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )
39 38 rspcv 
 |-  ( |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. ( dom U u. dom S ) -> ( A. g e. ( dom U u. dom S ) -. ( S |` suc g )  -. ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )
40 32 33 39 sylc 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  -. ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )
41 suceloni 
 |-  ( |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. On -> suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. On )
42 22 41 syl 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. On )
43 noreson 
 |-  ( ( U e. No /\ suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. On ) -> ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) e. No )
44 16 42 43 syl2anc 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) e. No )
45 noreson 
 |-  ( ( S e. No /\ suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. On ) -> ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) e. No )
46 17 42 45 syl2anc 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) e. No )
47 solin 
 |-  ( (  ( ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )
48 8 47 mpan 
 |-  ( ( ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) e. No /\ ( S |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } ) e. No ) -> ( ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )
49 44 46 48 syl2anc 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  ( ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )
50 30 40 49 ecase23d 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )
51 sltres 
 |-  ( ( U e. No /\ S e. No /\ suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } e. On ) -> ( ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )  U
52 16 17 42 51 syl3anc 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  ( ( U |` suc |^| { x e. On | ( U ` x ) =/= ( S ` x ) } )  U
53 50 52 mpd 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  U
54 soasym 
 |-  ( (  ( U  -. S
55 8 54 mpan 
 |-  ( ( U e. No /\ S e. No ) -> ( U  -. S
56 15 53 55 sylc 
 |-  ( ( U =/= S /\ ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  -. S
57 56 ex 
 |-  ( U =/= S -> ( ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  -. S
58 14 57 pm2.61ine 
 |-  ( ( ( U e. No /\ S e. No ) /\ A. g e. ( dom U u. dom S ) -. ( S |` suc g )  -. S
59 4 58 sylan2 
 |-  ( ( ( U e. No /\ S e. No ) /\ ( dom U C_ A /\ dom S C_ A /\ A. g e. A -. ( S |` suc g )  -. S