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		rightgt	Could not format ( xR e. ( _Right ` A ) -> A A
99	98	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~A A~~
100	95 84 83 97 99	slttrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
101	100	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 \|-~~~~
102	101	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 \|-~~~~
103		breq2	Could not format ( xO = xR -> ( 0s ~~0s ~~( 0s 0s~~~~
104		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 \|-
105	104	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 \|-
106	105	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 \|-
107	103 106	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 \|-~~~~~~
108	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 \|-~~~~
109	108	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 \|-~~~~
110		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 \|-
111	110	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 \|-~~~~
112	107 109 111	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 \|-~~~~~~~~
113	100 112	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 \|-~~~~
114	113	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 \|-~~~~
115	78 93 94 102 114	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 \|-~~
116		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 \|-
117	116	breq1d	Could not format ( b = yL -> ( ( A x.s b ) ~~( A x.s yL ) ~~( ( A x.s b ) ~~( A x.s yL )~~~~~~
118	117	rspccva	Could not format ( ( A. b e. ( L ` j ) ( A x.s b ) ~~( A x.s yL ) ~~( A x.s yL )~~~~
119	74 118	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 )~~~~
120	119	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 )~~~~
121	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 \|-~~~~
122	84 83	posdifsd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A ~~0s ~~( A 0s~~~~~~
123	99 122	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
124	123	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
125	121 80 86 124	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 ) )~~~~~~~~
126	120 125	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 ) )~~~~
127	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 \|-~~~~
128	126 127	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 ) )~~~~
129	86 121	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 \|-~~~~
130	78 129 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 ) )~~~~~~~~
131	128 130	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 ) ) )~~~~
132	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 \|-~~
133	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 \|-~~~~
134	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 \|-~~
135	133 134	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 \|-~~
136	132 135	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 \|-~~
137	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 \|-~~~~
138	131 136 137	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 ) ) )~~~~
139	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 \|-~~
140	100	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
141	139 80 94 140 114	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 ) ) )~~~~~~
142	138 141	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 )~~~~
143	115 142	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 ) )~~~~
144		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 \|-
145	144	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 ) )~~~~~~
146	143 145	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 )~~~~
147	146	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 )~~
148	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 \|-~~~~
149	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 \|-~~~~
150		leftssno	$⊢ L (A) \subseteq No$
151		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 \|-~~~~
152	151	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 \|-~~~~
153	150 152	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 \|-~~~~
154	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 \|-~~~~
155	153 154	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 \|-~~~~
156	155	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 \|-~~~~
157	87	simprd	$⊢ (φ \land j \in ω) \to R (j) \subseteq No$
158	157	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$
159	158	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 \|-~~~~
160	159	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 \|-~~~~
161	156 160	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 \|-~~~~
162	149 161	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 \|-~~~~
163	153	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 \|-~~~~
164		breq2	Could not format ( x = xL -> ( 0s ~~0s ~~( 0s 0s~~~~
165	164	elrab	Could not format ( xL e. { x e. ( _Left ` A ) \| 0s ~~( xL e. ( _Left ` A ) /\ 0s ~~( xL e. ( _Left ` A ) /\ 0s~~~~
166	165	simprbi	Could not format ( xL e. { x e. ( _Left ` A ) \| 0s ~~0s 0s~~
167	166	adantl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
168	167	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 \|-~~~~
169	168	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 \|-~~~~
170		breq2	Could not format ( xO = xL -> ( 0s ~~0s ~~( 0s 0s~~~~
171		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 \|-
172	171	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 \|-
173	172	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 \|-
174	170 173	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 \|-~~~~~~
175	108	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 \|-~~~~
176		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 \|-
177	152 176	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 \|-~~~~
178	174 175 177	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 \|-~~~~~~~~
179	167 178	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 \|-~~~~
180	179	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 \|-~~~~
181	148 162 163 169 180	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 \|-~~
182	154 153	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 \|-~~~~
183	182	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 \|-~~~~
184	183	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 \|-~~~~
185		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)$
186		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 \|-
187	186	breq2d	Could not format ( c = yR -> ( 1s ~~1s ~~( 1s 1s~~~~
188	187	rspccva	Could not format ( ( A. c e. ( R ` j ) 1s ~~1s 1s~~
189	185 188	sylan	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
190	189	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
191	148 160	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 \|-~~~~
192		leftlt	Could not format ( xL e. ( _Left ` A ) -> xL xL
193	152 192	syl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL xL~~
194	153 154	posdifsd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL ~~0s ~~( xL 0s~~~~~~
195	193 194	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
196	195	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
197	149 191 183 196	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 )~~~~~~~~
198	190 197	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 )~~~~
199	184 198	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( A -s xL ) ~~( A -s xL )~~~~
200	153 154	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 \|-~~~~
201	200	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 \|-~~~~
202	156 191	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 \|-~~
203	200	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 \|-~~
204	203	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 \|-~~
205	202 204	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 \|-~~
206	199 201 205	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 ) )~~~~
207	156 191	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 \|-~~~~
208	207 156	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 ) )~~~~~~~~
209	206 208	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 ) )~~~~
210	148 207 163	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 ) )~~~~~~~~
211	209 210	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 ) ) )~~~~
212	148 149 161	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 \|-~~
213	148	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 \|-~~~~
214	148 156 160	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 \|-~~
215	213 214	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 \|-~~
216	212 215	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 \|-~~
217	163	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 \|-~~~~
218	211 216 217	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 ) ) )~~~~
219	148 162	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 \|-~~
220	167	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
221	219 149 163 220 180	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 ) ) )~~~~~~
222	218 221	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 )~~~~
223	181 222	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 ) )~~~~
224		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 \|-
225	224	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 ) )~~~~~~
226	223 225	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 )~~~~
227	226	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 )~~~~~~~~
228	147 227	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 )~~~~~~
229	76 228	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 )~~~~~~
230	73 229	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})$
231	230	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}$
232	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~~
233	232	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~~~~
234	233	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~~~~
235		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~~~~
236		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~~~~
237		vex	$⊢ s \in V$
238		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 \|-
239	238	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~~~~~~
240	237 239	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~~~~
241		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 \|-
242	241	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 \|-
243	237 242	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 \|-
244	240 243	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~~~~
245	236 244	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~~~~
246	245	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~~~~
247	235 246	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~~~~
248	234 247	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~~~~
249	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))$
250	185 249	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))$
251	119	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 )~~~~
252	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 \|-~~~~
253	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 \|-~~~~
254	252 253	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 \|-~~~~
255	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 \|-~~~~
256	182	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 \|-~~~~
257	195	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
258	254 255 256 257	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 ) )~~~~~~~~
259	251 258	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 ) )~~~~
260	256	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 \|-~~~~
261	259 260	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 ) )~~~~
262	155	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 \|-~~~~
263	262 254	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 \|-~~
264	200	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 \|-~~
265	264	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 \|-~~
266	263 265	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 \|-~~
267	200	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 \|-~~~~
268	261 266 267	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 ) ) )~~~~
269	262 254	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 \|-~~~~
270	262 269	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 ) ) )~~~~~~~~
271	268 270	mpbird	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xL -s A ) ~~( xL -s A )~~~~
272	153	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 \|-~~~~
273	272 252 269	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~~~~~~
274	271 273	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xL xL~~
275	272	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 \|-~~~~
276	262 253	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 \|-~~~~
277	252 255 276	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 \|-~~
278	252	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 \|-~~~~
279	252 262 253	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 \|-~~
280	278 279	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 \|-~~
281	277 280	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 \|-~~
282	274 275 281	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 )~~~~
283	255 276	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 \|-~~~~
284	252 283	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 \|-~~
285	167	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
286	179	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 \|-~~~~
287	255 284 272 285 286	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~~~~~~
288	282 287	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
289	168	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 \|-~~~~
290	252 283 272 289 286	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 \|-~~
291	288 290	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
292		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 \|-
293	292	breq2d	Could not format ( s = ( ( 1s +s ( ( xL -s A ) x.s yL ) ) /su xL ) -> ( 1s ~~1s ~~( 1s 1s~~~~
294	291 293	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~~~~
295	294	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~~~~~~
296	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 \|-~~~~
297	296	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 \|-~~~~
298	189	adantrl	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
299	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 \|-~~~~
300	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 \|-~~~~
301	159	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 \|-~~~~
302	300 301	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 \|-~~~~
303	123	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
304	299 302 296 303	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 )~~~~~~~~
305	298 304	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 )~~~~
306	297 305	eqbrtrrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~( xR -s A ) ~~( xR -s A )~~~~
307	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 \|-~~~~
308	296 302	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 \|-~~~~
309	307 300 308	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~~~~~~
310	306 309	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~xR xR~~
311	307	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 \|-~~~~
312	296 301	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 \|-~~~~
313	300 299 312	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 \|-~~
314	300	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 \|-~~~~
315	300 296 301	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 \|-~~
316	314 315	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 \|-~~
317	313 316	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 \|-~~
318	310 311 317	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 )~~~~
319	299 312	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 \|-~~~~
320	300 319	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 \|-~~
321	100	adantrr	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~0s 0s~~
322	113	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 \|-~~~~
323	299 320 307 321 322	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~~~~~~
324	318 323	mpbid	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
325	101	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 \|-~~~~
326	300 319 307 325 322	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 \|-~~
327	324 326	breqtrd	Could not format ( ( ( ph /\ j e. _om /\ ( A. b e. ( L ` j ) ( A x.s b ) ~~1s 1s~~
328		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 \|-
329	328	breq2d	Could not format ( s = ( ( 1s +s ( ( xR -s A ) x.s yR ) ) /su xR ) -> ( 1s ~~1s ~~( 1s 1s~~~~
330	327 329	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~~~~
331	330	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~~
332	295 331	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~~~~~~
333	250 332	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~~~~~~
334	248 333	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))$
335	334	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)$
336	231 335	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))$
337	336	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))))$
338	337	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))))$
339	338	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))))$
340	12 18 32 38 56 339	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)))$
341	340	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