precsexlem9

Description: Lemma for surreal reciprocal. Show that the product of A and a left element is less than one and the product of A and a right element is greater than one. (Contributed by Scott Fenton, 14-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	$⊢ φ \to A \in No$
	precsexlem.5	$⊢ φ \to 0_{s} <_{s} A$
	precsexlem.6	No typesetting found for \|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s ~~E. y e. No ( xO x.s y ) = 1s ) ) with typecode \|-~~
Assertion	precsexlem9	$⊢ (φ \land I \in ω) \to (\forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c))$

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	$⊢ φ \to A \in No$
5		precsexlem.5	$⊢ φ \to 0_{s} <_{s} A$
6		precsexlem.6	Could not format ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s ~~E. y e. No ( xO x.s y ) = 1s ) ) : No typesetting found for \|- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s ~~E. y e. No ( xO x.s y ) = 1s ) ) with typecode \|-~~~~
7		fveq2	$⊢ i = \emptyset \to L (i) = L (\emptyset)$
8	7	raleqdv	$⊢ i = \emptyset \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s})$
9		fveq2	$⊢ i = \emptyset \to R (i) = R (\emptyset)$
10	9	raleqdv	$⊢ i = \emptyset \to (\forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c))$
11	8 10	anbi12d	$⊢ i = \emptyset \to ((\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c)))$
12	11	imbi2d	$⊢ i = \emptyset \to ((φ \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c))) \leftrightarrow (φ \to (\forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c))))$
13		fveq2	$⊢ i = j \to L (i) = L (j)$
14	13	raleqdv	$⊢ i = j \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s})$
15		fveq2	$⊢ i = j \to R (i) = R (j)$
16	15	raleqdv	$⊢ i = j \to (\forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))$
17	14 16	anbi12d	$⊢ i = j \to ((\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c)))$
18	17	imbi2d	$⊢ i = j \to ((φ \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c))) \leftrightarrow (φ \to (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))))$
19		fveq2	$⊢ i = suc j \to L (i) = L (suc j)$
20	19	raleqdv	$⊢ i = suc j \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall b \in L (suc j) (A \cdot_{s} b) <_{s} 1_{s})$
21		fveq2	$⊢ i = suc j \to R (i) = R (suc j)$
22	21	raleqdv	$⊢ i = suc j \to (\forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall c \in R (suc j) 1_{s} <_{s} (A \cdot_{s} c))$
23	20 22	anbi12d	$⊢ i = suc j \to ((\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall b \in L (suc j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (suc j) 1_{s} <_{s} (A \cdot_{s} c)))$
24		oveq2	$⊢ b = r \to A \cdot_{s} b = A \cdot_{s} r$
25	24	breq1d	$⊢ b = r \to ((A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow (A \cdot_{s} r) <_{s} 1_{s})$
26	25	cbvralvw	$⊢ \forall b \in L (suc j) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s}$
27		oveq2	$⊢ c = s \to A \cdot_{s} c = A \cdot_{s} s$
28	27	breq2d	$⊢ c = s \to (1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow 1_{s} <_{s} (A \cdot_{s} s))$
29	28	cbvralvw	$⊢ \forall c \in R (suc j) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s)$
30	26 29	anbi12i	$⊢ (\forall b \in L (suc j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (suc j) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))$
31	23 30	bitrdi	$⊢ i = suc j \to ((\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s)))$
32	31	imbi2d	$⊢ i = suc j \to ((φ \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c))) \leftrightarrow (φ \to (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))))$
33		fveq2	$⊢ i = I \to L (i) = L (I)$
34	33	raleqdv	$⊢ i = I \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s})$
35		fveq2	$⊢ i = I \to R (i) = R (I)$
36	35	raleqdv	$⊢ i = I \to (\forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c))$
37	34 36	anbi12d	$⊢ i = I \to ((\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c)) \leftrightarrow (\forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c)))$
38	37	imbi2d	$⊢ i = I \to ((φ \to (\forall b \in L (i) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (i) 1_{s} <_{s} (A \cdot_{s} c))) \leftrightarrow (φ \to (\forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c))))$
39		muls01	$⊢ A \in No \to A \cdot_{s} 0_{s} = 0_{s}$
40	4 39	syl	$⊢ φ \to A \cdot_{s} 0_{s} = 0_{s}$
41		0slt1s	$⊢ 0_{s} <_{s} 1_{s}$
42	40 41	eqbrtrdi	$⊢ φ \to (A \cdot_{s} 0_{s}) <_{s} 1_{s}$
43	1 2 3	precsexlem1	$⊢ L (\emptyset) = \{0_{s}\}$
44	43	raleqi	$⊢ \forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow \forall b \in \{0_{s}\} (A \cdot_{s} b) <_{s} 1_{s}$
45		0sno	$⊢ 0_{s} \in No$
46	45	elexi	$⊢ 0_{s} \in V$
47		oveq2	$⊢ b = 0_{s} \to A \cdot_{s} b = A \cdot_{s} 0_{s}$
48	47	breq1d	$⊢ b = 0_{s} \to ((A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow (A \cdot_{s} 0_{s}) <_{s} 1_{s})$
49	46 48	ralsn	$⊢ \forall b \in \{0_{s}\} (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow (A \cdot_{s} 0_{s}) <_{s} 1_{s}$
50	44 49	bitri	$⊢ \forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s} \leftrightarrow (A \cdot_{s} 0_{s}) <_{s} 1_{s}$
51	42 50	sylibr	$⊢ φ \to \forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s}$
52		ral0	$⊢ \forall c \in \emptyset 1_{s} <_{s} (A \cdot_{s} c)$
53	1 2 3	precsexlem2	$⊢ R (\emptyset) = \emptyset$
54	53	raleqi	$⊢ \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c) \leftrightarrow \forall c \in \emptyset 1_{s} <_{s} (A \cdot_{s} c)$
55	52 54	mpbir	$⊢ \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c)$
56	51 55	jctir	$⊢ φ \to (\forall b \in L (\emptyset) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (\emptyset) 1_{s} <_{s} (A \cdot_{s} c))$
57	1 2 3	precsexlem4	Could not format ( j e. _om -> ( L ` suc j ) = ( ( L ` j ) u. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( L ` suc j ) = ( ( L ` j ) u. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s~~
58	57	3ad2ant2	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( L ` suc j ) = ( ( L ` j ) u. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( L ` suc j ) = ( ( L ` j ) u. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s~~
59	58	eleq2d	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( r e. ( L ` suc j ) <-> r e. ( ( L ` j ) u. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( r e. ( L ` suc j ) <-> r e. ( ( L ` j ) u. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s~~
60		elun	Could not format ( r e. ( ( L ` j ) u. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ( r e. ( L ` j ) \/ r e. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( r e. ( L ` j ) \/ r e. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s~~
61		elun	Could not format ( r e. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ( r e. { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } \/ r e. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( r e. { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } \/ r e. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s~~
62		vex	$⊢ r \in V$
63		eqeq1	Could not format ( a = r -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for \|- ( a = r -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode \|-
64	63	2rexbidv	Could not format ( a = r -> ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for \|- ( a = r -> ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode \|-
65	62 64	elab	Could not format ( r e. { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) : No typesetting found for \|- ( r e. { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) with typecode \|-
66		eqeq1	Could not format ( a = r -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) : No typesetting found for \|- ( a = r -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) <-> r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) with typecode \|-
67	66	2rexbidv	Could not format ( a = r -> ( 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~~~~~~
68	62 67	elab	Could not format ( r 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~~~~
69	65 68	orbi12i	Could not format ( ( r e. { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } \/ r e. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s ~~( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s~~
70	61 69	bitri	Could not format ( r e. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s ~~( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s~~
71	70	orbi2i	Could not format ( ( r e. ( L ` j ) \/ r e. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s ~~( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s~~
72	60 71	bitri	Could not format ( r e. ( ( L ` j ) u. ( { a \| E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s ~~( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s~~
73	59 72	bitrdi	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( r e. ( L ` suc j ) <-> ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s ~~( r e. ( L ` suc j ) <-> ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s~~
74		simp3l	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to \forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s}$
75	25	rspccv	$⊢ \forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \to (r \in L (j) \to (A \cdot_{s} r) <_{s} 1_{s})$
76	74 75	syl	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (r \in L (j) \to (A \cdot_{s} r) <_{s} 1_{s})$
77	4	3ad2ant1	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to A \in No$
78	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) with typecode \|-~~~~
79		1sno	$⊢ 1_{s} \in No$
80	79	a1i	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s e. No ) with typecode \|-~~~~
81		rightssno	$⊢ R (A) \subseteq No$
82	81	sseli	Could not format ( xR e. ( _Right ` A ) -> xR e. No ) : No typesetting found for \|- ( xR e. ( _Right ` A ) -> xR e. No ) with typecode \|-
83	82	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR e. No ) with typecode \|-~~~~
84	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) with typecode \|-~~~~
85	83 84	subscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xR -s A ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xR -s A ) e. No ) with typecode \|-~~~~
86	85	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xR -s A ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xR -s A ) e. No ) with typecode \|-~~~~
87	1 2 3 4 5 6	precsexlem8	$⊢ (φ \land j \in ω) \to (L (j) \subseteq No \land R (j) \subseteq No)$
88	87	simpld	$⊢ (φ \land j \in ω) \to L (j) \subseteq No$
89	88	3adant3	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to L (j) \subseteq No$
90	89	sselda	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yL e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yL e. No ) with typecode \|-~~~~
91	90	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yL e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yL e. No ) with typecode \|-~~~~
92	86 91	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s yL ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s yL ) e. No ) with typecode \|-~~~~
93	80 92	addscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s +s ( ( xR -s A ) x.s yL ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s +s ( ( xR -s A ) x.s yL ) ) e. No ) with typecode \|-~~~~
94	83	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR e. No ) with typecode \|-~~~~
95	45	a1i	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s e. No ) with typecode \|-~~~~
96	5	3ad2ant1	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to 0_{s} <_{s} A$
97	96	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
98		breq2	Could not format ( xO = xR -> ( A ~~A ~~( A A~~~~
99		rightval	Could not format ( _Right ` A ) = { xO e. ( _Old ` ( bday ` A ) ) \| A
100	98 99	elrab2	Could not format ( xR e. ( _Right ` A ) <-> ( xR e. ( _Old ` ( bday ` A ) ) /\ A ~~( xR e. ( _Old ` ( bday ` A ) ) /\ A~~
101	100	simprbi	Could not format ( xR e. ( _Right ` A ) -> A A
102	101	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A A~~
103	95 84 83 97 102	slttrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
104	103	sgt0ne0d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR =/= 0s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR =/= 0s ) with typecode \|-~~~~
105	104	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR =/= 0s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR =/= 0s ) with typecode \|-~~~~
106		breq2	Could not format ( xO = xR -> ( 0s ~~0s ~~( 0s 0s~~~~
107		oveq1	Could not format ( xO = xR -> ( xO x.s y ) = ( xR x.s y ) ) : No typesetting found for \|- ( xO = xR -> ( xO x.s y ) = ( xR x.s y ) ) with typecode \|-
108	107	eqeq1d	Could not format ( xO = xR -> ( ( xO x.s y ) = 1s <-> ( xR x.s y ) = 1s ) ) : No typesetting found for \|- ( xO = xR -> ( ( xO x.s y ) = 1s <-> ( xR x.s y ) = 1s ) ) with typecode \|-
109	108	rexbidv	Could not format ( xO = xR -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xR x.s y ) = 1s ) ) : No typesetting found for \|- ( xO = xR -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xR x.s y ) = 1s ) ) with typecode \|-
110	106 109	imbi12d	Could not format ( xO = xR -> ( ( 0s E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s ~~E. y e. No ( xR x.s y ) = 1s ) ) ) : No typesetting found for \|- ( xO = xR -> ( ( 0s ~~E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s ~~E. y e. No ( xR x.s y ) = 1s ) ) ) with typecode \|-~~~~~~
111	6	3ad2ant1	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) : No typesetting found for \|- ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s ~~E. y e. No ( xO x.s y ) = 1s ) ) with typecode \|-~~~~
112	111	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s ~~E. y e. No ( xO x.s y ) = 1s ) ) with typecode \|-~~~~
113		elun2	Could not format ( xR e. ( _Right ` A ) -> xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for \|- ( xR e. ( _Right ` A ) -> xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode \|-
114	113	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode \|-~~~~
115	110 112 114	rspcdva	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 0s ~~E. y e. No ( xR x.s y ) = 1s ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 0s ~~E. y e. No ( xR x.s y ) = 1s ) ) with typecode \|-~~~~~~~~
116	103 115	mpd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xR x.s y ) = 1s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xR x.s y ) = 1s ) with typecode \|-~~~~
117	116	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xR x.s y ) = 1s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xR x.s y ) = 1s ) with typecode \|-~~~~
118	78 93 94 105 117	divsasswd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode \|-~~
119		oveq2	Could not format ( b = yL -> ( A x.s b ) = ( A x.s yL ) ) : No typesetting found for \|- ( b = yL -> ( A x.s b ) = ( A x.s yL ) ) with typecode \|-
120	119	breq1d	Could not format ( b = yL -> ( ( A x.s b ) ~~( A x.s yL ) ~~( ( A x.s b ) ~~( A x.s yL )~~~~~~
121	120	rspccva	Could not format ( ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yL ) ~~( A x.s yL )~~~~
122	74 121	sylan	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yL ) ~~( A x.s yL )~~~~
123	122	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yL ) ~~( A x.s yL )~~~~
124	78 91	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yL ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yL ) e. No ) with typecode \|-~~~~
125	84 83	posdifsd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A ~~0s ~~( A 0s~~~~~~
126	102 125	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
127	126	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
128	124 80 86 127	sltmul2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s yL ) ~~( ( xR -s A ) x.s ( A x.s yL ) ) ~~( ( A x.s yL ) ~~( ( xR -s A ) x.s ( A x.s yL ) )~~~~~~~~
129	123 128	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s ( A x.s yL ) ) ~~( ( xR -s A ) x.s ( A x.s yL ) )~~~~
130	86	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s 1s ) = ( xR -s A ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s 1s ) = ( xR -s A ) ) with typecode \|-~~~~
131	129 130	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s ( A x.s yL ) ) ~~( ( xR -s A ) x.s ( A x.s yL ) )~~~~
132	86 124	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s ( A x.s yL ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s ( A x.s yL ) ) e. No ) with typecode \|-~~~~
133	78 132 94	sltaddsub2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ~~( ( xR -s A ) x.s ( A x.s yL ) ) ~~( ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ~~( ( xR -s A ) x.s ( A x.s yL ) )~~~~~~~~
134	131 133	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ~~( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) )~~~~
135	78 80 92	addsdid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yL ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yL ) ) ) ) with typecode \|-~~
136	78	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s 1s ) = A ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s 1s ) = A ) with typecode \|-~~~~
137	78 86 91	muls12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xR -s A ) x.s yL ) ) = ( ( xR -s A ) x.s ( A x.s yL ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( ( xR -s A ) x.s yL ) ) = ( ( xR -s A ) x.s ( A x.s yL ) ) ) with typecode \|-~~
138	136 137	oveq12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yL ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yL ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ) with typecode \|-~~
139	135 138	eqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yL ) ) ) ) with typecode \|-~~
140	94	mulslidd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s x.s xR ) = xR ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s x.s xR ) = xR ) with typecode \|-~~~~
141	134 139 140	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) ~~( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) )~~~~
142	78 93	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) e. No ) with typecode \|-~~
143	103	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
144	142 80 94 143 117	sltdivmul2wd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR ) ~~( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) ~~( ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR ) ~~( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) )~~~~~~
145	141 144	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR ) ~~( ( A x.s ( 1s +s ( ( xR -s A ) x.s yL ) ) ) /su xR )~~~~
146	118 145	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ~~( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) )~~~~
147		oveq2	Could not format ( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) : No typesetting found for \|- ( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ) with typecode \|-
148	147	breq1d	Could not format ( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( ( A x.s r ) ~~( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) ) ~~( ( A x.s r ) ~~( A x.s ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) )~~~~~~
149	146 148	syl5ibrcom	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r ) ~~( r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r )~~~~
150	149	rexlimdvva	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r ) ~~( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) -> ( A x.s r )~~
151	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) with typecode \|-~~~~
152	79	a1i	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s e. No ) with typecode \|-~~~~
153		leftssno	$⊢ L (A) \subseteq No$
154		elrabi	Could not format ( xL e. { x e. ( _Left ` A ) \| 0s ~~xL e. ( _Left ` A ) ) : No typesetting found for \|- ( xL e. { x e. ( _Left ` A ) \| 0s ~~xL e. ( _Left ` A ) ) with typecode \|-~~~~
155	154	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL e. ( _Left ` A ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL e. ( _Left ` A ) ) with typecode \|-~~~~
156	153 155	sselid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL e. No ) with typecode \|-~~~~
157	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) with typecode \|-~~~~
158	156 157	subscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL -s A ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL -s A ) e. No ) with typecode \|-~~~~
159	158	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL -s A ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL -s A ) e. No ) with typecode \|-~~~~
160	87	simprd	$⊢ (φ \land j \in ω) \to R (j) \subseteq No$
161	160	3adant3	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to R (j) \subseteq No$
162	161	sselda	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yR e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yR e. No ) with typecode \|-~~~~
163	162	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yR e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yR e. No ) with typecode \|-~~~~
164	159 163	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) x.s yR ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) x.s yR ) e. No ) with typecode \|-~~~~
165	152 164	addscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s +s ( ( xL -s A ) x.s yR ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s +s ( ( xL -s A ) x.s yR ) ) e. No ) with typecode \|-~~~~
166	156	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL e. No ) with typecode \|-~~~~
167		breq2	Could not format ( x = xL -> ( 0s ~~0s ~~( 0s 0s~~~~
168	167	elrab	Could not format ( xL e. { x e. ( _Left ` A ) \| 0s ~~( xL e. ( _Left ` A ) /\ 0s ~~( xL e. ( _Left ` A ) /\ 0s~~~~
169	168	simprbi	Could not format ( xL e. { x e. ( _Left ` A ) \| 0s ~~0s 0s~~
170	169	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
171	170	sgt0ne0d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL =/= 0s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL =/= 0s ) with typecode \|-~~~~
172	171	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL =/= 0s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL =/= 0s ) with typecode \|-~~~~
173		breq2	Could not format ( xO = xL -> ( 0s ~~0s ~~( 0s 0s~~~~
174		oveq1	Could not format ( xO = xL -> ( xO x.s y ) = ( xL x.s y ) ) : No typesetting found for \|- ( xO = xL -> ( xO x.s y ) = ( xL x.s y ) ) with typecode \|-
175	174	eqeq1d	Could not format ( xO = xL -> ( ( xO x.s y ) = 1s <-> ( xL x.s y ) = 1s ) ) : No typesetting found for \|- ( xO = xL -> ( ( xO x.s y ) = 1s <-> ( xL x.s y ) = 1s ) ) with typecode \|-
176	175	rexbidv	Could not format ( xO = xL -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xL x.s y ) = 1s ) ) : No typesetting found for \|- ( xO = xL -> ( E. y e. No ( xO x.s y ) = 1s <-> E. y e. No ( xL x.s y ) = 1s ) ) with typecode \|-
177	173 176	imbi12d	Could not format ( xO = xL -> ( ( 0s E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s ~~E. y e. No ( xL x.s y ) = 1s ) ) ) : No typesetting found for \|- ( xO = xL -> ( ( 0s ~~E. y e. No ( xO x.s y ) = 1s ) <-> ( 0s ~~E. y e. No ( xL x.s y ) = 1s ) ) ) with typecode \|-~~~~~~
178	111	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s ~~E. y e. No ( xO x.s y ) = 1s ) ) with typecode \|-~~~~
179		elun1	Could not format ( xL e. ( _Left ` A ) -> xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for \|- ( xL e. ( _Left ` A ) -> xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode \|-
180	155 179	syl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode \|-~~~~
181	177 178 180	rspcdva	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 0s ~~E. y e. No ( xL x.s y ) = 1s ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 0s ~~E. y e. No ( xL x.s y ) = 1s ) ) with typecode \|-~~~~~~~~
182	170 181	mpd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xL x.s y ) = 1s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xL x.s y ) = 1s ) with typecode \|-~~~~
183	182	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xL x.s y ) = 1s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xL x.s y ) = 1s ) with typecode \|-~~~~
184	151 165 166 172 183	divsasswd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) with typecode \|-~~
185	157 156	subscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A -s xL ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A -s xL ) e. No ) with typecode \|-~~~~
186	185	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A -s xL ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A -s xL ) e. No ) with typecode \|-~~~~
187	186	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A -s xL ) x.s 1s ) = ( A -s xL ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A -s xL ) x.s 1s ) = ( A -s xL ) ) with typecode \|-~~~~
188		simp3r	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c)$
189		oveq2	Could not format ( c = yR -> ( A x.s c ) = ( A x.s yR ) ) : No typesetting found for \|- ( c = yR -> ( A x.s c ) = ( A x.s yR ) ) with typecode \|-
190	189	breq2d	Could not format ( c = yR -> ( 1s ~~1s ~~( 1s 1s~~~~
191	190	rspccva	Could not format ( ( A. c e. ( R ` j ) 1s ~~1s 1s~~
192	188 191	sylan	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
193	192	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
194	151 163	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yR ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yR ) e. No ) with typecode \|-~~~~
195		breq1	Could not format ( xO = xL -> ( xO ~~xL ~~( xO xL~~~~
196		leftval	Could not format ( _Left ` A ) = { xO e. ( _Old ` ( bday ` A ) ) \| xO
197	195 196	elrab2	Could not format ( xL e. ( _Left ` A ) <-> ( xL e. ( _Old ` ( bday ` A ) ) /\ xL ~~( xL e. ( _Old ` ( bday ` A ) ) /\ xL~~
198	197	simprbi	Could not format ( xL e. ( _Left ` A ) -> xL xL
199	155 198	syl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL xL~~
200	156 157	posdifsd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL ~~0s ~~( xL 0s~~~~~~
201	199 200	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
202	201	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
203	152 194 186 202	sltmul2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s ~~( ( A -s xL ) x.s 1s ) ~~( 1s ~~( ( A -s xL ) x.s 1s )~~~~~~~~
204	193 203	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A -s xL ) x.s 1s ) ~~( ( A -s xL ) x.s 1s )~~~~
205	187 204	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A -s xL ) ~~( A -s xL )~~~~
206	156 157	negsubsdi2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( -us ` ( xL -s A ) ) = ( A -s xL ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( -us ` ( xL -s A ) ) = ( A -s xL ) ) with typecode \|-~~~~
207	206	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( -us ` ( xL -s A ) ) = ( A -s xL ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( -us ` ( xL -s A ) ) = ( A -s xL ) ) with typecode \|-~~~~
208	159 194	mulnegs1d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( -us ` ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( -us ` ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) with typecode \|-~~
209	206	oveq1d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) with typecode \|-~~
210	209	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( -us ` ( xL -s A ) ) x.s ( A x.s yR ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) with typecode \|-~~
211	208 210	eqtr3d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( ( xL -s A ) x.s ( A x.s yR ) ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( -us ` ( ( xL -s A ) x.s ( A x.s yR ) ) ) = ( ( A -s xL ) x.s ( A x.s yR ) ) ) with typecode \|-~~
212	205 207 211	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( -us ` ( xL -s A ) ) ~~( -us ` ( xL -s A ) )~~~~
213	159 194	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) x.s ( A x.s yR ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) x.s ( A x.s yR ) ) e. No ) with typecode \|-~~~~
214	213 159	sltnegd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( ( xL -s A ) x.s ( A x.s yR ) ) ~~( -us ` ( xL -s A ) ) ~~( ( ( xL -s A ) x.s ( A x.s yR ) ) ~~( -us ` ( xL -s A ) )~~~~~~~~
215	212 214	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) x.s ( A x.s yR ) ) ~~( ( xL -s A ) x.s ( A x.s yR ) )~~~~
216	151 213 166	sltaddsub2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ~~( ( xL -s A ) x.s ( A x.s yR ) ) ~~( ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ~~( ( xL -s A ) x.s ( A x.s yR ) )~~~~~~~~
217	215 216	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ~~( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) )~~~~
218	151 152 164	addsdid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yR ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yR ) ) ) ) with typecode \|-~~
219	151	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s 1s ) = A ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s 1s ) = A ) with typecode \|-~~~~
220	151 159 163	muls12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xL -s A ) x.s yR ) ) = ( ( xL -s A ) x.s ( A x.s yR ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( ( xL -s A ) x.s yR ) ) = ( ( xL -s A ) x.s ( A x.s yR ) ) ) with typecode \|-~~
221	219 220	oveq12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yR ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yR ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) with typecode \|-~~
222	218 221	eqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yR ) ) ) ) with typecode \|-~~
223	166	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL x.s 1s ) = xL ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL x.s 1s ) = xL ) with typecode \|-~~~~
224	217 222 223	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) ~~( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) )~~~~
225	151 165	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) e. No ) with typecode \|-~~
226	170	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
227	225 152 166 226 183	sltdivmulwd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL ) ~~( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) ~~( ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL ) ~~( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) )~~~~~~
228	224 227	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL ) ~~( ( A x.s ( 1s +s ( ( xL -s A ) x.s yR ) ) ) /su xL )~~~~
229	184 228	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ~~( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) )~~~~
230		oveq2	Could not format ( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( A x.s r ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) : No typesetting found for \|- ( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( A x.s r ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ) with typecode \|-
231	230	breq1d	Could not format ( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( ( A x.s r ) ~~( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) ) ~~( ( A x.s r ) ~~( A x.s ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) )~~~~~~
232	229 231	syl5ibrcom	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( A x.s r ) ~~( r = ( ( 1s +s ( ( xL -s A ) x.s yR ) ) /su xL ) -> ( A x.s r )~~~~
233	232	rexlimdvva	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( E. xL e. { x e. ( _Left ` A ) \| 0s ~~( A x.s r ) ~~( E. xL e. { x e. ( _Left ` A ) \| 0s ~~( A x.s r )~~~~~~~~
234	150 233	jaod	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s ~~( A x.s r ) ~~( ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s ~~( A x.s r )~~~~~~
235	76 234	jaod	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s ~~( A x.s r ) ~~( ( r e. ( L ` j ) \/ ( E. xR e. ( _Right ` A ) E. yL e. ( L ` j ) r = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) \/ E. xL e. { x e. ( _Left ` A ) \| 0s ~~( A x.s r )~~~~~~
236	73 235	sylbid	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (r \in L (suc j) \to (A \cdot_{s} r) <_{s} 1_{s})$
237	236	ralrimiv	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to \forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s}$
238	1 2 3	precsexlem5	Could not format ( j e. _om -> ( R ` suc j ) = ( ( R ` j ) u. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( R ` suc j ) = ( ( R ` j ) u. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s~~
239	238	3ad2ant2	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( R ` suc j ) = ( ( R ` j ) u. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( R ` suc j ) = ( ( R ` j ) u. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s~~~~
240	239	eleq2d	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( s e. ( R ` suc j ) <-> s e. ( ( R ` j ) u. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( s e. ( R ` suc j ) <-> s e. ( ( R ` j ) u. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s~~~~
241		elun	Could not format ( s e. ( ( R ` j ) u. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( s e. ( R ` j ) \/ s e. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( s e. ( R ` j ) \/ s e. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s~~~~
242		elun	Could not format ( s e. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( s e. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( s e. { a \| E. xL e. { x e. ( _Left ` A ) \| 0s~~~~
243		vex	$⊢ s \in V$
244		eqeq1	Could not format ( a = s -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) : No typesetting found for \|- ( a = s -> ( a = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) <-> s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) with typecode \|-
245	244	2rexbidv	Could not format ( a = s -> ( 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~~~~~~
246	243 245	elab	Could not format ( s 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~~~~
247		eqeq1	Could not format ( a = s -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for \|- ( a = s -> ( a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode \|-
248	247	2rexbidv	Could not format ( a = s -> ( E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for \|- ( a = s -> ( E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode \|-
249	243 248	elab	Could not format ( s e. { a \| E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) : No typesetting found for \|- ( s e. { a \| E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) a = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) } <-> E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) with typecode \|-
250	246 249	orbi12i	Could not format ( ( s 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~~~~
251	242 250	bitri	Could not format ( s 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~~~~
252	251	orbi2i	Could not format ( ( s e. ( R ` j ) \/ s e. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) \| 0s ~~( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) \| 0s~~~~
253	241 252	bitri	Could not format ( s e. ( ( R ` j ) u. ( { a \| E. xL e. { x e. ( _Left ` A ) \| 0s ~~( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) \| 0s ~~( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) \| 0s~~~~
254	240 253	bitrdi	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( s e. ( R ` suc j ) <-> ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) \| 0s ~~( s e. ( R ` suc j ) <-> ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) \| 0s~~~~
255	28	rspccv	$⊢ \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c) \to (s \in R (j) \to 1_{s} <_{s} (A \cdot_{s} s))$
256	188 255	syl	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (s \in R (j) \to 1_{s} <_{s} (A \cdot_{s} s))$
257	122	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yL ) ~~( A x.s yL )~~~~
258	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) with typecode \|-~~~~
259	90	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yL e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yL e. No ) with typecode \|-~~~~
260	258 259	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yL ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yL ) e. No ) with typecode \|-~~~~
261	79	a1i	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s e. No ) with typecode \|-~~~~
262	185	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A -s xL ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A -s xL ) e. No ) with typecode \|-~~~~
263	201	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
264	260 261 262 263	sltmul2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s yL ) ~~( ( A -s xL ) x.s ( A x.s yL ) ) ~~( ( A x.s yL ) ~~( ( A -s xL ) x.s ( A x.s yL ) )~~~~~~~~
265	257 264	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A -s xL ) x.s ( A x.s yL ) ) ~~( ( A -s xL ) x.s ( A x.s yL ) )~~~~
266	262	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A -s xL ) x.s 1s ) = ( A -s xL ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A -s xL ) x.s 1s ) = ( A -s xL ) ) with typecode \|-~~~~
267	265 266	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A -s xL ) x.s ( A x.s yL ) ) ~~( ( A -s xL ) x.s ( A x.s yL ) )~~~~
268	158	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL -s A ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL -s A ) e. No ) with typecode \|-~~~~
269	268 260	mulnegs1d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) with typecode \|-~~
270	206	oveq1d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) with typecode \|-~~
271	270	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( -us ` ( xL -s A ) ) x.s ( A x.s yL ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) with typecode \|-~~
272	269 271	eqtr3d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) = ( ( A -s xL ) x.s ( A x.s yL ) ) ) with typecode \|-~~
273	206	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( -us ` ( xL -s A ) ) = ( A -s xL ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( -us ` ( xL -s A ) ) = ( A -s xL ) ) with typecode \|-~~~~
274	267 272 273	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) ~~( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) )~~~~
275	268 260	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) x.s ( A x.s yL ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) x.s ( A x.s yL ) ) e. No ) with typecode \|-~~~~
276	268 275	sltnegd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) ~~( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) ) ~~( ( xL -s A ) ~~( -us ` ( ( xL -s A ) x.s ( A x.s yL ) ) )~~~~~~~~
277	274 276	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL -s A ) ~~( xL -s A )~~~~
278	156	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL e. No ) with typecode \|-~~~~
279	278 258 275	sltsubadd2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) ~~xL ~~( ( xL -s A ) xL~~~~~~
280	277 279	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL xL~~
281	278	mulslidd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s x.s xL ) = xL ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s x.s xL ) = xL ) with typecode \|-~~~~
282	268 259	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) x.s yL ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xL -s A ) x.s yL ) e. No ) with typecode \|-~~~~
283	258 261 282	addsdid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yL ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yL ) ) ) ) with typecode \|-~~
284	258	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s 1s ) = A ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s 1s ) = A ) with typecode \|-~~~~
285	258 268 259	muls12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xL -s A ) x.s yL ) ) = ( ( xL -s A ) x.s ( A x.s yL ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( ( xL -s A ) x.s yL ) ) = ( ( xL -s A ) x.s ( A x.s yL ) ) ) with typecode \|-~~
286	284 285	oveq12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yL ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s 1s ) +s ( A x.s ( ( xL -s A ) x.s yL ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) with typecode \|-~~
287	283 286	eqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) = ( A +s ( ( xL -s A ) x.s ( A x.s yL ) ) ) ) with typecode \|-~~
288	280 281 287	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s x.s xL ) ~~( 1s x.s xL )~~~~
289	261 282	addscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s +s ( ( xL -s A ) x.s yL ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s +s ( ( xL -s A ) x.s yL ) ) e. No ) with typecode \|-~~~~
290	258 289	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) e. No ) with typecode \|-~~
291	170	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
292	182	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xL x.s y ) = 1s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xL x.s y ) = 1s ) with typecode \|-~~~~
293	261 290 278 291 292	sltmuldivwd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( 1s x.s xL ) ~~1s ~~( ( 1s x.s xL ) 1s~~~~~~
294	288 293	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
295	171	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL =/= 0s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL =/= 0s ) with typecode \|-~~~~
296	258 289 278 295 292	divsasswd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) /su xL ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s ( 1s +s ( ( xL -s A ) x.s yL ) ) ) /su xL ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) with typecode \|-~~
297	294 296	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
298		oveq2	Could not format ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( A x.s s ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) : No typesetting found for \|- ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( A x.s s ) = ( A x.s ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) ) ) with typecode \|-
299	298	breq2d	Could not format ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( 1s ~~1s ~~( 1s 1s~~~~
300	297 299	syl5ibrcom	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> 1s ~~( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> 1s~~~~
301	300	rexlimdvva	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( E. xL e. { x e. ( _Left ` A ) \| 0s ~~1s ~~( E. xL e. { x e. ( _Left ` A ) \| 0s 1s~~~~~~
302	85	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xR -s A ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xR -s A ) e. No ) with typecode \|-~~~~
303	302	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s 1s ) = ( xR -s A ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s 1s ) = ( xR -s A ) ) with typecode \|-~~~~
304	192	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
305	79	a1i	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s e. No ) with typecode \|-~~~~
306	77	adantr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A e. No ) with typecode \|-~~~~
307	162	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yR e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~yR e. No ) with typecode \|-~~~~
308	306 307	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yR ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yR ) e. No ) with typecode \|-~~~~
309	126	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
310	305 308 302 309	sltmul2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s ~~( ( xR -s A ) x.s 1s ) ~~( 1s ~~( ( xR -s A ) x.s 1s )~~~~~~~~
311	304 310	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s 1s ) ~~( ( xR -s A ) x.s 1s )~~~~
312	303 311	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xR -s A ) ~~( xR -s A )~~~~
313	83	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR e. No ) with typecode \|-~~~~
314	302 308	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s ( A x.s yR ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s ( A x.s yR ) ) e. No ) with typecode \|-~~~~
315	313 306 314	sltsubadd2d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) ~~xR ~~( ( xR -s A ) xR~~~~~~
316	312 315	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR xR~~
317	313	mulslidd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s x.s xR ) = xR ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s x.s xR ) = xR ) with typecode \|-~~~~
318	302 307	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s yR ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( xR -s A ) x.s yR ) e. No ) with typecode \|-~~~~
319	306 305 318	addsdid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yR ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) = ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yR ) ) ) ) with typecode \|-~~
320	306	mulsridd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s 1s ) = A ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s 1s ) = A ) with typecode \|-~~~~
321	306 302 307	muls12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( ( xR -s A ) x.s yR ) ) = ( ( xR -s A ) x.s ( A x.s yR ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( ( xR -s A ) x.s yR ) ) = ( ( xR -s A ) x.s ( A x.s yR ) ) ) with typecode \|-~~
322	320 321	oveq12d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yR ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yR ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s 1s ) +s ( A x.s ( ( xR -s A ) x.s yR ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yR ) ) ) ) with typecode \|-~~
323	319 322	eqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yR ) ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) = ( A +s ( ( xR -s A ) x.s ( A x.s yR ) ) ) ) with typecode \|-~~
324	316 317 323	3brtr4d	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s x.s xR ) ~~( 1s x.s xR )~~~~
325	305 318	addscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s +s ( ( xR -s A ) x.s yR ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( 1s +s ( ( xR -s A ) x.s yR ) ) e. No ) with typecode \|-~~~~
326	306 325	mulscld	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) e. No ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) e. No ) with typecode \|-~~
327	103	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
328	116	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xR x.s y ) = 1s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~E. y e. No ( xR x.s y ) = 1s ) with typecode \|-~~~~
329	305 326 313 327 328	sltmuldivwd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( 1s x.s xR ) ~~1s ~~( ( 1s x.s xR ) 1s~~~~~~
330	324 329	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
331	104	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR =/= 0s ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR =/= 0s ) with typecode \|-~~~~
332	306 325 313 331 328	divsasswd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) /su xR ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for \|- ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( A x.s ( 1s +s ( ( xR -s A ) x.s yR ) ) ) /su xR ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode \|-~~
333	330 332	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
334		oveq2	Could not format ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( A x.s s ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) : No typesetting found for \|- ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( A x.s s ) = ( A x.s ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) ) ) with typecode \|-
335	334	breq2d	Could not format ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( 1s ~~1s ~~( 1s 1s~~~~
336	333 335	syl5ibrcom	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> 1s ~~( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> 1s~~~~
337	336	rexlimdvva	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ( E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> 1s ~~( E. xR e. ( _Right ` A ) E. yR e. ( R ` j ) s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> 1s~~
338	301 337	jaod	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( E. xL e. { x e. ( _Left ` A ) \| 0s ~~1s ~~( ( E. xL e. { x e. ( _Left ` A ) \| 0s 1s~~~~~~
339	256 338	jaod	Could not format ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) \| 0s ~~1s ~~( ( s e. ( R ` j ) \/ ( E. xL e. { x e. ( _Left ` A ) \| 0s 1s~~~~~~
340	254 339	sylbid	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (s \in R (suc j) \to 1_{s} <_{s} (A \cdot_{s} s))$
341	340	ralrimiv	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s)$
342	237 341	jca	$⊢ (φ \land j \in ω \land (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))$
343	342	3exp	$⊢ φ \to (j \in ω \to ((\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c)) \to (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))))$
344	343	com12	$⊢ j \in ω \to (φ \to ((\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c)) \to (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))))$
345	344	a2d	$⊢ j \in ω \to ((φ \to (\forall b \in L (j) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (j) 1_{s} <_{s} (A \cdot_{s} c))) \to (φ \to (\forall r \in L (suc j) (A \cdot_{s} r) <_{s} 1_{s} \land \forall s \in R (suc j) 1_{s} <_{s} (A \cdot_{s} s))))$
346	12 18 32 38 56 345	finds	$⊢ I \in ω \to (φ \to (\forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c)))$
347	346	impcom	$⊢ (φ \land I \in ω) \to (\forall b \in L (I) (A \cdot_{s} b) <_{s} 1_{s} \land \forall c \in R (I) 1_{s} <_{s} (A \cdot_{s} c))$

Metamath Proof Explorer

Theorem precsexlem9

Proof