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		0sno	$$⊢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		1sno	$$⊢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		rightssno	$$⊢R\left(A\right)\subseteq \mathrm{No}$$
47		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 |-
48	46 47	sselid	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 |-
49	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}$$
50	49	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 |-
51	48 50	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 |-
52		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 |-
53		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 |-
54	52 53	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 |-
55	51 54	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 |-
56	45 55	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 |-
57	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 |-
58	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$$
59	58	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
60		rightgt	Could not format ( xR e. ( _Right ` A ) -> A A
61	47 60	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
62	57 50 48 59 61	slttrd	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
63	62	sgt0ne0d	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 |-
64		breq2	Could not format ( xO = xR -> ( 0s 0s ( 0s 0s
65		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 |-
66	65	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 |-
67	66	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 |-
68	64 67	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 |-
69	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 |-
70	69	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 |-
71		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 |-
72	47 71	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 |-
73	68 70 72	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 |-
74	62 73	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 |-
75	56 48 63 74	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 |-
76		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 |-
77	75 76	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 |-
78	77	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 |-
79	78	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 |-
80	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 |-
81		leftssno	$$⊢L\left(A\right)\subseteq \mathrm{No}$$
82		ssrab2	$$⊢\left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\subseteq L\left(A\right)$$
83		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
84	82 83	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 |-
85	81 84	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. 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 |-
86	49	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 |-
87	85 86	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 |-
88		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 |-
89		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 |-
90	88 89	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 |-
91	87 90	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 |-
92	80 91	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 |-
93		breq2	Could not format ( x = xL -> ( 0s 0s ( 0s 0s
94	93	elrab	Could not format ( xL e. { x e. ( _Left ` A ) | 0s ( xL e. ( _Left ` A ) /\ 0s ( xL e. ( _Left ` A ) /\ 0s
95	94	simprbi	Could not format ( xL e. { x e. ( _Left ` A ) | 0s 0s 0s
96	83 95	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
97	96	sgt0ne0d	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 |-
98		breq2	Could not format ( xO = xL -> ( 0s 0s ( 0s 0s
99		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 |-
100	99	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 |-
101	100	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 |-
102	98 101	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 |-
103	69	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 |-
104		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 |-
105	84 104	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 |-
106	102 103 105	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 |-
107	96 106	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 |-
108	92 85 97 107	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 |-
109		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 |-
110	108 109	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 |-
111	110	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 |-
112	111	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
113	79 112	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
114	43 113	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
115	42 114	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}$$
116	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
117	116	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
118		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}$$
119	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 |-
120		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
121	82 120	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 |-
122	81 121	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. 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 |-
123	49	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 |-
124	122 123	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 |-
125		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 |-
126		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 |-
127	125 126	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 |-
128	124 127	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 |-
129	119 128	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 |-
130	120 95	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
131	130	sgt0ne0d	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 |-
132	69	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 |-
133	121 104	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 |-
134	102 132 133	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 |-
135	130 134	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 |-
136	129 122 131 135	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 |-
137		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 |-
138	136 137	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 |-
139	138	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 |-
140	139	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
141	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 |-
142		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 |-
143	46 142	sselid	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 |-
144	49	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 |-
145	143 144	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 |-
146		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 |-
147		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 |-
148	146 147	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 |-
149	145 148	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 |-
150	141 149	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 |-
151	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 |-
152	58	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
153	142 60	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
154	151 144 143 152 153	slttrd	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
155	154	sgt0ne0d	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 |-
156	69	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 |-
157	142 71	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 |-
158	68 156 157	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 |-
159	154 158	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 |-
160	150 143 155 159	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 |-
161		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 |-
162	160 161	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 |-
163	162	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 |-
164	163	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 |-
165	140 164	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
166	118 165	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
167	117 166	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}$$
168	115 167	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)$$
169	168	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)$$
170	169	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)$$
171	170	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)$$
172	12 18 24 30 40 171	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)$$
173	172	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)$$