Metamath Proof Explorer

Theorem precsexlem8

Description: Lemma for surreal reciprocal. Show that the left and right functions give sets of surreals. (Contributed by Scott Fenton, 13-Mar-2025)

Ref Expression
Hypotheses precsexlem.1 
|- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. )
precsexlem.2 
|- L = ( 1st o. F )
precsexlem.3 
|- R = ( 2nd o. F )
precsexlem.4 
|- ( ph -> A e. No )
precsexlem.5 
|- ( ph -> 0s
precsexlem.6 
|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
Assertion precsexlem8 
|- ( ( ph /\ I e. _om ) -> ( ( L ` I ) C_ No /\ ( R ` I ) C_ No ) )

Proof

Step Hyp Ref Expression
1 precsexlem.1 
 |-  F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. )
2 precsexlem.2 
 |-  L = ( 1st o. F )
3 precsexlem.3 
 |-  R = ( 2nd o. F )
4 precsexlem.4 
 |-  ( ph -> A e. No )
5 precsexlem.5 
 |-  ( ph -> 0s
6 precsexlem.6 
 |-  ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
7 fveq2 
 |-  ( i = (/) -> ( L ` i ) = ( L ` (/) ) )
8 7 sseq1d 
 |-  ( i = (/) -> ( ( L ` i ) C_ No <-> ( L ` (/) ) C_ No ) )
9 fveq2 
 |-  ( i = (/) -> ( R ` i ) = ( R ` (/) ) )
10 9 sseq1d 
 |-  ( i = (/) -> ( ( R ` i ) C_ No <-> ( R ` (/) ) C_ No ) )
11 8 10 anbi12d 
 |-  ( i = (/) -> ( ( ( L ` i ) C_ No /\ ( R ` i ) C_ No ) <-> ( ( L ` (/) ) C_ No /\ ( R ` (/) ) C_ No ) ) )
12 11 imbi2d 
 |-  ( i = (/) -> ( ( ph -> ( ( L ` i ) C_ No /\ ( R ` i ) C_ No ) ) <-> ( ph -> ( ( L ` (/) ) C_ No /\ ( R ` (/) ) C_ No ) ) ) )
13 fveq2 
 |-  ( i = j -> ( L ` i ) = ( L ` j ) )
14 13 sseq1d 
 |-  ( i = j -> ( ( L ` i ) C_ No <-> ( L ` j ) C_ No ) )
15 fveq2 
 |-  ( i = j -> ( R ` i ) = ( R ` j ) )
16 15 sseq1d 
 |-  ( i = j -> ( ( R ` i ) C_ No <-> ( R ` j ) C_ No ) )
17 14 16 anbi12d 
 |-  ( i = j -> ( ( ( L ` i ) C_ No /\ ( R ` i ) C_ No ) <-> ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) )
18 17 imbi2d 
 |-  ( i = j -> ( ( ph -> ( ( L ` i ) C_ No /\ ( R ` i ) C_ No ) ) <-> ( ph -> ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) ) )
19 fveq2 
 |-  ( i = suc j -> ( L ` i ) = ( L ` suc j ) )
20 19 sseq1d 
 |-  ( i = suc j -> ( ( L ` i ) C_ No <-> ( L ` suc j ) C_ No ) )
21 fveq2 
 |-  ( i = suc j -> ( R ` i ) = ( R ` suc j ) )
22 21 sseq1d 
 |-  ( i = suc j -> ( ( R ` i ) C_ No <-> ( R ` suc j ) C_ No ) )
23 20 22 anbi12d 
 |-  ( i = suc j -> ( ( ( L ` i ) C_ No /\ ( R ` i ) C_ No ) <-> ( ( L ` suc j ) C_ No /\ ( R ` suc j ) C_ No ) ) )
24 23 imbi2d 
 |-  ( i = suc j -> ( ( ph -> ( ( L ` i ) C_ No /\ ( R ` i ) C_ No ) ) <-> ( ph -> ( ( L ` suc j ) C_ No /\ ( R ` suc j ) C_ No ) ) ) )
25 fveq2 
 |-  ( i = I -> ( L ` i ) = ( L ` I ) )
26 25 sseq1d 
 |-  ( i = I -> ( ( L ` i ) C_ No <-> ( L ` I ) C_ No ) )
27 fveq2 
 |-  ( i = I -> ( R ` i ) = ( R ` I ) )
28 27 sseq1d 
 |-  ( i = I -> ( ( R ` i ) C_ No <-> ( R ` I ) C_ No ) )
29 26 28 anbi12d 
 |-  ( i = I -> ( ( ( L ` i ) C_ No /\ ( R ` i ) C_ No ) <-> ( ( L ` I ) C_ No /\ ( R ` I ) C_ No ) ) )
30 29 imbi2d 
 |-  ( i = I -> ( ( ph -> ( ( L ` i ) C_ No /\ ( R ` i ) C_ No ) ) <-> ( ph -> ( ( L ` I ) C_ No /\ ( R ` I ) C_ No ) ) ) )
31 1 2 3 precsexlem1 
 |-  ( L ` (/) ) = { 0s }
32 0sno 
 |-  0s e. No
33 snssi 
 |-  ( 0s e. No -> { 0s } C_ No )
34 32 33 ax-mp 
 |-  { 0s } C_ No
35 31 34 eqsstri 
 |-  ( L ` (/) ) C_ No
36 1 2 3 precsexlem2 
 |-  ( R ` (/) ) = (/)
37 0ss 
 |-  (/) C_ No
38 36 37 eqsstri 
 |-  ( R ` (/) ) C_ No
39 35 38 pm3.2i 
 |-  ( ( L ` (/) ) C_ No /\ ( R ` (/) ) C_ No )
40 39 a1i 
 |-  ( ph -> ( ( L ` (/) ) C_ No /\ ( R ` (/) ) C_ No ) )
41 1 2 3 precsexlem4 
 |-  ( j e. _om -> ( L ` suc j ) = ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
42 41 3ad2ant2 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( L ` suc j ) = ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
43 simp3l 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( L ` j ) C_ No )
44 1sno 
 |-  1s e. No
45 44 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> 1s e. No )
46 rightssno 
 |-  ( _Right ` A ) C_ No
47 simprl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> xR e. ( _Right ` A ) )
48 46 47 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> xR e. No )
49 4 3ad2ant1 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> A e. No )
50 49 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> A e. No )
51 48 50 subscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> ( xR -s A ) e. No )
52 simpl3l 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> ( L ` j ) C_ No )
53 simprr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> yL e. ( L ` j ) )
54 52 53 sseldd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> yL e. No )
55 51 54 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> ( ( xR -s A ) x.s yL ) e. No )
56 45 55 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> ( 1s +s ( ( xR -s A ) x.s yL ) ) e. No )
57 32 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> 0s e. No )
58 5 3ad2ant1 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> 0s
59 58 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> 0s
60 breq2 
 |-  ( xO = xR -> ( A  A
61 rightval 
 |-  ( _Right ` A ) = { xO e. ( _Old ` ( bday ` A ) ) | A
62 60 61 elrab2 
 |-  ( xR e. ( _Right ` A ) <-> ( xR e. ( _Old ` ( bday ` A ) ) /\ A
63 62 simprbi 
 |-  ( xR e. ( _Right ` A ) -> A
64 47 63 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> A
65 57 50 48 59 64 slttrd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> 0s
66 65 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> xR =/= 0s )
67 breq2 
 |-  ( xO = xR -> ( 0s  0s
68 oveq1 
 |-  ( xO = xR -> ( xO x.s y ) = ( xR x.s y ) )
69 68 eqeq1d 
 |-  ( xO = xR -> ( ( xO x.s y ) = 1s <-> ( xR x.s y ) = 1s ) )
70 69 rexbidv 
 |-  ( xO = xR -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xR x.s y ) = 1s ) )
71 67 70 imbi12d 
 |-  ( xO = xR -> ( ( 0s  E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s  E. y e. No ( xR x.s y ) = 1s ) ) )
72 6 3ad2ant1 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
73 72 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
74 elun2 
 |-  ( xR e. ( _Right ` A ) -> xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
75 47 74 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
76 71 73 75 rspcdva 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> ( 0s  E. y e. No ( xR x.s y ) = 1s ) )
77 65 76 mpd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> E. y e. No ( xR x.s y ) = 1s )
78 56 48 66 77 divsclwd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) e. No )
79 eleq1 
 |-  ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( a e. No <-> ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) e. No ) )
80 78 79 syl5ibrcom 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> a e. No ) )
81 80 rexlimdvva 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> a e. No ) )
82 81 abssdv 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } C_ No )
83 44 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  1s e. No )
84 leftssno 
 |-  ( _Left ` A ) C_ No
85 ssrab2 
 |-  { x e. ( _Left ` A ) | 0s
86 simprl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. { x e. ( _Left ` A ) | 0s
87 85 86 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. ( _Left ` A ) )
88 84 87 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. No )
89 49 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  A e. No )
90 88 89 subscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( xL -s A ) e. No )
91 simpl3r 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( R ` j ) C_ No )
92 simprr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  yR e. ( R ` j ) )
93 91 92 sseldd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  yR e. No )
94 90 93 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( ( xL -s A ) x.s yR ) e. No )
95 83 94 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( 1s +s ( ( xL -s A ) x.s yR ) ) e. No )
96 breq2 
 |-  ( x = xL -> ( 0s  0s
97 96 elrab 
 |-  ( xL e. { x e. ( _Left ` A ) | 0s  ( xL e. ( _Left ` A ) /\ 0s
98 97 simprbi 
 |-  ( xL e. { x e. ( _Left ` A ) | 0s  0s
99 86 98 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  0s
100 99 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL =/= 0s )
101 breq2 
 |-  ( xO = xL -> ( 0s  0s
102 oveq1 
 |-  ( xO = xL -> ( xO x.s y ) = ( xL x.s y ) )
103 102 eqeq1d 
 |-  ( xO = xL -> ( ( xO x.s y ) = 1s <-> ( xL x.s y ) = 1s ) )
104 103 rexbidv 
 |-  ( xO = xL -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xL x.s y ) = 1s ) )
105 101 104 imbi12d 
 |-  ( xO = xL -> ( ( 0s  E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s  E. y e. No ( xL x.s y ) = 1s ) ) )
106 72 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
107 elun1 
 |-  ( xL e. ( _Left ` A ) -> xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
108 87 107 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
109 105 106 108 rspcdva 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( 0s  E. y e. No ( xL x.s y ) = 1s ) )
110 99 109 mpd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  E. y e. No ( xL x.s y ) = 1s )
111 95 88 100 110 divsclwd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) e. No )
112 eleq1 
 |-  ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( a e. No <-> ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) e. No ) )
113 111 112 syl5ibrcom 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> a e. No ) )
114 113 rexlimdvva 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s  a e. No ) )
115 114 abssdv 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> { a | E. xL e. { x e. ( _Left ` A ) | 0s
116 82 115 unssd 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
117 43 116 unssd 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( ( L ` j ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
118 42 117 eqsstrd 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( L ` suc j ) C_ No )
119 1 2 3 precsexlem5 
 |-  ( j e. _om -> ( R ` suc j ) = ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
120 119 3ad2ant2 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( R ` suc j ) = ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
121 simp3r 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( R ` j ) C_ No )
122 44 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  1s e. No )
123 simprl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. { x e. ( _Left ` A ) | 0s
124 85 123 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. ( _Left ` A ) )
125 84 124 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. No )
126 49 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  A e. No )
127 125 126 subscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( xL -s A ) e. No )
128 simpl3l 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( L ` j ) C_ No )
129 simprr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  yL e. ( L ` j ) )
130 128 129 sseldd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  yL e. No )
131 127 130 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( ( xL -s A ) x.s yL ) e. No )
132 122 131 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( 1s +s ( ( xL -s A ) x.s yL ) ) e. No )
133 123 98 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  0s
134 133 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL =/= 0s )
135 72 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
136 124 107 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
137 105 135 136 rspcdva 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( 0s  E. y e. No ( xL x.s y ) = 1s ) )
138 133 137 mpd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  E. y e. No ( xL x.s y ) = 1s )
139 132 125 134 138 divsclwd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) e. No )
140 eleq1 
 |-  ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( a e. No <-> ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) e. No ) )
141 139 140 syl5ibrcom 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> a e. No ) )
142 141 rexlimdvva 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s  a e. No ) )
143 142 abssdv 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> { a | E. xL e. { x e. ( _Left ` A ) | 0s
144 44 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> 1s e. No )
145 simprl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> xR e. ( _Right ` A ) )
146 46 145 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> xR e. No )
147 49 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> A e. No )
148 146 147 subscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> ( xR -s A ) e. No )
149 simpl3r 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> ( R ` j ) C_ No )
150 simprr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> yR e. ( R ` j ) )
151 149 150 sseldd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> yR e. No )
152 148 151 mulscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> ( ( xR -s A ) x.s yR ) e. No )
153 144 152 addscld 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> ( 1s +s ( ( xR -s A ) x.s yR ) ) e. No )
154 32 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> 0s e. No )
155 58 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> 0s
156 145 63 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> A
157 154 147 146 155 156 slttrd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> 0s
158 157 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> xR =/= 0s )
159 72 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s  E. y e. No ( xO x.s y ) = 1s ) )
160 145 74 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
161 71 159 160 rspcdva 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> ( 0s  E. y e. No ( xR x.s y ) = 1s ) )
162 157 161 mpd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> E. y e. No ( xR x.s y ) = 1s )
163 153 146 158 162 divsclwd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) e. No )
164 eleq1 
 |-  ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( a e. No <-> ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) e. No ) )
165 163 164 syl5ibrcom 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> a e. No ) )
166 165 rexlimdvva 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> a e. No ) )
167 166 abssdv 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } C_ No )
168 143 167 unssd 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
169 121 168 unssd 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
170 120 169 eqsstrd 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( R ` suc j ) C_ No )
171 118 170 jca 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( ( L ` suc j ) C_ No /\ ( R ` suc j ) C_ No ) )
172 171 3exp 
 |-  ( ph -> ( j e. _om -> ( ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) -> ( ( L ` suc j ) C_ No /\ ( R ` suc j ) C_ No ) ) ) )
173 172 com12 
 |-  ( j e. _om -> ( ph -> ( ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) -> ( ( L ` suc j ) C_ No /\ ( R ` suc j ) C_ No ) ) ) )
174 173 a2d 
 |-  ( j e. _om -> ( ( ph -> ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( ph -> ( ( L ` suc j ) C_ No /\ ( R ` suc j ) C_ No ) ) ) )
175 12 18 24 30 40 174 finds 
 |-  ( I e. _om -> ( ph -> ( ( L ` I ) C_ No /\ ( R ` I ) C_ No ) ) )
176 175 impcom 
 |-  ( ( ph /\ I e. _om ) -> ( ( L ` I ) C_ No /\ ( R ` I ) C_ No ) )