Theorem precsexlem11

Description: Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for A . (Contributed by Scott Fenton, 15-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 |-
	precsexlem.7	$$⊢Y=\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]$$
Assertion	precsexlem11	$$⊢\phi \to A{\cdot }_{s}Y=1_s$$

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		precsexlem.7	$$⊢Y=\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]$$
8		lltropt	$$⊢L\left(A\right){\ll }_{s}R\left(A\right)$$
9	4 5	0elleft	$$⊢\phi \to 0_s\in L\left(A\right)$$
10	9	snssd	$$⊢\phi \to \left\{0_s\right\}\subseteq L\left(A\right)$$
11		ssrab2	$$⊢\left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\subseteq L\left(A\right)$$
12	11	a1i	$$⊢\phi \to \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\subseteq L\left(A\right)$$
13	10 12	unssd	$$⊢\phi \to \left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\subseteq L\left(A\right)$$
14		sssslt1	$$⊢\left(L\left(A\right){\ll }_{s}R\left(A\right)\wedge \left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\subseteq L\left(A\right)\right)\to \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right){\ll }_{s}R\left(A\right)$$
15	8 13 14	sylancr	$$⊢\phi \to \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right){\ll }_{s}R\left(A\right)$$
16	1 2 3 4 5 6	precsexlem10	$$⊢\phi \to \bigcup L\left[\mathrm{\omega }\right]{\ll }_s\bigcup R\left[\mathrm{\omega }\right]$$
17	4 5	cutpos	$$⊢\phi \to A=\left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right){|}_{s}R\left(A\right)$$
18	7	a1i	$$⊢\phi \to Y=\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]$$
19	15 16 17 18	mulsunif	$$⊢\phi \to A{\cdot }_{s}Y=\left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right){|}_s\left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)$$
20		0sno	$$⊢0_s\in \mathrm{No}$$
21	20	elexi	$$⊢0_s\in \mathrm{V}$$
22	21	snid	$$⊢0_s\in \left\{0_s\right\}$$
23		elun1	$$⊢0_s\in \left\{0_s\right\}\to 0_s\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)$$
24	22 23	ax-mp	$$⊢0_s\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)$$
25		peano1	$$⊢\varnothing \in \mathrm{\omega }$$
26	1 2 3	precsexlem1	$$⊢L\left(\varnothing \right)=\left\{0_s\right\}$$
27	22 26	eleqtrri	$$⊢0_s\in L\left(\varnothing \right)$$
28		fveq2	$$⊢b=\varnothing \to L\left(b\right)=L\left(\varnothing \right)$$
29	28	eleq2d	$$⊢b=\varnothing \to \left(0_s\in L\left(b\right)\leftrightarrow 0_s\in L\left(\varnothing \right)\right)$$
30	29	rspcev	$$⊢\left(\varnothing \in \mathrm{\omega }\wedge 0_s\in L\left(\varnothing \right)\right)\to \exists b\in \mathrm{\omega }{0}_s\in L\left(b\right)$$
31	25 27 30	mp2an	$$⊢\exists b\in \mathrm{\omega }{0}_s\in L\left(b\right)$$
32		eliun	$$⊢0_s\in \bigcup _{b\in \mathrm{\omega }}L\left(b\right)\leftrightarrow \exists b\in \mathrm{\omega }{0}_s\in L\left(b\right)$$
33	31 32	mpbir	$$⊢0_s\in \bigcup _{b\in \mathrm{\omega }}L\left(b\right)$$
34		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
35		fofun	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to \mathrm{Fun}{1}^{st}$$
36	34 35	ax-mp	$$⊢\mathrm{Fun}{1}^{st}$$
37		rdgfun	Could not format Fun 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 |- Fun 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 |-
38	1	funeqi	Could not format ( Fun F <-> Fun 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 |- ( Fun F <-> Fun 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 |-
39	37 38	mpbir	$$⊢\mathrm{Fun}F$$
40		funco	$$⊢\left(\mathrm{Fun}{1}^{st}\wedge \mathrm{Fun}F\right)\to \mathrm{Fun}\left(1^{st}\circ F\right)$$
41	36 39 40	mp2an	$$⊢\mathrm{Fun}\left(1^{st}\circ F\right)$$
42	2	funeqi	$$⊢\mathrm{Fun}L\leftrightarrow \mathrm{Fun}\left(1^{st}\circ F\right)$$
43	41 42	mpbir	$$⊢\mathrm{Fun}L$$
44		funiunfv	$$⊢\mathrm{Fun}L\to \bigcup _{b\in \mathrm{\omega }}L\left(b\right)=\bigcup L\left[\mathrm{\omega }\right]$$
45	43 44	ax-mp	$$⊢\bigcup _{b\in \mathrm{\omega }}L\left(b\right)=\bigcup L\left[\mathrm{\omega }\right]$$
46	33 45	eleqtri	$$⊢0_s\in \bigcup L\left[\mathrm{\omega }\right]$$
47		addsrid	$$⊢0_s\in \mathrm{No}\to 0_s{+}_s{0}_s=0_s$$
48	20 47	ax-mp	$$⊢0_s{+}_s{0}_s=0_s$$
49		muls01	$$⊢0_s\in \mathrm{No}\to 0_s{\cdot }_s{0}_s=0_s$$
50	20 49	ax-mp	$$⊢0_s{\cdot }_s{0}_s=0_s$$
51	48 50	oveq12i	$$⊢\left(0_s{+}_s{0}_s\right){-}_s\left(0_s{\cdot }_s{0}_s\right)=0_s{-}_s{0}_s$$
52		subsid	$$⊢0_s\in \mathrm{No}\to 0_s{-}_s{0}_s=0_s$$
53	20 52	ax-mp	$$⊢0_s{-}_s{0}_s=0_s$$
54	51 53	eqtr2i	$$⊢0_s=\left(0_s{+}_s{0}_s\right){-}_s\left(0_s{\cdot }_s{0}_s\right)$$
55	16	scutcld	$$⊢\phi \to \bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\in \mathrm{No}$$
56	7 55	eqeltrid	$$⊢\phi \to Y\in \mathrm{No}$$
57		muls02	$$⊢Y\in \mathrm{No}\to 0_s{\cdot }_{s}Y=0_s$$
58	56 57	syl	$$⊢\phi \to 0_s{\cdot }_{s}Y=0_s$$
59		muls01	$$⊢A\in \mathrm{No}\to A{\cdot }_s{0}_s=0_s$$
60	4 59	syl	$$⊢\phi \to A{\cdot }_s{0}_s=0_s$$
61	58 60	oveq12d	$$⊢\phi \to \left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_s{0}_s\right)=0_s{+}_s{0}_s$$
62	61	oveq1d	$$⊢\phi \to \left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_s{0}_s\right)\right){-}_s\left(0_s{\cdot }_s{0}_s\right)=\left(0_s{+}_s{0}_s\right){-}_s\left(0_s{\cdot }_s{0}_s\right)$$
63	54 62	eqtr4id	$$⊢\phi \to 0_s=\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_s{0}_s\right)\right){-}_s\left(0_s{\cdot }_s{0}_s\right)$$
64		oveq1	$$⊢c=0_s\to c{\cdot }_{s}Y=0_s{\cdot }_{s}Y$$
65	64	oveq1d	$$⊢c=0_s\to \left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)=\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)$$
66		oveq1	$$⊢c=0_s\to c{\cdot }_{s}d=0_s{\cdot }_{s}d$$
67	65 66	oveq12d	$$⊢c=0_s\to \left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)=\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)$$
68	67	eqeq2d	$$⊢c=0_s\to \left(0_s=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\leftrightarrow 0_s=\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)\right)$$
69		oveq2	$$⊢d=0_s\to A{\cdot }_{s}d=A{\cdot }_s{0}_s$$
70	69	oveq2d	$$⊢d=0_s\to \left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)=\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_s{0}_s\right)$$
71		oveq2	$$⊢d=0_s\to 0_s{\cdot }_{s}d=0_s{\cdot }_s{0}_s$$
72	70 71	oveq12d	$$⊢d=0_s\to \left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)=\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_s{0}_s\right)\right){-}_s\left(0_s{\cdot }_s{0}_s\right)$$
73	72	eqeq2d	$$⊢d=0_s\to \left(0_s=\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)\leftrightarrow 0_s=\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_s{0}_s\right)\right){-}_s\left(0_s{\cdot }_s{0}_s\right)\right)$$
74	68 73	rspc2ev	$$⊢\left(0_s\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge 0_s\in \bigcup L\left[\mathrm{\omega }\right]\wedge 0_s=\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_s{0}_s\right)\right){-}_s\left(0_s{\cdot }_s{0}_s\right)\right)\to \exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]0_s=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)$$
75	24 46 63 74	mp3an12i	$$⊢\phi \to \exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]0_s=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)$$
76		eqeq1	$$⊢b=0_s\to \left(b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\leftrightarrow 0_s=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
77	76	2rexbidv	$$⊢b=0_s\to \left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\leftrightarrow \exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]0_s=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
78	21 77	elab	$$⊢0_s\in \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\leftrightarrow \exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]0_s=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)$$
79	75 78	sylibr	$$⊢\phi \to 0_s\in \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}$$
80		elun1	$$⊢0_s\in \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\to 0_s\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)$$
81	79 80	syl	$$⊢\phi \to 0_s\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)$$
82		eqid	$$⊢\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)=\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
83	82	rnmpo	$$⊢\mathrm{ran}\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)=\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}$$
84		ssltex1	$$⊢\left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right){\ll }_{s}R\left(A\right)\to \left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\in \mathrm{V}$$
85	15 84	syl	$$⊢\phi \to \left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\in \mathrm{V}$$
86		ssltex1	$$⊢\bigcup L\left[\mathrm{\omega }\right]{\ll }_s\bigcup R\left[\mathrm{\omega }\right]\to \bigcup L\left[\mathrm{\omega }\right]\in \mathrm{V}$$
87	16 86	syl	$$⊢\phi \to \bigcup L\left[\mathrm{\omega }\right]\in \mathrm{V}$$
88		mpoexga	$$⊢\left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\in \mathrm{V}\wedge \bigcup L\left[\mathrm{\omega }\right]\in \mathrm{V}\right)\to \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
89	85 87 88	syl2anc	$$⊢\phi \to \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
90		rnexg	$$⊢\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}\to \mathrm{ran}\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
91	89 90	syl	$$⊢\phi \to \mathrm{ran}\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
92	83 91	eqeltrrid	$$⊢\phi \to \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\in \mathrm{V}$$
93		eqid	$$⊢\left(c\in R\left(A\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)=\left(c\in R\left(A\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
94	93	rnmpo	$$⊢\mathrm{ran}\left(c\in R\left(A\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)=\left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}$$
95		fvex	$$⊢R\left(A\right)\in \mathrm{V}$$
96		ssltex2	$$⊢\bigcup L\left[\mathrm{\omega }\right]{\ll }_s\bigcup R\left[\mathrm{\omega }\right]\to \bigcup R\left[\mathrm{\omega }\right]\in \mathrm{V}$$
97	16 96	syl	$$⊢\phi \to \bigcup R\left[\mathrm{\omega }\right]\in \mathrm{V}$$
98		mpoexga	$$⊢\left(R\left(A\right)\in \mathrm{V}\wedge \bigcup R\left[\mathrm{\omega }\right]\in \mathrm{V}\right)\to \left(c\in R\left(A\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
99	95 97 98	sylancr	$$⊢\phi \to \left(c\in R\left(A\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
100		rnexg	$$⊢\left(c\in R\left(A\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}\to \mathrm{ran}\left(c\in R\left(A\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
101	99 100	syl	$$⊢\phi \to \mathrm{ran}\left(c\in R\left(A\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
102	94 101	eqeltrrid	$$⊢\phi \to \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\in \mathrm{V}$$
103	92 102	unexd	$$⊢\phi \to \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\in \mathrm{V}$$
104		snex	$$⊢\left\{1_s\right\}\in \mathrm{V}$$
105	104	a1i	$$⊢\phi \to \left\{1_s\right\}\in \mathrm{V}$$
106		ssltss1	$$⊢\left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right){\ll }_{s}R\left(A\right)\to \left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\subseteq \mathrm{No}$$
107	15 106	syl	$$⊢\phi \to \left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\subseteq \mathrm{No}$$
108	107	sselda	$$⊢\left(\phi \wedge c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\right)\to c\in \mathrm{No}$$
109	108	adantrr	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to c\in \mathrm{No}$$
110	56	adantr	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to Y\in \mathrm{No}$$
111	109 110	mulscld	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}Y\in \mathrm{No}$$
112	4	adantr	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to A\in \mathrm{No}$$
113		ssltss1	$$⊢\bigcup L\left[\mathrm{\omega }\right]{\ll }_s\bigcup R\left[\mathrm{\omega }\right]\to \bigcup L\left[\mathrm{\omega }\right]\subseteq \mathrm{No}$$
114	16 113	syl	$$⊢\phi \to \bigcup L\left[\mathrm{\omega }\right]\subseteq \mathrm{No}$$
115	114	sselda	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to d\in \mathrm{No}$$
116	115	adantrl	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to d\in \mathrm{No}$$
117	112 116	mulscld	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to A{\cdot }_{s}d\in \mathrm{No}$$
118	111 117	addscld	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\in \mathrm{No}$$
119	109 116	mulscld	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}d\in \mathrm{No}$$
120	118 119	subscld	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\in \mathrm{No}$$
121		eleq1	$$⊢b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to \left(b\in \mathrm{No}\leftrightarrow \left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\in \mathrm{No}\right)$$
122	120 121	syl5ibrcom	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to b\in \mathrm{No}\right)$$
123	122	rexlimdvva	$$⊢\phi \to \left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to b\in \mathrm{No}\right)$$
124	123	abssdv	$$⊢\phi \to \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\subseteq \mathrm{No}$$
125		rightssno	$$⊢R\left(A\right)\subseteq \mathrm{No}$$
126	125	a1i	$$⊢\phi \to R\left(A\right)\subseteq \mathrm{No}$$
127	126	sselda	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to c\in \mathrm{No}$$
128	127	adantrr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to c\in \mathrm{No}$$
129	56	adantr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to Y\in \mathrm{No}$$
130	128 129	mulscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}Y\in \mathrm{No}$$
131	4	adantr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to A\in \mathrm{No}$$
132		ssltss2	$$⊢\bigcup L\left[\mathrm{\omega }\right]{\ll }_s\bigcup R\left[\mathrm{\omega }\right]\to \bigcup R\left[\mathrm{\omega }\right]\subseteq \mathrm{No}$$
133	16 132	syl	$$⊢\phi \to \bigcup R\left[\mathrm{\omega }\right]\subseteq \mathrm{No}$$
134	133	sselda	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to d\in \mathrm{No}$$
135	134	adantrl	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to d\in \mathrm{No}$$
136	131 135	mulscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to A{\cdot }_{s}d\in \mathrm{No}$$
137	130 136	addscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\in \mathrm{No}$$
138	128 135	mulscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}d\in \mathrm{No}$$
139	137 138	subscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\in \mathrm{No}$$
140	139 121	syl5ibrcom	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to b\in \mathrm{No}\right)$$
141	140	rexlimdvva	$$⊢\phi \to \left(\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to b\in \mathrm{No}\right)$$
142	141	abssdv	$$⊢\phi \to \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\subseteq \mathrm{No}$$
143	124 142	unssd	$$⊢\phi \to \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\subseteq \mathrm{No}$$
144		1sno	$$⊢1_s\in \mathrm{No}$$
145		snssi	$$⊢1_s\in \mathrm{No}\to \left\{1_s\right\}\subseteq \mathrm{No}$$
146	144 145	mp1i	$$⊢\phi \to \left\{1_s\right\}\subseteq \mathrm{No}$$
147		elun	$$⊢e\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\leftrightarrow \left(e\in \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\vee e\in \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)$$
148		vex	$$⊢e\in \mathrm{V}$$
149		eqeq1	$$⊢b=e\to \left(b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\leftrightarrow e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
150	149	2rexbidv	$$⊢b=e\to \left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\leftrightarrow \exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
151	148 150	elab	$$⊢e\in \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\leftrightarrow \exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)$$
152	149	2rexbidv	$$⊢b=e\to \left(\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\leftrightarrow \exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
153	148 152	elab	$$⊢e\in \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\leftrightarrow \exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)$$
154	151 153	orbi12i	$$⊢\left(e\in \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\vee e\in \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\leftrightarrow \left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\vee \exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
155	147 154	bitri	$$⊢e\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\leftrightarrow \left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\vee \exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
156		elun	$$⊢c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\leftrightarrow \left(c\in \left\{0_s\right\}\vee c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)$$
157		velsn	$$⊢c\in \left\{0_s\right\}\leftrightarrow c=0_s$$
158	157	orbi1i	$$⊢\left(c\in \left\{0_s\right\}\vee c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\leftrightarrow \left(c=0_s\vee c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)$$
159	156 158	bitri	$$⊢c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\leftrightarrow \left(c=0_s\vee c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)$$
160	58	adantr	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to 0_s{\cdot }_{s}Y=0_s$$
161	160	oveq1d	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to \left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)=0_s{+}_s\left(A{\cdot }_{s}d\right)$$
162		muls02	$$⊢d\in \mathrm{No}\to 0_s{\cdot }_{s}d=0_s$$
163	115 162	syl	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to 0_s{\cdot }_{s}d=0_s$$
164	161 163	oveq12d	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to \left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)=\left(0_s{+}_s\left(A{\cdot }_{s}d\right)\right){-}_s{0}_s$$
165	4	adantr	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to A\in \mathrm{No}$$
166	165 115	mulscld	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to A{\cdot }_{s}d\in \mathrm{No}$$
167		addslid	$$⊢A{\cdot }_{s}d\in \mathrm{No}\to 0_s{+}_s\left(A{\cdot }_{s}d\right)=A{\cdot }_{s}d$$
168	166 167	syl	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to 0_s{+}_s\left(A{\cdot }_{s}d\right)=A{\cdot }_{s}d$$
169	168	oveq1d	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to \left(0_s{+}_s\left(A{\cdot }_{s}d\right)\right){-}_s{0}_s=\left(A{\cdot }_{s}d\right){-}_s{0}_s$$
170		subsid1	$$⊢A{\cdot }_{s}d\in \mathrm{No}\to \left(A{\cdot }_{s}d\right){-}_s{0}_s=A{\cdot }_{s}d$$
171	166 170	syl	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to \left(A{\cdot }_{s}d\right){-}_s{0}_s=A{\cdot }_{s}d$$
172	164 169 171	3eqtrd	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to \left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)=A{\cdot }_{s}d$$
173		eliun	$$⊢d\in \bigcup _{i\in \mathrm{\omega }}L\left(i\right)\leftrightarrow \exists i\in \mathrm{\omega }d\in L\left(i\right)$$
174		funiunfv	$$⊢\mathrm{Fun}L\to \bigcup _{i\in \mathrm{\omega }}L\left(i\right)=\bigcup L\left[\mathrm{\omega }\right]$$
175	43 174	ax-mp	$$⊢\bigcup _{i\in \mathrm{\omega }}L\left(i\right)=\bigcup L\left[\mathrm{\omega }\right]$$
176	175	eleq2i	$$⊢d\in \bigcup _{i\in \mathrm{\omega }}L\left(i\right)\leftrightarrow d\in \bigcup L\left[\mathrm{\omega }\right]$$
177	173 176	bitr3i	$$⊢\exists i\in \mathrm{\omega }d\in L\left(i\right)\leftrightarrow d\in \bigcup L\left[\mathrm{\omega }\right]$$
178	1 2 3 4 5 6	precsexlem9	$$⊢\left(\phi \wedge i\in \mathrm{\omega }\right)\to \left(\forall d\in L\left(i\right)\left(A{\cdot }_{s}d\right){<}_s{1}_s\wedge \forall c\in R\left(i\right)1_s{<}_s\left(A{\cdot }_{s}c\right)\right)$$
179	178	simpld	$$⊢\left(\phi \wedge i\in \mathrm{\omega }\right)\to \forall d\in L\left(i\right)\left(A{\cdot }_{s}d\right){<}_s{1}_s$$
180		rsp	$$⊢\forall d\in L\left(i\right)\left(A{\cdot }_{s}d\right){<}_s{1}_s\to \left(d\in L\left(i\right)\to \left(A{\cdot }_{s}d\right){<}_s{1}_s\right)$$
181	179 180	syl	$$⊢\left(\phi \wedge i\in \mathrm{\omega }\right)\to \left(d\in L\left(i\right)\to \left(A{\cdot }_{s}d\right){<}_s{1}_s\right)$$
182	181	rexlimdva	$$⊢\phi \to \left(\exists i\in \mathrm{\omega }d\in L\left(i\right)\to \left(A{\cdot }_{s}d\right){<}_s{1}_s\right)$$
183	177 182	biimtrrid	$$⊢\phi \to \left(d\in \bigcup L\left[\mathrm{\omega }\right]\to \left(A{\cdot }_{s}d\right){<}_s{1}_s\right)$$
184	183	imp	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to \left(A{\cdot }_{s}d\right){<}_s{1}_s$$
185	172 184	eqbrtrd	$$⊢\left(\phi \wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\to \left(\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)\right){<}_s{1}_s$$
186	185	ex	$$⊢\phi \to \left(d\in \bigcup L\left[\mathrm{\omega }\right]\to \left(\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)\right){<}_s{1}_s\right)$$
187	67	breq1d	$$⊢c=0_s\to \left(\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s\leftrightarrow \left(\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)\right){<}_s{1}_s\right)$$
188	187	imbi2d	$$⊢c=0_s\to \left(\left(d\in \bigcup L\left[\mathrm{\omega }\right]\to \left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s\right)\leftrightarrow \left(d\in \bigcup L\left[\mathrm{\omega }\right]\to \left(\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)\right){<}_s{1}_s\right)\right)$$
189	186 188	syl5ibrcom	$$⊢\phi \to \left(c=0_s\to \left(d\in \bigcup L\left[\mathrm{\omega }\right]\to \left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s\right)\right)$$
190		scutcut	$$⊢\bigcup L\left[\mathrm{\omega }\right]{\ll }_s\bigcup R\left[\mathrm{\omega }\right]\to \left(\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\in \mathrm{No}\wedge \bigcup L\left[\mathrm{\omega }\right]{\ll }_s\left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}\wedge \left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}{\ll }_s\bigcup R\left[\mathrm{\omega }\right]\right)$$
191	16 190	syl	$$⊢\phi \to \left(\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\in \mathrm{No}\wedge \bigcup L\left[\mathrm{\omega }\right]{\ll }_s\left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}\wedge \left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}{\ll }_s\bigcup R\left[\mathrm{\omega }\right]\right)$$
192	191	simp3d	$$⊢\phi \to \left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}{\ll }_s\bigcup R\left[\mathrm{\omega }\right]$$
193	192	adantr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}{\ll }_s\bigcup R\left[\mathrm{\omega }\right]$$
194		ovex	$$⊢\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\in \mathrm{V}$$
195	194	snid	$$⊢\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\in \left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}$$
196	7 195	eqeltri	$$⊢Y\in \left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}$$
197	196	a1i	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to Y\in \left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}$$
198		peano2	$$⊢i\in \mathrm{\omega }\to \mathrm{suc}i\in \mathrm{\omega }$$
199	198	ad2antrl	$$⊢\left(\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in L\left(i\right)\right)\right)\to \mathrm{suc}i\in \mathrm{\omega }$$
200		eqid	$$⊢\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c=\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c$$
201		oveq1	Could not format ( xL = c -> ( xL -s A ) = ( c -s A ) ) : No typesetting found for |- ( xL = c -> ( xL -s A ) = ( c -s A ) ) with typecode |-
202	201	oveq1d	Could not format ( xL = c -> ( ( xL -s A ) x.s yL ) = ( ( c -s A ) x.s yL ) ) : No typesetting found for |- ( xL = c -> ( ( xL -s A ) x.s yL ) = ( ( c -s A ) x.s yL ) ) with typecode |-
203	202	oveq2d	Could not format ( xL = c -> ( 1s +s ( ( xL -s A ) x.s yL ) ) = ( 1s +s ( ( c -s A ) x.s yL ) ) ) : No typesetting found for |- ( xL = c -> ( 1s +s ( ( xL -s A ) x.s yL ) ) = ( 1s +s ( ( c -s A ) x.s yL ) ) ) with typecode |-
204		id	Could not format ( xL = c -> xL = c ) : No typesetting found for |- ( xL = c -> xL = c ) with typecode |-
205	203 204	oveq12d	Could not format ( xL = c -> ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) ) : No typesetting found for |- ( xL = c -> ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) ) with typecode |-
206	205	eqeq2d	Could not format ( xL = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) ) ) : No typesetting found for |- ( xL = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) ) ) with typecode |-
207		oveq2	Could not format ( yL = d -> ( ( c -s A ) x.s yL ) = ( ( c -s A ) x.s d ) ) : No typesetting found for |- ( yL = d -> ( ( c -s A ) x.s yL ) = ( ( c -s A ) x.s d ) ) with typecode |-
208	207	oveq2d	Could not format ( yL = d -> ( 1s +s ( ( c -s A ) x.s yL ) ) = ( 1s +s ( ( c -s A ) x.s d ) ) ) : No typesetting found for |- ( yL = d -> ( 1s +s ( ( c -s A ) x.s yL ) ) = ( 1s +s ( ( c -s A ) x.s d ) ) ) with typecode |-
209	208	oveq1d	Could not format ( yL = d -> ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) : No typesetting found for |- ( yL = d -> ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) with typecode |-
210	209	eqeq2d	Could not format ( yL = d -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) ) : No typesetting found for |- ( yL = d -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) ) with typecode |-
211	206 210	rspc2ev	Could not format ( ( c e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
212	200 211	mp3an3	Could not format ( ( c e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
213	212	ad2ant2l	Could not format ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
214		ovex	$$⊢\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \mathrm{V}$$
215		eqeq1	Could not format ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) : No typesetting found for |- ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) with typecode |-
216	215	2rexbidv	Could not format ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
217	214 216	elab	Could not format ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
218	213 217	sylibr	Could not format ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s
219		elun1	Could not format ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
220		elun2	Could not format ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
221	218 219 220	3syl	Could not format ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
222	1 2 3	precsexlem5	Could not format ( i e. _om -> ( R ` suc i ) = ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( R ` suc i ) = ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
223	222	ad2antrl	Could not format ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s ( R ` suc i ) = ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( R ` suc i ) = ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
224	221 223	eleqtrrd	$$⊢\left(\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in L\left(i\right)\right)\right)\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(\mathrm{suc}i\right)$$
225		fveq2	$$⊢j=\mathrm{suc}i\to R\left(j\right)=R\left(\mathrm{suc}i\right)$$
226	225	eleq2d	$$⊢j=\mathrm{suc}i\to \left(\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(j\right)\leftrightarrow \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(\mathrm{suc}i\right)\right)$$
227	226	rspcev	$$⊢\left(\mathrm{suc}i\in \mathrm{\omega }\wedge \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(\mathrm{suc}i\right)\right)\to \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(j\right)$$
228	199 224 227	syl2anc	$$⊢\left(\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in L\left(i\right)\right)\right)\to \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(j\right)$$
229	228	rexlimdvaa	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to \left(\exists i\in \mathrm{\omega }d\in L\left(i\right)\to \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(j\right)\right)$$
230		eliun	$$⊢\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup _{j\in \mathrm{\omega }}R\left(j\right)\leftrightarrow \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(j\right)$$
231		fo2nd	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
232		fofun	$$⊢2^{nd}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to \mathrm{Fun}{2}^{nd}$$
233	231 232	ax-mp	$$⊢\mathrm{Fun}{2}^{nd}$$
234		funco	$$⊢\left(\mathrm{Fun}{2}^{nd}\wedge \mathrm{Fun}F\right)\to \mathrm{Fun}\left(2^{nd}\circ F\right)$$
235	233 39 234	mp2an	$$⊢\mathrm{Fun}\left(2^{nd}\circ F\right)$$
236	3	funeqi	$$⊢\mathrm{Fun}R\leftrightarrow \mathrm{Fun}\left(2^{nd}\circ F\right)$$
237	235 236	mpbir	$$⊢\mathrm{Fun}R$$
238		funiunfv	$$⊢\mathrm{Fun}R\to \bigcup _{j\in \mathrm{\omega }}R\left(j\right)=\bigcup R\left[\mathrm{\omega }\right]$$
239	237 238	ax-mp	$$⊢\bigcup _{j\in \mathrm{\omega }}R\left(j\right)=\bigcup R\left[\mathrm{\omega }\right]$$
240	239	eleq2i	$$⊢\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup _{j\in \mathrm{\omega }}R\left(j\right)\leftrightarrow \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup R\left[\mathrm{\omega }\right]$$
241	230 240	bitr3i	$$⊢\exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(j\right)\leftrightarrow \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup R\left[\mathrm{\omega }\right]$$
242	229 177 241	3imtr3g	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to \left(d\in \bigcup L\left[\mathrm{\omega }\right]\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup R\left[\mathrm{\omega }\right]\right)$$
243	242	impr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup R\left[\mathrm{\omega }\right]$$
244	193 197 243	ssltsepcd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to Y{<}_s\left(\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\right)$$
245	56	adantr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to Y\in \mathrm{No}$$
246	144	a1i	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to 1_s\in \mathrm{No}$$
247		leftssno	$$⊢L\left(A\right)\subseteq \mathrm{No}$$
248	11 247	sstri	$$⊢\left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\subseteq \mathrm{No}$$
249	248	sseli	$$⊢c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\to c\in \mathrm{No}$$
250	249	adantl	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to c\in \mathrm{No}$$
251	4	adantr	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to A\in \mathrm{No}$$
252	250 251	subscld	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to c{-}_{s}A\in \mathrm{No}$$
253	252	adantrr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to c{-}_{s}A\in \mathrm{No}$$
254	115	adantrl	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to d\in \mathrm{No}$$
255	253 254	mulscld	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(c{-}_{s}A\right){\cdot }_{s}d\in \mathrm{No}$$
256	246 255	addscld	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\in \mathrm{No}$$
257	249	ad2antrl	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to c\in \mathrm{No}$$
258		breq2	$$⊢x=c\to \left(0_s{<}_{s}x\leftrightarrow 0_s{<}_{s}c\right)$$
259	258	elrab	$$⊢c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\leftrightarrow \left(c\in L\left(A\right)\wedge 0_s{<}_{s}c\right)$$
260	259	simprbi	$$⊢c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\to 0_s{<}_{s}c$$
261	260	ad2antrl	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to 0_s{<}_{s}c$$
262	260	adantl	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to 0_s{<}_{s}c$$
263		breq2	Could not format ( xO = c -> ( 0s 0s ( 0s 0s
264		oveq1	Could not format ( xO = c -> ( xO x.s y ) = ( c x.s y ) ) : No typesetting found for |- ( xO = c -> ( xO x.s y ) = ( c x.s y ) ) with typecode |-
265	264	eqeq1d	Could not format ( xO = c -> ( ( xO x.s y ) = 1s <-> ( c x.s y ) = 1s ) ) : No typesetting found for |- ( xO = c -> ( ( xO x.s y ) = 1s <-> ( c x.s y ) = 1s ) ) with typecode |-
266	265	rexbidv	Could not format ( xO = c -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( c x.s y ) = 1s ) ) : No typesetting found for |- ( xO = c -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( c x.s y ) = 1s ) ) with typecode |-
267	263 266	imbi12d	Could not format ( xO = c -> ( ( 0s E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s E. y e. No ( c x.s y ) = 1s ) ) ) : No typesetting found for |- ( xO = c -> ( ( 0s E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s E. y e. No ( c x.s y ) = 1s ) ) ) with typecode |-
268	6	adantr	Could not format ( ( ph /\ c 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 /\ c 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 |-
269		ssun1	$$⊢L\left(A\right)\subseteq L\left(A\right)\cup R\left(A\right)$$
270	11 269	sstri	$$⊢\left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\subseteq L\left(A\right)\cup R\left(A\right)$$
271	270	sseli	$$⊢c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\to c\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
272	271	adantl	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to c\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
273	267 268 272	rspcdva	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to \left(0_s{<}_{s}c\to \exists y\in \mathrm{No}c{\cdot }_{s}y=1_s\right)$$
274	262 273	mpd	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to \exists y\in \mathrm{No}c{\cdot }_{s}y=1_s$$
275	274	adantrr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \exists y\in \mathrm{No}c{\cdot }_{s}y=1_s$$
276	245 256 257 261 275	sltmuldiv2wd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(c{\cdot }_{s}Y\right){<}_s\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right)\leftrightarrow Y{<}_s\left(\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\right)\right)$$
277	244 276	mpbird	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(c{\cdot }_{s}Y\right){<}_s\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right)$$
278	257 254	mulscld	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}d\in \mathrm{No}$$
279	166	adantrl	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to A{\cdot }_{s}d\in \mathrm{No}$$
280	246 278 279	addsubsassd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)\right)$$
281	4	adantr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to A\in \mathrm{No}$$
282	257 281 254	subsdird	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(c{-}_{s}A\right){\cdot }_{s}d=\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)$$
283	282	oveq2d	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)\right)$$
284	280 283	eqtr4d	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)$$
285	277 284	breqtrrd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(c{\cdot }_{s}Y\right){<}_s\left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right)$$
286	56	adantr	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to Y\in \mathrm{No}$$
287	250 286	mulscld	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to c{\cdot }_{s}Y\in \mathrm{No}$$
288	287	adantrr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}Y\in \mathrm{No}$$
289	288 279	addscld	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\in \mathrm{No}$$
290	289 278 246	sltsubaddd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s\leftrightarrow \left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){<}_s\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right)\right)$$
291	246 278	addscld	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(c{\cdot }_{s}d\right)\in \mathrm{No}$$
292	288 279 291	sltaddsubd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){<}_s\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right)\leftrightarrow \left(c{\cdot }_{s}Y\right){<}_s\left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right)\right)$$
293	290 292	bitrd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s\leftrightarrow \left(c{\cdot }_{s}Y\right){<}_s\left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right)\right)$$
294	285 293	mpbird	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s$$
295	294	exp32	$$⊢\phi \to \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\to \left(d\in \bigcup L\left[\mathrm{\omega }\right]\to \left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s\right)\right)$$
296	189 295	jaod	$$⊢\phi \to \left(\left(c=0_s\vee c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to \left(d\in \bigcup L\left[\mathrm{\omega }\right]\to \left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s\right)\right)$$
297	159 296	biimtrid	$$⊢\phi \to \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to \left(d\in \bigcup L\left[\mathrm{\omega }\right]\to \left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s\right)\right)$$
298	297	imp32	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s$$
299		breq1	$$⊢e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to \left(e{<}_s{1}_s\leftrightarrow \left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s\right)$$
300	298 299	syl5ibrcom	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to e{<}_s{1}_s\right)$$
301	300	rexlimdvva	$$⊢\phi \to \left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to e{<}_s{1}_s\right)$$
302	192	adantr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}{\ll }_s\bigcup R\left[\mathrm{\omega }\right]$$
303	196	a1i	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to Y\in \left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}$$
304	198	ad2antrl	$$⊢\left(\left(\phi \wedge c\in R\left(A\right)\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in R\left(i\right)\right)\right)\to \mathrm{suc}i\in \mathrm{\omega }$$
305		oveq1	Could not format ( xR = c -> ( xR -s A ) = ( c -s A ) ) : No typesetting found for |- ( xR = c -> ( xR -s A ) = ( c -s A ) ) with typecode |-
306	305	oveq1d	Could not format ( xR = c -> ( ( xR -s A ) x.s yR ) = ( ( c -s A ) x.s yR ) ) : No typesetting found for |- ( xR = c -> ( ( xR -s A ) x.s yR ) = ( ( c -s A ) x.s yR ) ) with typecode |-
307	306	oveq2d	Could not format ( xR = c -> ( 1s +s ( ( xR -s A ) x.s yR ) ) = ( 1s +s ( ( c -s A ) x.s yR ) ) ) : No typesetting found for |- ( xR = c -> ( 1s +s ( ( xR -s A ) x.s yR ) ) = ( 1s +s ( ( c -s A ) x.s yR ) ) ) with typecode |-
308		id	Could not format ( xR = c -> xR = c ) : No typesetting found for |- ( xR = c -> xR = c ) with typecode |-
309	307 308	oveq12d	Could not format ( xR = c -> ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) ) : No typesetting found for |- ( xR = c -> ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) ) with typecode |-
310	309	eqeq2d	Could not format ( xR = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) ) ) : No typesetting found for |- ( xR = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) ) ) with typecode |-
311		oveq2	Could not format ( yR = d -> ( ( c -s A ) x.s yR ) = ( ( c -s A ) x.s d ) ) : No typesetting found for |- ( yR = d -> ( ( c -s A ) x.s yR ) = ( ( c -s A ) x.s d ) ) with typecode |-
312	311	oveq2d	Could not format ( yR = d -> ( 1s +s ( ( c -s A ) x.s yR ) ) = ( 1s +s ( ( c -s A ) x.s d ) ) ) : No typesetting found for |- ( yR = d -> ( 1s +s ( ( c -s A ) x.s yR ) ) = ( 1s +s ( ( c -s A ) x.s d ) ) ) with typecode |-
313	312	oveq1d	Could not format ( yR = d -> ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) : No typesetting found for |- ( yR = d -> ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) with typecode |-
314	313	eqeq2d	Could not format ( yR = d -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) ) : No typesetting found for |- ( yR = d -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) ) with typecode |-
315	310 314	rspc2ev	Could not format ( ( c e. ( _Right ` A ) /\ d e. ( R ` i ) /\ ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) -> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) : No typesetting found for |- ( ( c e. ( _Right ` A ) /\ d e. ( R ` i ) /\ ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) -> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) with typecode |-
316	200 315	mp3an3	Could not format ( ( c e. ( _Right ` A ) /\ d e. ( R ` i ) ) -> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) : No typesetting found for |- ( ( c e. ( _Right ` A ) /\ d e. ( R ` i ) ) -> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) with typecode |-
317	316	ad2ant2l	Could not format ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) : No typesetting found for |- ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) with typecode |-
318		eqeq1	Could not format ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for |- ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode |-
319	318	2rexbidv	Could not format ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for |- ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode |-
320	214 319	elab	Could not format ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) : No typesetting found for |- ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) with typecode |-
321	317 320	sylibr	Could not format ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } ) : No typesetting found for |- ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } ) with typecode |-
322		elun2	Could not format ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yR e. ( R ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
323	321 322 220	3syl	Could not format ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
324	222	ad2antrl	Could not format ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( R ` i ) ) ) -> ( R ` suc i ) = ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s ( R ` suc i ) = ( ( R ` i ) u. ( { a | E. xL e. { x e. ( _Left ` A ) | 0s
325	323 324	eleqtrrd	$$⊢\left(\left(\phi \wedge c\in R\left(A\right)\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in R\left(i\right)\right)\right)\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(\mathrm{suc}i\right)$$
326	304 325 227	syl2anc	$$⊢\left(\left(\phi \wedge c\in R\left(A\right)\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in R\left(i\right)\right)\right)\to \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(j\right)$$
327	326	rexlimdvaa	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to \left(\exists i\in \mathrm{\omega }d\in R\left(i\right)\to \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in R\left(j\right)\right)$$
328		eliun	$$⊢d\in \bigcup _{i\in \mathrm{\omega }}R\left(i\right)\leftrightarrow \exists i\in \mathrm{\omega }d\in R\left(i\right)$$
329		funiunfv	$$⊢\mathrm{Fun}R\to \bigcup _{i\in \mathrm{\omega }}R\left(i\right)=\bigcup R\left[\mathrm{\omega }\right]$$
330	237 329	ax-mp	$$⊢\bigcup _{i\in \mathrm{\omega }}R\left(i\right)=\bigcup R\left[\mathrm{\omega }\right]$$
331	330	eleq2i	$$⊢d\in \bigcup _{i\in \mathrm{\omega }}R\left(i\right)\leftrightarrow d\in \bigcup R\left[\mathrm{\omega }\right]$$
332	328 331	bitr3i	$$⊢\exists i\in \mathrm{\omega }d\in R\left(i\right)\leftrightarrow d\in \bigcup R\left[\mathrm{\omega }\right]$$
333	327 332 241	3imtr3g	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to \left(d\in \bigcup R\left[\mathrm{\omega }\right]\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup R\left[\mathrm{\omega }\right]\right)$$
334	333	impr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup R\left[\mathrm{\omega }\right]$$
335	302 303 334	ssltsepcd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to Y{<}_s\left(\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\right)$$
336	144	a1i	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 1_s\in \mathrm{No}$$
337	4	adantr	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to A\in \mathrm{No}$$
338	127 337	subscld	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to c{-}_{s}A\in \mathrm{No}$$
339	338	adantrr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to c{-}_{s}A\in \mathrm{No}$$
340	339 135	mulscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(c{-}_{s}A\right){\cdot }_{s}d\in \mathrm{No}$$
341	336 340	addscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\in \mathrm{No}$$
342	20	a1i	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to 0_s\in \mathrm{No}$$
343	5	adantr	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to 0_s{<}_{s}A$$
344		rightgt	$$⊢c\in R\left(A\right)\to A{<}_{s}c$$
345	344	adantl	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to A{<}_{s}c$$
346	342 337 127 343 345	slttrd	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to 0_s{<}_{s}c$$
347	346	adantrr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 0_s{<}_{s}c$$
348	6	adantr	Could not format ( ( ph /\ c e. ( _Right ` A ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) : No typesetting found for |- ( ( ph /\ c e. ( _Right ` A ) ) -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) with typecode |-
349		elun2	$$⊢c\in R\left(A\right)\to c\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
350	349	adantl	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to c\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
351	267 348 350	rspcdva	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to \left(0_s{<}_{s}c\to \exists y\in \mathrm{No}c{\cdot }_{s}y=1_s\right)$$
352	346 351	mpd	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to \exists y\in \mathrm{No}c{\cdot }_{s}y=1_s$$
353	352	adantrr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \exists y\in \mathrm{No}c{\cdot }_{s}y=1_s$$
354	129 341 128 347 353	sltmuldiv2wd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(c{\cdot }_{s}Y\right){<}_s\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right)\leftrightarrow Y{<}_s\left(\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\right)\right)$$
355	335 354	mpbird	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(c{\cdot }_{s}Y\right){<}_s\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right)$$
356	336 138 136	addsubsassd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)\right)$$
357	128 131 135	subsdird	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(c{-}_{s}A\right){\cdot }_{s}d=\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)$$
358	357	oveq2d	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)\right)$$
359	356 358	eqtr4d	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)$$
360	355 359	breqtrrd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(c{\cdot }_{s}Y\right){<}_s\left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right)$$
361	137 138 336	sltsubaddd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s\leftrightarrow \left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){<}_s\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right)\right)$$
362	336 138	addscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(c{\cdot }_{s}d\right)\in \mathrm{No}$$
363	130 136 362	sltaddsubd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){<}_s\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right)\leftrightarrow \left(c{\cdot }_{s}Y\right){<}_s\left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right)\right)$$
364	361 363	bitrd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s\leftrightarrow \left(c{\cdot }_{s}Y\right){<}_s\left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right)\right)$$
365	360 364	mpbird	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right){<}_s{1}_s$$
366	365 299	syl5ibrcom	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to e{<}_s{1}_s\right)$$
367	366	rexlimdvva	$$⊢\phi \to \left(\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to e{<}_s{1}_s\right)$$
368	301 367	jaod	$$⊢\phi \to \left(\left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\vee \exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]e=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\to e{<}_s{1}_s\right)$$
369	155 368	biimtrid	$$⊢\phi \to \left(e\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\to e{<}_s{1}_s\right)$$
370	369	imp	$$⊢\left(\phi \wedge e\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\right)\to e{<}_s{1}_s$$
371		velsn	$$⊢f\in \left\{1_s\right\}\leftrightarrow f=1_s$$
372		breq2	$$⊢f=1_s\to \left(e{<}_{s}f\leftrightarrow e{<}_s{1}_s\right)$$
373	371 372	sylbi	$$⊢f\in \left\{1_s\right\}\to \left(e{<}_{s}f\leftrightarrow e{<}_s{1}_s\right)$$
374	370 373	syl5ibrcom	$$⊢\left(\phi \wedge e\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\right)\to \left(f\in \left\{1_s\right\}\to e{<}_{s}f\right)$$
375	374	3impia	$$⊢\left(\phi \wedge e\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\wedge f\in \left\{1_s\right\}\right)\to e{<}_{s}f$$
376	103 105 143 146 375	ssltd	$$⊢\phi \to \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right){\ll }_s\left\{1_s\right\}$$
377		eqid	$$⊢\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)=\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
378	377	rnmpo	$$⊢\mathrm{ran}\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)=\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}$$
379		mpoexga	$$⊢\left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\in \mathrm{V}\wedge \bigcup R\left[\mathrm{\omega }\right]\in \mathrm{V}\right)\to \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
380	85 97 379	syl2anc	$$⊢\phi \to \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
381		rnexg	$$⊢\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}\to \mathrm{ran}\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
382	380 381	syl	$$⊢\phi \to \mathrm{ran}\left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right),d\in \bigcup R\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
383	378 382	eqeltrrid	$$⊢\phi \to \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\in \mathrm{V}$$
384		eqid	$$⊢\left(c\in R\left(A\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)=\left(c\in R\left(A\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
385	384	rnmpo	$$⊢\mathrm{ran}\left(c\in R\left(A\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)=\left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}$$
386		mpoexga	$$⊢\left(R\left(A\right)\in \mathrm{V}\wedge \bigcup L\left[\mathrm{\omega }\right]\in \mathrm{V}\right)\to \left(c\in R\left(A\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
387	95 87 386	sylancr	$$⊢\phi \to \left(c\in R\left(A\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
388		rnexg	$$⊢\left(c\in R\left(A\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}\to \mathrm{ran}\left(c\in R\left(A\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
389	387 388	syl	$$⊢\phi \to \mathrm{ran}\left(c\in R\left(A\right),d\in \bigcup L\left[\mathrm{\omega }\right]⟼\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\in \mathrm{V}$$
390	385 389	eqeltrrid	$$⊢\phi \to \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\in \mathrm{V}$$
391	383 390	unexd	$$⊢\phi \to \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\in \mathrm{V}$$
392	108	adantrr	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to c\in \mathrm{No}$$
393	56	adantr	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to Y\in \mathrm{No}$$
394	392 393	mulscld	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}Y\in \mathrm{No}$$
395	4	adantr	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to A\in \mathrm{No}$$
396	134	adantrl	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to d\in \mathrm{No}$$
397	395 396	mulscld	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to A{\cdot }_{s}d\in \mathrm{No}$$
398	394 397	addscld	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\in \mathrm{No}$$
399	392 396	mulscld	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}d\in \mathrm{No}$$
400	398 399	subscld	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\in \mathrm{No}$$
401	400 121	syl5ibrcom	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to b\in \mathrm{No}\right)$$
402	401	rexlimdvva	$$⊢\phi \to \left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to b\in \mathrm{No}\right)$$
403	402	abssdv	$$⊢\phi \to \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\subseteq \mathrm{No}$$
404	127	adantrr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to c\in \mathrm{No}$$
405	56	adantr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to Y\in \mathrm{No}$$
406	404 405	mulscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}Y\in \mathrm{No}$$
407	4	adantr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to A\in \mathrm{No}$$
408	115	adantrl	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to d\in \mathrm{No}$$
409	407 408	mulscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to A{\cdot }_{s}d\in \mathrm{No}$$
410	406 409	addscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\in \mathrm{No}$$
411	404 408	mulscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}d\in \mathrm{No}$$
412	410 411	subscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\in \mathrm{No}$$
413	412 121	syl5ibrcom	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to b\in \mathrm{No}\right)$$
414	413	rexlimdvva	$$⊢\phi \to \left(\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to b\in \mathrm{No}\right)$$
415	414	abssdv	$$⊢\phi \to \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\subseteq \mathrm{No}$$
416	403 415	unssd	$$⊢\phi \to \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\subseteq \mathrm{No}$$
417		elun	$$⊢f\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\leftrightarrow \left(f\in \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\vee f\in \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)$$
418		vex	$$⊢f\in \mathrm{V}$$
419		eqeq1	$$⊢b=f\to \left(b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\leftrightarrow f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
420	419	2rexbidv	$$⊢b=f\to \left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\leftrightarrow \exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
421	418 420	elab	$$⊢f\in \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\leftrightarrow \exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)$$
422	419	2rexbidv	$$⊢b=f\to \left(\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\leftrightarrow \exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
423	418 422	elab	$$⊢f\in \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\leftrightarrow \exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)$$
424	421 423	orbi12i	$$⊢\left(f\in \left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\vee f\in \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\leftrightarrow \left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\vee \exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
425	417 424	bitri	$$⊢f\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\leftrightarrow \left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\vee \exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
426		eliun	$$⊢d\in \bigcup _{j\in \mathrm{\omega }}R\left(j\right)\leftrightarrow \exists j\in \mathrm{\omega }d\in R\left(j\right)$$
427	239	eleq2i	$$⊢d\in \bigcup _{j\in \mathrm{\omega }}R\left(j\right)\leftrightarrow d\in \bigcup R\left[\mathrm{\omega }\right]$$
428	426 427	bitr3i	$$⊢\exists j\in \mathrm{\omega }d\in R\left(j\right)\leftrightarrow d\in \bigcup R\left[\mathrm{\omega }\right]$$
429	1 2 3 4 5 6	precsexlem9	$$⊢\left(\phi \wedge j\in \mathrm{\omega }\right)\to \left(\forall c\in L\left(j\right)\left(A{\cdot }_{s}c\right){<}_s{1}_s\wedge \forall d\in R\left(j\right)1_s{<}_s\left(A{\cdot }_{s}d\right)\right)$$
430		rsp	$$⊢\forall d\in R\left(j\right)1_s{<}_s\left(A{\cdot }_{s}d\right)\to \left(d\in R\left(j\right)\to 1_s{<}_s\left(A{\cdot }_{s}d\right)\right)$$
431	429 430	simpl2im	$$⊢\left(\phi \wedge j\in \mathrm{\omega }\right)\to \left(d\in R\left(j\right)\to 1_s{<}_s\left(A{\cdot }_{s}d\right)\right)$$
432	431	rexlimdva	$$⊢\phi \to \left(\exists j\in \mathrm{\omega }d\in R\left(j\right)\to 1_s{<}_s\left(A{\cdot }_{s}d\right)\right)$$
433	428 432	biimtrrid	$$⊢\phi \to \left(d\in \bigcup R\left[\mathrm{\omega }\right]\to 1_s{<}_s\left(A{\cdot }_{s}d\right)\right)$$
434	433	imp	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to 1_s{<}_s\left(A{\cdot }_{s}d\right)$$
435	56	adantr	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to Y\in \mathrm{No}$$
436	57	oveq1d	$$⊢Y\in \mathrm{No}\to \left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)=0_s{+}_s\left(A{\cdot }_{s}d\right)$$
437	435 436	syl	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to \left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)=0_s{+}_s\left(A{\cdot }_{s}d\right)$$
438	4	adantr	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to A\in \mathrm{No}$$
439	438 134	mulscld	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to A{\cdot }_{s}d\in \mathrm{No}$$
440	439 167	syl	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to 0_s{+}_s\left(A{\cdot }_{s}d\right)=A{\cdot }_{s}d$$
441	437 440	eqtrd	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to \left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)=A{\cdot }_{s}d$$
442	134 162	syl	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to 0_s{\cdot }_{s}d=0_s$$
443	441 442	oveq12d	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to \left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)=\left(A{\cdot }_{s}d\right){-}_s{0}_s$$
444	439 170	syl	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to \left(A{\cdot }_{s}d\right){-}_s{0}_s=A{\cdot }_{s}d$$
445	443 444	eqtrd	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to \left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)=A{\cdot }_{s}d$$
446	434 445	breqtrrd	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to 1_s{<}_s\left(\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)\right)$$
447	446	ex	$$⊢\phi \to \left(d\in \bigcup R\left[\mathrm{\omega }\right]\to 1_s{<}_s\left(\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)\right)\right)$$
448	67	breq2d	$$⊢c=0_s\to \left(1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\leftrightarrow 1_s{<}_s\left(\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)\right)\right)$$
449	448	imbi2d	$$⊢c=0_s\to \left(\left(d\in \bigcup R\left[\mathrm{\omega }\right]\to 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\right)\leftrightarrow \left(d\in \bigcup R\left[\mathrm{\omega }\right]\to 1_s{<}_s\left(\left(\left(0_s{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(0_s{\cdot }_{s}d\right)\right)\right)\right)$$
450	447 449	syl5ibrcom	$$⊢\phi \to \left(c=0_s\to \left(d\in \bigcup R\left[\mathrm{\omega }\right]\to 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\right)\right)$$
451	144	a1i	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 1_s\in \mathrm{No}$$
452	249	ad2antrl	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to c\in \mathrm{No}$$
453	134	adantrl	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to d\in \mathrm{No}$$
454	452 453	mulscld	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}d\in \mathrm{No}$$
455	439	adantrl	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to A{\cdot }_{s}d\in \mathrm{No}$$
456	451 454 455	addsubsassd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)\right)$$
457	4	adantr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to A\in \mathrm{No}$$
458	452 457 453	subsdird	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(c{-}_{s}A\right){\cdot }_{s}d=\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)$$
459	458	oveq2d	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)\right)$$
460	456 459	eqtr4d	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)$$
461	191	simp2d	$$⊢\phi \to \bigcup L\left[\mathrm{\omega }\right]{\ll }_s\left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}$$
462	461	adantr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \bigcup L\left[\mathrm{\omega }\right]{\ll }_s\left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}$$
463	198	ad2antrl	$$⊢\left(\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in R\left(i\right)\right)\right)\to \mathrm{suc}i\in \mathrm{\omega }$$
464	201	oveq1d	Could not format ( xL = c -> ( ( xL -s A ) x.s yR ) = ( ( c -s A ) x.s yR ) ) : No typesetting found for |- ( xL = c -> ( ( xL -s A ) x.s yR ) = ( ( c -s A ) x.s yR ) ) with typecode |-
465	464	oveq2d	Could not format ( xL = c -> ( 1s +s ( ( xL -s A ) x.s yR ) ) = ( 1s +s ( ( c -s A ) x.s yR ) ) ) : No typesetting found for |- ( xL = c -> ( 1s +s ( ( xL -s A ) x.s yR ) ) = ( 1s +s ( ( c -s A ) x.s yR ) ) ) with typecode |-
466	465 204	oveq12d	Could not format ( xL = c -> ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) ) : No typesetting found for |- ( xL = c -> ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) ) with typecode |-
467	466	eqeq2d	Could not format ( xL = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) ) ) : No typesetting found for |- ( xL = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yR ) ) /su c ) ) ) with typecode |-
468	467 314	rspc2ev	Could not format ( ( c e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
469	200 468	mp3an3	Could not format ( ( c e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
470	469	ad2ant2l	Could not format ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
471		eqeq1	Could not format ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) : No typesetting found for |- ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) with typecode |-
472	471	2rexbidv	Could not format ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s ( E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
473	214 472	elab	Could not format ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s E. xL e. { x e. ( _Left ` A ) | 0s
474	470 473	sylibr	Could not format ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s
475		elun2	Could not format ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
476		elun2	Could not format ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
477	474 475 476	3syl	Could not format ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
478	1 2 3	precsexlem4	Could not format ( i e. _om -> ( L ` suc i ) = ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( L ` suc i ) = ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
479	478	ad2antrl	Could not format ( ( ( ph /\ c e. { x e. ( _Left ` A ) | 0s ( L ` suc i ) = ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( L ` suc i ) = ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
480	477 479	eleqtrrd	$$⊢\left(\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in R\left(i\right)\right)\right)\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(\mathrm{suc}i\right)$$
481		fveq2	$$⊢j=\mathrm{suc}i\to L\left(j\right)=L\left(\mathrm{suc}i\right)$$
482	481	eleq2d	$$⊢j=\mathrm{suc}i\to \left(\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(j\right)\leftrightarrow \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(\mathrm{suc}i\right)\right)$$
483	482	rspcev	$$⊢\left(\mathrm{suc}i\in \mathrm{\omega }\wedge \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(\mathrm{suc}i\right)\right)\to \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(j\right)$$
484	463 480 483	syl2anc	$$⊢\left(\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in R\left(i\right)\right)\right)\to \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(j\right)$$
485	484	rexlimdvaa	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to \left(\exists i\in \mathrm{\omega }d\in R\left(i\right)\to \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(j\right)\right)$$
486		eliun	$$⊢\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup _{j\in \mathrm{\omega }}L\left(j\right)\leftrightarrow \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(j\right)$$
487		funiunfv	$$⊢\mathrm{Fun}L\to \bigcup _{j\in \mathrm{\omega }}L\left(j\right)=\bigcup L\left[\mathrm{\omega }\right]$$
488	43 487	ax-mp	$$⊢\bigcup _{j\in \mathrm{\omega }}L\left(j\right)=\bigcup L\left[\mathrm{\omega }\right]$$
489	488	eleq2i	$$⊢\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup _{j\in \mathrm{\omega }}L\left(j\right)\leftrightarrow \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup L\left[\mathrm{\omega }\right]$$
490	486 489	bitr3i	$$⊢\exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(j\right)\leftrightarrow \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup L\left[\mathrm{\omega }\right]$$
491	485 332 490	3imtr3g	$$⊢\left(\phi \wedge c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to \left(d\in \bigcup R\left[\mathrm{\omega }\right]\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup L\left[\mathrm{\omega }\right]\right)$$
492	491	impr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup L\left[\mathrm{\omega }\right]$$
493	196	a1i	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to Y\in \left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}$$
494	462 492 493	ssltsepcd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\right){<}_{s}Y$$
495	252	adantrr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to c{-}_{s}A\in \mathrm{No}$$
496	495 453	mulscld	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(c{-}_{s}A\right){\cdot }_{s}d\in \mathrm{No}$$
497	451 496	addscld	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\in \mathrm{No}$$
498	56	adantr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to Y\in \mathrm{No}$$
499	260	ad2antrl	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 0_s{<}_{s}c$$
500	274	adantrr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \exists y\in \mathrm{No}c{\cdot }_{s}y=1_s$$
501	497 498 452 499 500	sltdivmulwd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\right){<}_{s}Y\leftrightarrow \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){<}_s\left(c{\cdot }_{s}Y\right)\right)$$
502	494 501	mpbid	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){<}_s\left(c{\cdot }_{s}Y\right)$$
503	460 502	eqbrtrd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right){<}_s\left(c{\cdot }_{s}Y\right)$$
504	451 454	addscld	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(c{\cdot }_{s}d\right)\in \mathrm{No}$$
505	287	adantrr	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to c{\cdot }_{s}Y\in \mathrm{No}$$
506	504 455 505	sltsubaddd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right){<}_s\left(c{\cdot }_{s}Y\right)\leftrightarrow \left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){<}_s\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right)\right)$$
507	505 455	addscld	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\in \mathrm{No}$$
508	451 454 507	sltaddsubd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){<}_s\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right)\leftrightarrow 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\right)$$
509	506 508	bitrd	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right){<}_s\left(c{\cdot }_{s}Y\right)\leftrightarrow 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\right)$$
510	503 509	mpbid	$$⊢\left(\phi \wedge \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
511	510	exp32	$$⊢\phi \to \left(c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\to \left(d\in \bigcup R\left[\mathrm{\omega }\right]\to 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\right)\right)$$
512	450 511	jaod	$$⊢\phi \to \left(\left(c=0_s\vee c\in \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to \left(d\in \bigcup R\left[\mathrm{\omega }\right]\to 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\right)\right)$$
513	159 512	biimtrid	$$⊢\phi \to \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\to \left(d\in \bigcup R\left[\mathrm{\omega }\right]\to 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\right)\right)$$
514	513	imp32	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
515		breq2	$$⊢f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to \left(1_s{<}_{s}f\leftrightarrow 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\right)$$
516	514 515	syl5ibrcom	$$⊢\left(\phi \wedge \left(c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\right)\to \left(f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to 1_s{<}_{s}f\right)$$
517	516	rexlimdvva	$$⊢\phi \to \left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to 1_s{<}_{s}f\right)$$
518	144	a1i	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to 1_s\in \mathrm{No}$$
519	518 411 409	addsubsassd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)\right)$$
520	404 407 408	subsdird	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(c{-}_{s}A\right){\cdot }_{s}d=\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)$$
521	520	oveq2d	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{\cdot }_{s}d\right){-}_s\left(A{\cdot }_{s}d\right)\right)$$
522	519 521	eqtr4d	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)=1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)$$
523	461	adantr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \bigcup L\left[\mathrm{\omega }\right]{\ll }_s\left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}$$
524	198	ad2antrl	$$⊢\left(\left(\phi \wedge c\in R\left(A\right)\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in L\left(i\right)\right)\right)\to \mathrm{suc}i\in \mathrm{\omega }$$
525	305	oveq1d	Could not format ( xR = c -> ( ( xR -s A ) x.s yL ) = ( ( c -s A ) x.s yL ) ) : No typesetting found for |- ( xR = c -> ( ( xR -s A ) x.s yL ) = ( ( c -s A ) x.s yL ) ) with typecode |-
526	525	oveq2d	Could not format ( xR = c -> ( 1s +s ( ( xR -s A ) x.s yL ) ) = ( 1s +s ( ( c -s A ) x.s yL ) ) ) : No typesetting found for |- ( xR = c -> ( 1s +s ( ( xR -s A ) x.s yL ) ) = ( 1s +s ( ( c -s A ) x.s yL ) ) ) with typecode |-
527	526 308	oveq12d	Could not format ( xR = c -> ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) ) : No typesetting found for |- ( xR = c -> ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) ) with typecode |-
528	527	eqeq2d	Could not format ( xR = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) ) ) : No typesetting found for |- ( xR = c -> ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s yL ) ) /su c ) ) ) with typecode |-
529	528 210	rspc2ev	Could not format ( ( c e. ( _Right ` A ) /\ d e. ( L ` i ) /\ ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) -> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) : No typesetting found for |- ( ( c e. ( _Right ` A ) /\ d e. ( L ` i ) /\ ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) ) -> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) with typecode |-
530	200 529	mp3an3	Could not format ( ( c e. ( _Right ` A ) /\ d e. ( L ` i ) ) -> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) : No typesetting found for |- ( ( c e. ( _Right ` A ) /\ d e. ( L ` i ) ) -> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) with typecode |-
531	530	ad2ant2l	Could not format ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) : No typesetting found for |- ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) with typecode |-
532		eqeq1	Could not format ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for |- ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode |-
533	532	2rexbidv	Could not format ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for |- ( a = ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) -> ( E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode |-
534	214 533	elab	Could not format ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) : No typesetting found for |- ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) with typecode |-
535	531 534	sylibr	Could not format ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } ) : No typesetting found for |- ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } ) with typecode |-
536		elun1	Could not format ( ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
537	535 536 476	3syl	Could not format ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( ( 1s +s ( ( c -s A ) x.s d ) ) /su c ) e. ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
538	478	ad2antrl	Could not format ( ( ( ph /\ c e. ( _Right ` A ) ) /\ ( i e. _om /\ d e. ( L ` i ) ) ) -> ( L ` suc i ) = ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s ( L ` suc i ) = ( ( L ` i ) u. ( { a | E. xR e. ( _Right ` A ) E. yL e. ( L ` i ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s
539	537 538	eleqtrrd	$$⊢\left(\left(\phi \wedge c\in R\left(A\right)\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in L\left(i\right)\right)\right)\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(\mathrm{suc}i\right)$$
540	524 539 483	syl2anc	$$⊢\left(\left(\phi \wedge c\in R\left(A\right)\right)\wedge \left(i\in \mathrm{\omega }\wedge d\in L\left(i\right)\right)\right)\to \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(j\right)$$
541	540	rexlimdvaa	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to \left(\exists i\in \mathrm{\omega }d\in L\left(i\right)\to \exists j\in \mathrm{\omega }\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in L\left(j\right)\right)$$
542	541 177 490	3imtr3g	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to \left(d\in \bigcup L\left[\mathrm{\omega }\right]\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup L\left[\mathrm{\omega }\right]\right)$$
543	542	impr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\in \bigcup L\left[\mathrm{\omega }\right]$$
544	196	a1i	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to Y\in \left\{\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]\right\}$$
545	523 543 544	ssltsepcd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\right){<}_{s}Y$$
546	338	adantrr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to c{-}_{s}A\in \mathrm{No}$$
547	546 408	mulscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(c{-}_{s}A\right){\cdot }_{s}d\in \mathrm{No}$$
548	518 547	addscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\in \mathrm{No}$$
549	346	adantrr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to 0_s{<}_{s}c$$
550	352	adantrr	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \exists y\in \mathrm{No}c{\cdot }_{s}y=1_s$$
551	548 405 404 549 550	sltdivmulwd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){/}_{\mathrm{su}}c\right){<}_{s}Y\leftrightarrow \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){<}_s\left(c{\cdot }_{s}Y\right)\right)$$
552	545 551	mpbid	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(1_s{+}_s\left(\left(c{-}_{s}A\right){\cdot }_{s}d\right)\right){<}_s\left(c{\cdot }_{s}Y\right)$$
553	522 552	eqbrtrd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right){<}_s\left(c{\cdot }_{s}Y\right)$$
554	518 411	addscld	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to 1_s{+}_s\left(c{\cdot }_{s}d\right)\in \mathrm{No}$$
555	554 409 406	sltsubaddd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right){<}_s\left(c{\cdot }_{s}Y\right)\leftrightarrow \left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){<}_s\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right)\right)$$
556	518 411 410	sltaddsubd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){<}_s\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right)\leftrightarrow 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\right)$$
557	555 556	bitrd	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(\left(\left(1_s{+}_s\left(c{\cdot }_{s}d\right)\right){-}_s\left(A{\cdot }_{s}d\right)\right){<}_s\left(c{\cdot }_{s}Y\right)\leftrightarrow 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\right)$$
558	553 557	mpbid	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to 1_s{<}_s\left(\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)$$
559	558 515	syl5ibrcom	$$⊢\left(\phi \wedge \left(c\in R\left(A\right)\wedge d\in \bigcup L\left[\mathrm{\omega }\right]\right)\right)\to \left(f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to 1_s{<}_{s}f\right)$$
560	559	rexlimdvva	$$⊢\phi \to \left(\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\to 1_s{<}_{s}f\right)$$
561	517 560	jaod	$$⊢\phi \to \left(\left(\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\vee \exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]f=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right)\to 1_s{<}_{s}f\right)$$
562	425 561	biimtrid	$$⊢\phi \to \left(f\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\to 1_s{<}_{s}f\right)$$
563		velsn	$$⊢e\in \left\{1_s\right\}\leftrightarrow e=1_s$$
564		breq1	$$⊢e=1_s\to \left(e{<}_{s}f\leftrightarrow 1_s{<}_{s}f\right)$$
565	564	imbi2d	$$⊢e=1_s\to \left(\left(f\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\to e{<}_{s}f\right)\leftrightarrow \left(f\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\to 1_s{<}_{s}f\right)\right)$$
566	563 565	sylbi	$$⊢e\in \left\{1_s\right\}\to \left(\left(f\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\to e{<}_{s}f\right)\leftrightarrow \left(f\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\to 1_s{<}_{s}f\right)\right)$$
567	562 566	syl5ibrcom	$$⊢\phi \to \left(e\in \left\{1_s\right\}\to \left(f\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\to e{<}_{s}f\right)\right)$$
568	567	3imp	$$⊢\left(\phi \wedge e\in \left\{1_s\right\}\wedge f\in \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)\right)\to e{<}_{s}f$$
569	105 391 146 416 568	ssltd	$$⊢\phi \to \left\{1_s\right\}{\ll }_s\left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)$$
570	81 376 569	cuteq1	$$⊢\phi \to \left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right){|}_s\left(\left\{b|\exists c\in \left(\left\{0_s\right\}\cup \left\{x\in L\left(A\right)|0_s{<}_{s}x\right\}\right)\exists d\in \bigcup R\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\cup \left\{b|\exists c\in R\left(A\right)\exists d\in \bigcup L\left[\mathrm{\omega }\right]b=\left(\left(c{\cdot }_{s}Y\right){+}_s\left(A{\cdot }_{s}d\right)\right){-}_s\left(c{\cdot }_{s}d\right)\right\}\right)=1_s$$
571	19 570	eqtrd	$$⊢\phi \to A{\cdot }_{s}Y=1_s$$