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		breq2	Could not format ( xO = c -> ( A A ( A A
345		rightval	Could not format ( _Right ` A ) = { xO e. ( _Old ` ( bday ` A ) ) | A
346	344 345	elrab2	$$⊢c\in R\left(A\right)\leftrightarrow \left(c\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\wedge A{<}_{s}c\right)$$
347	346	simprbi	$$⊢c\in R\left(A\right)\to A{<}_{s}c$$
348	347	adantl	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to A{<}_{s}c$$
349	342 337 127 343 348	slttrd	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to 0_s{<}_{s}c$$
350	349	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$$
351	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 |-
352		elun2	$$⊢c\in R\left(A\right)\to c\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
353	352	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)$$
354	267 351 353	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)$$
355	349 354	mpd	$$⊢\left(\phi \wedge c\in R\left(A\right)\right)\to \exists y\in \mathrm{No}c{\cdot }_{s}y=1_s$$
356	355	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$$
357	129 341 128 350 356	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)$$
358	335 357	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)$$
359	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)$$
360	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)$$
361	360	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)$$
362	359 361	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)$$
363	358 362	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)$$
364	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)$$
365	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}$$
366	130 136 365	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)$$
367	364 366	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)$$
368	363 367	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$$
369	368 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)$$
370	369	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)$$
371	301 370	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)$$
372	155 371	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)$$
373	372	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$$
374		velsn	$$⊢f\in \left\{1_s\right\}\leftrightarrow f=1_s$$
375		breq2	$$⊢f=1_s\to \left(e{<}_{s}f\leftrightarrow e{<}_s{1}_s\right)$$
376	374 375	sylbi	$$⊢f\in \left\{1_s\right\}\to \left(e{<}_{s}f\leftrightarrow e{<}_s{1}_s\right)$$
377	373 376	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)$$
378	377	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$$
379	103 105 143 146 378	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\}$$
380		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)$$
381	380	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\}$$
382		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}$$
383	85 97 382	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}$$
384		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}$$
385	383 384	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}$$
386	381 385	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}$$
387		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)$$
388	387	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\}$$
389		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}$$
390	95 87 389	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}$$
391		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}$$
392	390 391	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}$$
393	388 392	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}$$
394	386 393	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}$$
395	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}$$
396	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}$$
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 c{\cdot }_{s}Y\in \mathrm{No}$$
398	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}$$
399	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}$$
400	398 399	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}$$
401	397 400	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}$$
402	395 399	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}$$
403	401 402	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}$$
404	403 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)$$
405	404	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)$$
406	405	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}$$
407	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}$$
408	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}$$
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 c{\cdot }_{s}Y\in \mathrm{No}$$
410	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}$$
411	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}$$
412	410 411	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}$$
413	409 412	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}$$
414	407 411	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}$$
415	413 414	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}$$
416	415 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)$$
417	416	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)$$
418	417	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}$$
419	406 418	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}$$
420		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)$$
421		vex	$$⊢f\in \mathrm{V}$$
422		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)$$
423	422	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)$$
424	421 423	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)$$
425	422	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)$$
426	421 425	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)$$
427	424 426	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)$$
428	420 427	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)$$
429		eliun	$$⊢d\in \bigcup _{j\in \mathrm{\omega }}R\left(j\right)\leftrightarrow \exists j\in \mathrm{\omega }d\in R\left(j\right)$$
430	239	eleq2i	$$⊢d\in \bigcup _{j\in \mathrm{\omega }}R\left(j\right)\leftrightarrow d\in \bigcup R\left[\mathrm{\omega }\right]$$
431	429 430	bitr3i	$$⊢\exists j\in \mathrm{\omega }d\in R\left(j\right)\leftrightarrow d\in \bigcup R\left[\mathrm{\omega }\right]$$
432	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)$$
433		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)$$
434	432 433	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)$$
435	434	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)$$
436	431 435	biimtrrid	$$⊢\phi \to \left(d\in \bigcup R\left[\mathrm{\omega }\right]\to 1_s{<}_s\left(A{\cdot }_{s}d\right)\right)$$
437	436	imp	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to 1_s{<}_s\left(A{\cdot }_{s}d\right)$$
438	56	adantr	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to Y\in \mathrm{No}$$
439	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)$$
440	438 439	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)$$
441	4	adantr	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to A\in \mathrm{No}$$
442	441 134	mulscld	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to A{\cdot }_{s}d\in \mathrm{No}$$
443	442 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$$
444	440 443	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$$
445	134 162	syl	$$⊢\left(\phi \wedge d\in \bigcup R\left[\mathrm{\omega }\right]\right)\to 0_s{\cdot }_{s}d=0_s$$
446	444 445	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$$
447	442 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$$
448	446 447	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$$
449	437 448	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)$$
450	449	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)$$
451	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)$$
452	451	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)$$
453	450 452	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)$$
454	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}$$
455	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}$$
456	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}$$
457	455 456	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}$$
458	442	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}$$
459	454 457 458	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)$$
460	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}$$
461	455 460 456	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)$$
462	461	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)$$
463	459 462	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)$$
464	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\}$$
465	464	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\}$$
466	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 }$$
467	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 |-
468	467	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 |-
469	468 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 |-
470	469	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 |-
471	470 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
472	200 471	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
473	472	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
474		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 |-
475	474	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
476	214 475	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
477	473 476	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
478		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
479		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
480	477 478 479	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
481	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
482	481	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
483	480 482	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)$$
484		fveq2	$$⊢j=\mathrm{suc}i\to L\left(j\right)=L\left(\mathrm{suc}i\right)$$
485	484	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)$$
486	485	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)$$
487	466 483 486	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)$$
488	487	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)$$
489		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)$$
490		funiunfv	$$⊢\mathrm{Fun}L\to \bigcup _{j\in \mathrm{\omega }}L\left(j\right)=\bigcup L\left[\mathrm{\omega }\right]$$
491	43 490	ax-mp	$$⊢\bigcup _{j\in \mathrm{\omega }}L\left(j\right)=\bigcup L\left[\mathrm{\omega }\right]$$
492	491	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]$$
493	489 492	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]$$
494	488 332 493	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)$$
495	494	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]$$
496	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\}$$
497	465 495 496	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$$
498	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}$$
499	498 456	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}$$
500	454 499	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}$$
501	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}$$
502	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$$
503	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$$
504	500 501 455 502 503	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)$$
505	497 504	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)$$
506	463 505	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)$$
507	454 457	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}$$
508	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}$$
509	507 458 508	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)$$
510	508 458	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}$$
511	454 457 510	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)$$
512	509 511	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)$$
513	506 512	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)$$
514	513	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)$$
515	453 514	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)$$
516	159 515	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)$$
517	516	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)$$
518		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)$$
519	517 518	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)$$
520	519	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)$$
521	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}$$
522	521 414 412	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)$$
523	407 410 411	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)$$
524	523	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)$$
525	522 524	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)$$
526	464	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\}$$
527	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 }$$
528	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 |-
529	528	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 |-
530	529 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 |-
531	530	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 |-
532	531 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 |-
533	200 532	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 |-
534	533	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 |-
535		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 |-
536	535	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 |-
537	214 536	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 |-
538	534 537	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 |-
539		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
540	538 539 479	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
541	481	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
542	540 541	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)$$
543	527 542 486	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)$$
544	543	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)$$
545	544 177 493	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)$$
546	545	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]$$
547	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\}$$
548	526 546 547	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$$
549	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}$$
550	549 411	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}$$
551	521 550	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}$$
552	349	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$$
553	355	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$$
554	551 408 407 552 553	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)$$
555	548 554	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)$$
556	525 555	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)$$
557	521 414	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}$$
558	557 412 409	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)$$
559	521 414 413	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)$$
560	558 559	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)$$
561	556 560	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)$$
562	561 518	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)$$
563	562	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)$$
564	520 563	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)$$
565	428 564	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)$$
566		velsn	$$⊢e\in \left\{1_s\right\}\leftrightarrow e=1_s$$
567		breq1	$$⊢e=1_s\to \left(e{<}_{s}f\leftrightarrow 1_s{<}_{s}f\right)$$
568	567	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)$$
569	566 568	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)$$
570	565 569	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)$$
571	570	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$$
572	105 394 146 419 571	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)$$
573	81 379 572	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$$
574	19 573	eqtrd	$$⊢\phi \to A{\cdot }_{s}Y=1_s$$