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	No typesetting found for |- 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 } , (/) >. ) with typecode |-
	precsexlem.2	$$⊢L=1^{st}\circ F$$
	precsexlem.3	$$⊢R=2^{nd}\circ F$$
	precsexlem.4	$$⊢\phi \to A\in \mathrm{No}$$
	precsexlem.5	$$⊢\phi \to 0_s{<}_{s}A$$
	precsexlem.6	No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) with typecode |-
Assertion	precsexlem8	$$⊢\left(\phi \wedge I\in \mathrm{\omega }\right)\to \left(L\left(I\right)\subseteq \mathrm{No}\wedge R\left(I\right)\subseteq \mathrm{No}\right)$$

Proof

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