Theorem precsexlem11

Description: Lemma for surreal reciprocal. Show that the cut of the left and right sets is a multiplicative inverse for A . (Contributed by Scott Fenton, 15-Mar-2025)

	Ref	Expression
Hypotheses	precsexlem.1	No typesetting found for |- F = rec ( ( p e. _V |-> [_ ( 1st ` p ) / l ]_ [_ ( 2nd ` p ) / r ]_ <. ( l u. ( { a | E. xR e. ( _Right ` A ) E. yL e. l a = ( ( 1s +s ( ( xR -s A ) x.s yL ) ) /su xR ) } u. { a | E. xL e. { x e. ( _Left ` A ) | 0s . ) , <. { 0s } , (/) >. ) with typecode |-
	precsexlem.2	$$⊢L=1^{st}\circ F$$
	precsexlem.3	$$⊢R=2^{nd}\circ F$$
	precsexlem.4	$$⊢\phi \to A\in \mathrm{No}$$
	precsexlem.5	No typesetting found for |- ( ph -> 0s
	precsexlem.6	No typesetting found for |- ( ph -> A. xO e. ( ( _Left ` A ) u. ( _Right ` A ) ) ( 0s E. y e. No ( xO x.s y ) = 1s ) ) with typecode |-
	precsexlem.7	$$⊢Y=\bigcup L\left[\mathrm{\omega }\right]{|}_s\bigcup R\left[\mathrm{\omega }\right]$$
Assertion	precsexlem11	Could not format assertion : No typesetting found for |- ( ph -> ( A x.s Y ) = 1s ) with typecode |-

Proof

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