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 rightgt 
 |-  ( xR e. ( _Right ` A ) -> A
61 47 60 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> A
62 57 50 48 59 61 slttrd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> 0s
63 62 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yL e. ( L ` j ) ) ) -> xR =/= 0s )
64 breq2 
 |-  ( xO = xR -> ( 0s  0s
65 oveq1 
 |-  ( xO = xR -> ( xO x.s y ) = ( xR x.s y ) )
66 65 eqeq1d 
 |-  ( xO = xR -> ( ( xO x.s y ) = 1s <-> ( xR x.s y ) = 1s ) )
67 66 rexbidv 
 |-  ( xO = xR -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xR x.s y ) = 1s ) )
68 64 67 imbi12d 
 |-  ( xO = xR -> ( ( 0s  E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s  E. y e. No ( xR x.s y ) = 1s ) ) )
69 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 ) )
70 69 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 ) )
71 elun2 
 |-  ( xR e. ( _Right ` A ) -> xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
72 47 71 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 ) ) )
73 68 70 72 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 ) )
74 62 73 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 )
75 56 48 63 74 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 )
76 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 ) )
77 75 76 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 ) )
78 77 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 ) )
79 78 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 )
80 44 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  1s e. No )
81 leftssno 
 |-  ( _Left ` A ) C_ No
82 ssrab2 
 |-  { x e. ( _Left ` A ) | 0s
83 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
84 82 83 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. ( _Left ` A ) )
85 81 84 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. No )
86 49 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  A e. No )
87 85 86 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 )
88 simpl3r 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( R ` j ) C_ No )
89 simprr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  yR e. ( R ` j ) )
90 88 89 sseldd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  yR e. No )
91 87 90 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 )
92 80 91 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 )
93 breq2 
 |-  ( x = xL -> ( 0s  0s
94 93 elrab 
 |-  ( xL e. { x e. ( _Left ` A ) | 0s  ( xL e. ( _Left ` A ) /\ 0s
95 94 simprbi 
 |-  ( xL e. { x e. ( _Left ` A ) | 0s  0s
96 83 95 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  0s
97 96 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL =/= 0s )
98 breq2 
 |-  ( xO = xL -> ( 0s  0s
99 oveq1 
 |-  ( xO = xL -> ( xO x.s y ) = ( xL x.s y ) )
100 99 eqeq1d 
 |-  ( xO = xL -> ( ( xO x.s y ) = 1s <-> ( xL x.s y ) = 1s ) )
101 100 rexbidv 
 |-  ( xO = xL -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xL x.s y ) = 1s ) )
102 98 101 imbi12d 
 |-  ( xO = xL -> ( ( 0s  E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s  E. y e. No ( xL x.s y ) = 1s ) ) )
103 69 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 ) )
104 elun1 
 |-  ( xL e. ( _Left ` A ) -> xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) )
105 84 104 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 ) ) )
106 102 103 105 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 ) )
107 96 106 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 )
108 92 85 97 107 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 )
109 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 ) )
110 108 109 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 ) )
111 110 rexlimdvva 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s  a e. No ) )
112 111 abssdv 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> { a | E. xL e. { x e. ( _Left ` A ) | 0s
113 79 112 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
114 43 113 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
115 42 114 eqsstrd 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( L ` suc j ) C_ No )
116 1 2 3 precsexlem5 
 |-  ( j e. _om -> ( R ` suc j ) = ( ( R ` j ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
117 116 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
118 simp3r 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( R ` j ) C_ No )
119 44 a1i 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  1s e. No )
120 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
121 82 120 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. ( _Left ` A ) )
122 81 121 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL e. No )
123 49 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  A e. No )
124 122 123 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 )
125 simpl3l 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  ( L ` j ) C_ No )
126 simprr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  yL e. ( L ` j ) )
127 125 126 sseldd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  yL e. No )
128 124 127 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 )
129 119 128 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 )
130 120 95 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  0s
131 130 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xL e. { x e. ( _Left ` A ) | 0s  xL =/= 0s )
132 69 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 ) )
133 121 104 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 ) ) )
134 102 132 133 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 ) )
135 130 134 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 )
136 129 122 131 135 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 )
137 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 ) )
138 136 137 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 ) )
139 138 rexlimdvva 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s  a e. No ) )
140 139 abssdv 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> { a | E. xL e. { x e. ( _Left ` A ) | 0s
141 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 )
142 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 ) )
143 46 142 sselid 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> xR e. No )
144 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 )
145 143 144 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 )
146 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 )
147 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 ) )
148 146 147 sseldd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> yR e. No )
149 145 148 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 )
150 141 149 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 )
151 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 )
152 58 adantr 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> 0s
153 142 60 syl 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> A
154 151 144 143 152 153 slttrd 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> 0s
155 154 sgt0ne0d 
 |-  ( ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) /\ ( xR e. ( _Right ` A ) /\ yR e. ( R ` j ) ) ) -> xR =/= 0s )
156 69 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 ) )
157 142 71 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 ) ) )
158 68 156 157 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 ) )
159 154 158 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 )
160 150 143 155 159 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 )
161 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 ) )
162 160 161 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 ) )
163 162 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 ) )
164 163 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 )
165 140 164 unssd 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
166 118 165 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
167 117 166 eqsstrd 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( R ` suc j ) C_ No )
168 115 167 jca 
 |-  ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( ( L ` suc j ) C_ No /\ ( R ` suc j ) C_ No ) )
169 168 3exp 
 |-  ( ph -> ( j e. _om -> ( ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) -> ( ( L ` suc j ) C_ No /\ ( R ` suc j ) C_ No ) ) ) )
170 169 com12 
 |-  ( j e. _om -> ( ph -> ( ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) -> ( ( L ` suc j ) C_ No /\ ( R ` suc j ) C_ No ) ) ) )
171 170 a2d 
 |-  ( j e. _om -> ( ( ph -> ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> ( ph -> ( ( L ` suc j ) C_ No /\ ( R ` suc j ) C_ No ) ) ) )
172 12 18 24 30 40 171 finds 
 |-  ( I e. _om -> ( ph -> ( ( L ` I ) C_ No /\ ( R ` I ) C_ No ) ) )
173 172 impcom 
 |-  ( ( ph /\ I e. _om ) -> ( ( L ` I ) C_ No /\ ( R ` I ) C_ No ) )