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	No typesetting found for |- ( ph -> 0s
	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	Could not format ( ph -> 0s 0s
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	Could not format ( L ` (/) ) = { 0s } : No typesetting found for |- ( L ` (/) ) = { 0s } with typecode |-
32		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
33		snssi	Could not format ( 0s e. No -> { 0s } C_ No ) : No typesetting found for |- ( 0s e. No -> { 0s } C_ No ) with typecode |-
34	32 33	ax-mp	Could not format { 0s } C_ No : No typesetting found for |- { 0s } C_ No with typecode |-
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	Could not format 1s e. No : No typesetting found for |- 1s e. No with typecode |-
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	Could not format ( _Right ` A ) C_ No : No typesetting found for |- ( _Right ` A ) C_ No with typecode |-
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	Could not format ( ( ph /\ j e. _om /\ ( ( L ` j ) C_ No /\ ( R ` j ) C_ No ) ) -> 0s 0s
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		breq2	Could not format ( xO = xR -> ( A A ( A A
61		rightval	Could not format ( _Right ` A ) = { xO e. ( _Old ` ( bday ` A ) ) | A
62	60 61	elrab2	Could not format ( xR e. ( _Right ` A ) <-> ( xR e. ( _Old ` ( bday ` A ) ) /\ A ( xR e. ( _Old ` ( bday ` A ) ) /\ A
63	62	simprbi	Could not format ( xR e. ( _Right ` A ) -> A A
64	47 63	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
65	57 50 48 59 64	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
66	65	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 |-
67		breq2	Could not format ( xO = xR -> ( 0s 0s ( 0s 0s
68		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 |-
69	68	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 |-
70	69	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 |-
71	67 70	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 |-
72	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 |-
73	72	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 |-
74		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 |-
75	47 74	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 |-
76	71 73 75	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 |-
77	65 76	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 |-
78	56 48 66 77	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 |-
79		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 |-
80	78 79	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 |-
81	80	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 |-
82	81	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 |-
83	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 |-
84		leftssno	Could not format ( _Left ` A ) C_ No : No typesetting found for |- ( _Left ` A ) C_ No with typecode |-
85		ssrab2	Could not format { x e. ( _Left ` A ) | 0s
86		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
87	85 86	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 |-
88	84 87	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 |-
89	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 |-
90	88 89	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 |-
91		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 |-
92		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 |-
93	91 92	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 |-
94	90 93	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 |-
95	83 94	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 |-
96		breq2	Could not format ( x = xL -> ( 0s 0s ( 0s 0s
97	96	elrab	Could not format ( xL e. { x e. ( _Left ` A ) | 0s ( xL e. ( _Left ` A ) /\ 0s ( xL e. ( _Left ` A ) /\ 0s
98	97	simprbi	Could not format ( xL e. { x e. ( _Left ` A ) | 0s 0s 0s
99	86 98	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
100	99	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 |-
101		breq2	Could not format ( xO = xL -> ( 0s 0s ( 0s 0s
102		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 |-
103	102	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 |-
104	103	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 |-
105	101 104	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 |-
106	72	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 |-
107		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 |-
108	87 107	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 |-
109	105 106 108	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 |-
110	99 109	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 |-
111	95 88 100 110	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 |-
112		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 |-
113	111 112	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 |-
114	113	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 |-
115	114	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
116	82 115	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
117	43 116	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
118	42 117	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}$$
119	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
120	119	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
121		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}$$
122	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 |-
123		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
124	85 123	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 |-
125	84 124	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 |-
126	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 |-
127	125 126	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 |-
128		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 |-
129		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 |-
130	128 129	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 |-
131	127 130	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 |-
132	122 131	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 |-
133	123 98	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
134	133	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 |-
135	72	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 |-
136	124 107	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 |-
137	105 135 136	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 |-
138	133 137	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 |-
139	132 125 134 138	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 |-
140		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 |-
141	139 140	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 |-
142	141	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 |-
143	142	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
144	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 |-
145		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 |-
146	46 145	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 |-
147	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 |-
148	146 147	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 |-
149		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 |-
150		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 |-
151	149 150	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 |-
152	148 151	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 |-
153	144 152	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 |-
154	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 |-
155	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
156	145 63	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
157	154 147 146 155 156	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
158	157	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 |-
159	72	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 |-
160	145 74	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 |-
161	71 159 160	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 |-
162	157 161	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 |-
163	153 146 158 162	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 |-
164		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 |-
165	163 164	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 |-
166	165	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 |-
167	166	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 |-
168	143 167	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
169	121 168	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
170	120 169	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}$$
171	118 170	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)$$
172	171	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)$$
173	172	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)$$
174	173	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)$$
175	12 18 24 30 40 174	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)$$
176	175	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)$$