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