Theorem addsval

Description: The value of surreal addition. Definition from Conway p. 5. (Contributed by Scott Fenton, 20-Aug-2024)

	Ref	Expression
Assertion	addsval	Could not format assertion : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. l e. ( _Left ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _Right ` A ) y = ( r +s B ) } u. { z | E. r e. ( _Right ` B ) z = ( A +s r ) } ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-adds	Could not format +s = norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ) : No typesetting found for |- +s = norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ) with typecode |-
2	1	norec2ov	Could not format ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) ) with typecode |-
3		opex	$$⊢⟨A,B⟩\in \mathrm{V}$$
4		addsfn	Could not format +s Fn ( No X. No ) : No typesetting found for |- +s Fn ( No X. No ) with typecode |-
5		fnfun	Could not format ( +s Fn ( No X. No ) -> Fun +s ) : No typesetting found for |- ( +s Fn ( No X. No ) -> Fun +s ) with typecode |-
6	4 5	ax-mp	Could not format Fun +s : No typesetting found for |- Fun +s with typecode |-
7		fvex	Could not format ( _Left ` A ) e. _V : No typesetting found for |- ( _Left ` A ) e. _V with typecode |-
8		fvex	Could not format ( _Right ` A ) e. _V : No typesetting found for |- ( _Right ` A ) e. _V with typecode |-
9	7 8	unex	Could not format ( ( _Left ` A ) u. ( _Right ` A ) ) e. _V : No typesetting found for |- ( ( _Left ` A ) u. ( _Right ` A ) ) e. _V with typecode |-
10		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
11	9 10	unex	Could not format ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) e. _V : No typesetting found for |- ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) e. _V with typecode |-
12		fvex	Could not format ( _Left ` B ) e. _V : No typesetting found for |- ( _Left ` B ) e. _V with typecode |-
13		fvex	Could not format ( _Right ` B ) e. _V : No typesetting found for |- ( _Right ` B ) e. _V with typecode |-
14	12 13	unex	Could not format ( ( _Left ` B ) u. ( _Right ` B ) ) e. _V : No typesetting found for |- ( ( _Left ` B ) u. ( _Right ` B ) ) e. _V with typecode |-
15		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
16	14 15	unex	Could not format ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) e. _V : No typesetting found for |- ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) e. _V with typecode |-
17	11 16	xpex	Could not format ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) e. _V : No typesetting found for |- ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) e. _V with typecode |-
18	17	difexi	Could not format ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) e. _V : No typesetting found for |- ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) e. _V with typecode |-
19		resfunexg	Could not format ( ( Fun +s /\ ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) e. _V ) -> ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V ) : No typesetting found for |- ( ( Fun +s /\ ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) e. _V ) -> ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V ) with typecode |-
20	6 18 19	mp2an	Could not format ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V : No typesetting found for |- ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V with typecode |-
21		2fveq3	Could not format ( x = <. A , B >. -> ( _Left ` ( 1st ` x ) ) = ( _Left ` ( 1st ` <. A , B >. ) ) ) : No typesetting found for |- ( x = <. A , B >. -> ( _Left ` ( 1st ` x ) ) = ( _Left ` ( 1st ` <. A , B >. ) ) ) with typecode |-
22		fveq2	$$⊢x=⟨A,B⟩\to 2^{nd}\left(x\right)=2^{nd}\left(⟨A,B⟩\right)$$
23	22	oveq2d	$$⊢x=⟨A,B⟩\to la{2}^{nd}\left(x\right)=la{2}^{nd}\left(⟨A,B⟩\right)$$
24	23	eqeq2d	$$⊢x=⟨A,B⟩\to \left(y=la{2}^{nd}\left(x\right)\leftrightarrow y=la{2}^{nd}\left(⟨A,B⟩\right)\right)$$
25	21 24	rexeqbidv	Could not format ( x = <. A , B >. -> ( E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) <-> E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) ) ) : No typesetting found for |- ( x = <. A , B >. -> ( E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) <-> E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) ) ) with typecode |-
26	25	abbidv	Could not format ( x = <. A , B >. -> { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } = { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } ) : No typesetting found for |- ( x = <. A , B >. -> { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } = { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } ) with typecode |-
27		2fveq3	Could not format ( x = <. A , B >. -> ( _Left ` ( 2nd ` x ) ) = ( _Left ` ( 2nd ` <. A , B >. ) ) ) : No typesetting found for |- ( x = <. A , B >. -> ( _Left ` ( 2nd ` x ) ) = ( _Left ` ( 2nd ` <. A , B >. ) ) ) with typecode |-
28		fveq2	$$⊢x=⟨A,B⟩\to 1^{st}\left(x\right)=1^{st}\left(⟨A,B⟩\right)$$
29	28	oveq1d	$$⊢x=⟨A,B⟩\to 1^{st}\left(x\right)al=1^{st}\left(⟨A,B⟩\right)al$$
30	29	eqeq2d	$$⊢x=⟨A,B⟩\to \left(z=1^{st}\left(x\right)al\leftrightarrow z=1^{st}\left(⟨A,B⟩\right)al\right)$$
31	27 30	rexeqbidv	Could not format ( x = <. A , B >. -> ( E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) <-> E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) ) ) : No typesetting found for |- ( x = <. A , B >. -> ( E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) <-> E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) ) ) with typecode |-
32	31	abbidv	Could not format ( x = <. A , B >. -> { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } = { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) : No typesetting found for |- ( x = <. A , B >. -> { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } = { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) with typecode |-
33	26 32	uneq12d	Could not format ( x = <. A , B >. -> ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) = ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) ) : No typesetting found for |- ( x = <. A , B >. -> ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) = ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) ) with typecode |-
34		2fveq3	Could not format ( x = <. A , B >. -> ( _Right ` ( 1st ` x ) ) = ( _Right ` ( 1st ` <. A , B >. ) ) ) : No typesetting found for |- ( x = <. A , B >. -> ( _Right ` ( 1st ` x ) ) = ( _Right ` ( 1st ` <. A , B >. ) ) ) with typecode |-
35	22	oveq2d	$$⊢x=⟨A,B⟩\to ra{2}^{nd}\left(x\right)=ra{2}^{nd}\left(⟨A,B⟩\right)$$
36	35	eqeq2d	$$⊢x=⟨A,B⟩\to \left(y=ra{2}^{nd}\left(x\right)\leftrightarrow y=ra{2}^{nd}\left(⟨A,B⟩\right)\right)$$
37	34 36	rexeqbidv	Could not format ( x = <. A , B >. -> ( E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) <-> E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) ) ) : No typesetting found for |- ( x = <. A , B >. -> ( E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) <-> E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) ) ) with typecode |-
38	37	abbidv	Could not format ( x = <. A , B >. -> { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } = { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } ) : No typesetting found for |- ( x = <. A , B >. -> { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } = { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } ) with typecode |-
39		2fveq3	Could not format ( x = <. A , B >. -> ( _Right ` ( 2nd ` x ) ) = ( _Right ` ( 2nd ` <. A , B >. ) ) ) : No typesetting found for |- ( x = <. A , B >. -> ( _Right ` ( 2nd ` x ) ) = ( _Right ` ( 2nd ` <. A , B >. ) ) ) with typecode |-
40	28	oveq1d	$$⊢x=⟨A,B⟩\to 1^{st}\left(x\right)ar=1^{st}\left(⟨A,B⟩\right)ar$$
41	40	eqeq2d	$$⊢x=⟨A,B⟩\to \left(z=1^{st}\left(x\right)ar\leftrightarrow z=1^{st}\left(⟨A,B⟩\right)ar\right)$$
42	39 41	rexeqbidv	Could not format ( x = <. A , B >. -> ( E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) <-> E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) ) ) : No typesetting found for |- ( x = <. A , B >. -> ( E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) <-> E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) ) ) with typecode |-
43	42	abbidv	Could not format ( x = <. A , B >. -> { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } = { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) : No typesetting found for |- ( x = <. A , B >. -> { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } = { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) with typecode |-
44	38 43	uneq12d	Could not format ( x = <. A , B >. -> ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) = ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) ) : No typesetting found for |- ( x = <. A , B >. -> ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) = ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) ) with typecode |-
45	33 44	oveq12d	Could not format ( x = <. A , B >. -> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) = ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) ) ) : No typesetting found for |- ( x = <. A , B >. -> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) = ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) ) ) with typecode |-
46		oveq	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( l a ( 2nd ` <. A , B >. ) ) = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( l a ( 2nd ` <. A , B >. ) ) = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) with typecode |-
47	46	eqeq2d	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( y = ( l a ( 2nd ` <. A , B >. ) ) <-> y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( y = ( l a ( 2nd ` <. A , B >. ) ) <-> y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) with typecode |-
48	47	rexbidv	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) <-> E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) <-> E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) with typecode |-
49	48	abbidv	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } = { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } = { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } ) with typecode |-
50		oveq	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( 1st ` <. A , B >. ) a l ) = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( 1st ` <. A , B >. ) a l ) = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) with typecode |-
51	50	eqeq2d	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( z = ( ( 1st ` <. A , B >. ) a l ) <-> z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( z = ( ( 1st ` <. A , B >. ) a l ) <-> z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) ) with typecode |-
52	51	rexbidv	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) <-> E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) <-> E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) ) with typecode |-
53	52	abbidv	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } = { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } = { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) with typecode |-
54	49 53	uneq12d	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) = ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) = ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) ) with typecode |-
55		oveq	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( r a ( 2nd ` <. A , B >. ) ) = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( r a ( 2nd ` <. A , B >. ) ) = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) with typecode |-
56	55	eqeq2d	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( y = ( r a ( 2nd ` <. A , B >. ) ) <-> y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( y = ( r a ( 2nd ` <. A , B >. ) ) <-> y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) with typecode |-
57	56	rexbidv	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) <-> E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) <-> E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) with typecode |-
58	57	abbidv	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } = { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } = { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } ) with typecode |-
59		oveq	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( 1st ` <. A , B >. ) a r ) = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( 1st ` <. A , B >. ) a r ) = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) with typecode |-
60	59	eqeq2d	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( z = ( ( 1st ` <. A , B >. ) a r ) <-> z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( z = ( ( 1st ` <. A , B >. ) a r ) <-> z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) ) with typecode |-
61	60	rexbidv	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) <-> E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) <-> E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) ) with typecode |-
62	61	abbidv	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } = { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } = { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) with typecode |-
63	58 62	uneq12d	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) = ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) = ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) with typecode |-
64	54 63	oveq12d	Could not format ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) ) = ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) ) = ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) ) with typecode |-
65		eqid	Could not format ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) = ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) : No typesetting found for |- ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) = ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) with typecode |-
66		ovex	Could not format ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) e. _V : No typesetting found for |- ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) e. _V with typecode |-
67	45 64 65 66	ovmpo	Could not format ( ( <. A , B >. e. _V /\ ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V ) -> ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) ) : No typesetting found for |- ( ( <. A , B >. e. _V /\ ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V ) -> ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) ) with typecode |-
68	3 20 67	mp2an	Could not format ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) : No typesetting found for |- ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) with typecode |-
69		op1stg	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to 1^{st}\left(⟨A,B⟩\right)=A$$
70	69	fveq2d	Could not format ( ( A e. No /\ B e. No ) -> ( _Left ` ( 1st ` <. A , B >. ) ) = ( _Left ` A ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( _Left ` ( 1st ` <. A , B >. ) ) = ( _Left ` A ) ) with typecode |-
71	70	eleq2d	Could not format ( ( A e. No /\ B e. No ) -> ( l e. ( _Left ` ( 1st ` <. A , B >. ) ) <-> l e. ( _Left ` A ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( l e. ( _Left ` ( 1st ` <. A , B >. ) ) <-> l e. ( _Left ` A ) ) ) with typecode |-
72		op2ndg	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to 2^{nd}\left(⟨A,B⟩\right)=B$$
73	72	adantr	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( 2nd ` <. A , B >. ) = B ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( 2nd ` <. A , B >. ) = B ) with typecode |-
74	73	oveq2d	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) ) with typecode |-
75		elun1	Could not format ( l e. ( _Left ` A ) -> l e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( l e. ( _Left ` A ) -> l e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
76		elun1	Could not format ( l e. ( ( _Left ` A ) u. ( _Right ` A ) ) -> l e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) : No typesetting found for |- ( l e. ( ( _Left ` A ) u. ( _Right ` A ) ) -> l e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) with typecode |-
77	75 76	syl	Could not format ( l e. ( _Left ` A ) -> l e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) : No typesetting found for |- ( l e. ( _Left ` A ) -> l e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) with typecode |-
78	77	adantl	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> l e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> l e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) with typecode |-
79		snidg	$$⊢B\in \mathrm{No}\to B\in \left\{B\right\}$$
80		elun2	Could not format ( B e. { B } -> B e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) : No typesetting found for |- ( B e. { B } -> B e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) with typecode |-
81	79 80	syl	Could not format ( B e. No -> B e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) : No typesetting found for |- ( B e. No -> B e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) with typecode |-
82	81	adantl	Could not format ( ( A e. No /\ B e. No ) -> B e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> B e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) with typecode |-
83	82	adantr	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> B e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> B e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) with typecode |-
84	78 83	opelxpd	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> <. l , B >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> <. l , B >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) ) with typecode |-
85		leftirr	Could not format -. A e. ( _Left ` A ) : No typesetting found for |- -. A e. ( _Left ` A ) with typecode |-
86	85	a1i	Could not format ( ( A e. No /\ B e. No ) -> -. A e. ( _Left ` A ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> -. A e. ( _Left ` A ) ) with typecode |-
87		eleq1	Could not format ( l = A -> ( l e. ( _Left ` A ) <-> A e. ( _Left ` A ) ) ) : No typesetting found for |- ( l = A -> ( l e. ( _Left ` A ) <-> A e. ( _Left ` A ) ) ) with typecode |-
88	87	notbid	Could not format ( l = A -> ( -. l e. ( _Left ` A ) <-> -. A e. ( _Left ` A ) ) ) : No typesetting found for |- ( l = A -> ( -. l e. ( _Left ` A ) <-> -. A e. ( _Left ` A ) ) ) with typecode |-
89	86 88	syl5ibrcom	Could not format ( ( A e. No /\ B e. No ) -> ( l = A -> -. l e. ( _Left ` A ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( l = A -> -. l e. ( _Left ` A ) ) ) with typecode |-
90	89	necon2ad	Could not format ( ( A e. No /\ B e. No ) -> ( l e. ( _Left ` A ) -> l =/= A ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( l e. ( _Left ` A ) -> l =/= A ) ) with typecode |-
91	90	imp	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> l =/= A ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> l =/= A ) with typecode |-
92	91	orcd	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( l =/= A \/ B =/= B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( l =/= A \/ B =/= B ) ) with typecode |-
93		simpr	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> l e. ( _Left ` A ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> l e. ( _Left ` A ) ) with typecode |-
94		simplr	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> B e. No ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> B e. No ) with typecode |-
95		opthneg	Could not format ( ( l e. ( _Left ` A ) /\ B e. No ) -> ( <. l , B >. =/= <. A , B >. <-> ( l =/= A \/ B =/= B ) ) ) : No typesetting found for |- ( ( l e. ( _Left ` A ) /\ B e. No ) -> ( <. l , B >. =/= <. A , B >. <-> ( l =/= A \/ B =/= B ) ) ) with typecode |-
96	93 94 95	syl2anc	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( <. l , B >. =/= <. A , B >. <-> ( l =/= A \/ B =/= B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( <. l , B >. =/= <. A , B >. <-> ( l =/= A \/ B =/= B ) ) ) with typecode |-
97	92 96	mpbird	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> <. l , B >. =/= <. A , B >. ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> <. l , B >. =/= <. A , B >. ) with typecode |-
98		eldifsn	Could not format ( <. l , B >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. l , B >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) /\ <. l , B >. =/= <. A , B >. ) ) : No typesetting found for |- ( <. l , B >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. l , B >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) /\ <. l , B >. =/= <. A , B >. ) ) with typecode |-
99	84 97 98	sylanbrc	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> <. l , B >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> <. l , B >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) with typecode |-
100	99	fvresd	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. l , B >. ) = ( +s ` <. l , B >. ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. l , B >. ) = ( +s ` <. l , B >. ) ) with typecode |-
101		df-ov	Could not format ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. l , B >. ) : No typesetting found for |- ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. l , B >. ) with typecode |-
102		df-ov	Could not format ( l +s B ) = ( +s ` <. l , B >. ) : No typesetting found for |- ( l +s B ) = ( +s ` <. l , B >. ) with typecode |-
103	100 101 102	3eqtr4g	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( l +s B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( l +s B ) ) with typecode |-
104	74 103	eqtrd	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( l +s B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( l +s B ) ) with typecode |-
105	104	eqeq2d	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( l +s B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` A ) ) -> ( y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( l +s B ) ) ) with typecode |-
106	71 105	sylbida	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` ( 1st ` <. A , B >. ) ) ) -> ( y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( l +s B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` ( 1st ` <. A , B >. ) ) ) -> ( y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( l +s B ) ) ) with typecode |-
107	70 106	rexeqbidva	Could not format ( ( A e. No /\ B e. No ) -> ( E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> E. l e. ( _Left ` A ) y = ( l +s B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> E. l e. ( _Left ` A ) y = ( l +s B ) ) ) with typecode |-
108	107	abbidv	Could not format ( ( A e. No /\ B e. No ) -> { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } = { y | E. l e. ( _Left ` A ) y = ( l +s B ) } ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } = { y | E. l e. ( _Left ` A ) y = ( l +s B ) } ) with typecode |-
109	72	fveq2d	Could not format ( ( A e. No /\ B e. No ) -> ( _Left ` ( 2nd ` <. A , B >. ) ) = ( _Left ` B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( _Left ` ( 2nd ` <. A , B >. ) ) = ( _Left ` B ) ) with typecode |-
110	109	eleq2d	Could not format ( ( A e. No /\ B e. No ) -> ( l e. ( _Left ` ( 2nd ` <. A , B >. ) ) <-> l e. ( _Left ` B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( l e. ( _Left ` ( 2nd ` <. A , B >. ) ) <-> l e. ( _Left ` B ) ) ) with typecode |-
111	69	adantr	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( 1st ` <. A , B >. ) = A ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( 1st ` <. A , B >. ) = A ) with typecode |-
112	111	oveq1d	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) with typecode |-
113		snidg	$$⊢A\in \mathrm{No}\to A\in \left\{A\right\}$$
114	113	adantr	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A\in \left\{A\right\}$$
115		elun2	Could not format ( A e. { A } -> A e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) : No typesetting found for |- ( A e. { A } -> A e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) with typecode |-
116	114 115	syl	Could not format ( ( A e. No /\ B e. No ) -> A e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> A e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) with typecode |-
117	116	adantr	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> A e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> A e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) with typecode |-
118		elun1	Could not format ( l e. ( _Left ` B ) -> l e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( l e. ( _Left ` B ) -> l e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
119		elun1	Could not format ( l e. ( ( _Left ` B ) u. ( _Right ` B ) ) -> l e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) : No typesetting found for |- ( l e. ( ( _Left ` B ) u. ( _Right ` B ) ) -> l e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) with typecode |-
120	118 119	syl	Could not format ( l e. ( _Left ` B ) -> l e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) : No typesetting found for |- ( l e. ( _Left ` B ) -> l e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) with typecode |-
121	120	adantl	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> l e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> l e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) with typecode |-
122	117 121	opelxpd	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> <. A , l >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> <. A , l >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) ) with typecode |-
123		leftirr	Could not format -. B e. ( _Left ` B ) : No typesetting found for |- -. B e. ( _Left ` B ) with typecode |-
124	123	a1i	Could not format ( ( A e. No /\ B e. No ) -> -. B e. ( _Left ` B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> -. B e. ( _Left ` B ) ) with typecode |-
125		eleq1	Could not format ( l = B -> ( l e. ( _Left ` B ) <-> B e. ( _Left ` B ) ) ) : No typesetting found for |- ( l = B -> ( l e. ( _Left ` B ) <-> B e. ( _Left ` B ) ) ) with typecode |-
126	125	notbid	Could not format ( l = B -> ( -. l e. ( _Left ` B ) <-> -. B e. ( _Left ` B ) ) ) : No typesetting found for |- ( l = B -> ( -. l e. ( _Left ` B ) <-> -. B e. ( _Left ` B ) ) ) with typecode |-
127	124 126	syl5ibrcom	Could not format ( ( A e. No /\ B e. No ) -> ( l = B -> -. l e. ( _Left ` B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( l = B -> -. l e. ( _Left ` B ) ) ) with typecode |-
128	127	necon2ad	Could not format ( ( A e. No /\ B e. No ) -> ( l e. ( _Left ` B ) -> l =/= B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( l e. ( _Left ` B ) -> l =/= B ) ) with typecode |-
129	128	imp	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> l =/= B ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> l =/= B ) with typecode |-
130	129	olcd	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( A =/= A \/ l =/= B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( A =/= A \/ l =/= B ) ) with typecode |-
131		opthneg	Could not format ( ( A e. No /\ l e. ( _Left ` B ) ) -> ( <. A , l >. =/= <. A , B >. <-> ( A =/= A \/ l =/= B ) ) ) : No typesetting found for |- ( ( A e. No /\ l e. ( _Left ` B ) ) -> ( <. A , l >. =/= <. A , B >. <-> ( A =/= A \/ l =/= B ) ) ) with typecode |-
132	131	adantlr	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( <. A , l >. =/= <. A , B >. <-> ( A =/= A \/ l =/= B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( <. A , l >. =/= <. A , B >. <-> ( A =/= A \/ l =/= B ) ) ) with typecode |-
133	130 132	mpbird	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> <. A , l >. =/= <. A , B >. ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> <. A , l >. =/= <. A , B >. ) with typecode |-
134		eldifsn	Could not format ( <. A , l >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. A , l >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) /\ <. A , l >. =/= <. A , B >. ) ) : No typesetting found for |- ( <. A , l >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. A , l >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) /\ <. A , l >. =/= <. A , B >. ) ) with typecode |-
135	122 133 134	sylanbrc	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> <. A , l >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> <. A , l >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) with typecode |-
136	135	fvresd	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , l >. ) = ( +s ` <. A , l >. ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , l >. ) = ( +s ` <. A , l >. ) ) with typecode |-
137		df-ov	Could not format ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , l >. ) : No typesetting found for |- ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , l >. ) with typecode |-
138		df-ov	Could not format ( A +s l ) = ( +s ` <. A , l >. ) : No typesetting found for |- ( A +s l ) = ( +s ` <. A , l >. ) with typecode |-
139	136 137 138	3eqtr4g	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A +s l ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A +s l ) ) with typecode |-
140	112 139	eqtrd	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A +s l ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A +s l ) ) with typecode |-
141	140	eqeq2d	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> z = ( A +s l ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` B ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> z = ( A +s l ) ) ) with typecode |-
142	110 141	sylbida	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` ( 2nd ` <. A , B >. ) ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> z = ( A +s l ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _Left ` ( 2nd ` <. A , B >. ) ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> z = ( A +s l ) ) ) with typecode |-
143	109 142	rexeqbidva	Could not format ( ( A e. No /\ B e. No ) -> ( E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> E. l e. ( _Left ` B ) z = ( A +s l ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> E. l e. ( _Left ` B ) z = ( A +s l ) ) ) with typecode |-
144	143	abbidv	Could not format ( ( A e. No /\ B e. No ) -> { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } = { z | E. l e. ( _Left ` B ) z = ( A +s l ) } ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } = { z | E. l e. ( _Left ` B ) z = ( A +s l ) } ) with typecode |-
145	108 144	uneq12d	Could not format ( ( A e. No /\ B e. No ) -> ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) = ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. l e. ( _Left ` B ) z = ( A +s l ) } ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) = ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. l e. ( _Left ` B ) z = ( A +s l ) } ) ) with typecode |-
146	69	fveq2d	Could not format ( ( A e. No /\ B e. No ) -> ( _Right ` ( 1st ` <. A , B >. ) ) = ( _Right ` A ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( _Right ` ( 1st ` <. A , B >. ) ) = ( _Right ` A ) ) with typecode |-
147	146	eleq2d	Could not format ( ( A e. No /\ B e. No ) -> ( r e. ( _Right ` ( 1st ` <. A , B >. ) ) <-> r e. ( _Right ` A ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( r e. ( _Right ` ( 1st ` <. A , B >. ) ) <-> r e. ( _Right ` A ) ) ) with typecode |-
148	72	adantr	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( 2nd ` <. A , B >. ) = B ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( 2nd ` <. A , B >. ) = B ) with typecode |-
149	148	oveq2d	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) ) with typecode |-
150		elun2	Could not format ( r e. ( _Right ` A ) -> r e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) : No typesetting found for |- ( r e. ( _Right ` A ) -> r e. ( ( _Left ` A ) u. ( _Right ` A ) ) ) with typecode |-
151		elun1	Could not format ( r e. ( ( _Left ` A ) u. ( _Right ` A ) ) -> r e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) : No typesetting found for |- ( r e. ( ( _Left ` A ) u. ( _Right ` A ) ) -> r e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) with typecode |-
152	150 151	syl	Could not format ( r e. ( _Right ` A ) -> r e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) : No typesetting found for |- ( r e. ( _Right ` A ) -> r e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) with typecode |-
153	152	adantl	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> r e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> r e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) with typecode |-
154	82	adantr	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> B e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> B e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) with typecode |-
155	153 154	opelxpd	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> <. r , B >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> <. r , B >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) ) with typecode |-
156		rightirr	Could not format -. A e. ( _Right ` A ) : No typesetting found for |- -. A e. ( _Right ` A ) with typecode |-
157	156	a1i	Could not format ( ( A e. No /\ B e. No ) -> -. A e. ( _Right ` A ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> -. A e. ( _Right ` A ) ) with typecode |-
158		eleq1	Could not format ( r = A -> ( r e. ( _Right ` A ) <-> A e. ( _Right ` A ) ) ) : No typesetting found for |- ( r = A -> ( r e. ( _Right ` A ) <-> A e. ( _Right ` A ) ) ) with typecode |-
159	158	notbid	Could not format ( r = A -> ( -. r e. ( _Right ` A ) <-> -. A e. ( _Right ` A ) ) ) : No typesetting found for |- ( r = A -> ( -. r e. ( _Right ` A ) <-> -. A e. ( _Right ` A ) ) ) with typecode |-
160	157 159	syl5ibrcom	Could not format ( ( A e. No /\ B e. No ) -> ( r = A -> -. r e. ( _Right ` A ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( r = A -> -. r e. ( _Right ` A ) ) ) with typecode |-
161	160	necon2ad	Could not format ( ( A e. No /\ B e. No ) -> ( r e. ( _Right ` A ) -> r =/= A ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( r e. ( _Right ` A ) -> r =/= A ) ) with typecode |-
162	161	imp	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> r =/= A ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> r =/= A ) with typecode |-
163	162	orcd	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( r =/= A \/ B =/= B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( r =/= A \/ B =/= B ) ) with typecode |-
164		simpr	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> r e. ( _Right ` A ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> r e. ( _Right ` A ) ) with typecode |-
165		simplr	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> B e. No ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> B e. No ) with typecode |-
166		opthneg	Could not format ( ( r e. ( _Right ` A ) /\ B e. No ) -> ( <. r , B >. =/= <. A , B >. <-> ( r =/= A \/ B =/= B ) ) ) : No typesetting found for |- ( ( r e. ( _Right ` A ) /\ B e. No ) -> ( <. r , B >. =/= <. A , B >. <-> ( r =/= A \/ B =/= B ) ) ) with typecode |-
167	164 165 166	syl2anc	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( <. r , B >. =/= <. A , B >. <-> ( r =/= A \/ B =/= B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( <. r , B >. =/= <. A , B >. <-> ( r =/= A \/ B =/= B ) ) ) with typecode |-
168	163 167	mpbird	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> <. r , B >. =/= <. A , B >. ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> <. r , B >. =/= <. A , B >. ) with typecode |-
169		eldifsn	Could not format ( <. r , B >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. r , B >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) /\ <. r , B >. =/= <. A , B >. ) ) : No typesetting found for |- ( <. r , B >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. r , B >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) /\ <. r , B >. =/= <. A , B >. ) ) with typecode |-
170	155 168 169	sylanbrc	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> <. r , B >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> <. r , B >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) with typecode |-
171	170	fvresd	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. r , B >. ) = ( +s ` <. r , B >. ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. r , B >. ) = ( +s ` <. r , B >. ) ) with typecode |-
172		df-ov	Could not format ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. r , B >. ) : No typesetting found for |- ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. r , B >. ) with typecode |-
173		df-ov	Could not format ( r +s B ) = ( +s ` <. r , B >. ) : No typesetting found for |- ( r +s B ) = ( +s ` <. r , B >. ) with typecode |-
174	171 172 173	3eqtr4g	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( r +s B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( r +s B ) ) with typecode |-
175	149 174	eqtrd	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( r +s B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( r +s B ) ) with typecode |-
176	175	eqeq2d	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( r +s B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` A ) ) -> ( y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( r +s B ) ) ) with typecode |-
177	147 176	sylbida	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` ( 1st ` <. A , B >. ) ) ) -> ( y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( r +s B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` ( 1st ` <. A , B >. ) ) ) -> ( y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( r +s B ) ) ) with typecode |-
178	146 177	rexeqbidva	Could not format ( ( A e. No /\ B e. No ) -> ( E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> E. r e. ( _Right ` A ) y = ( r +s B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> E. r e. ( _Right ` A ) y = ( r +s B ) ) ) with typecode |-
179	178	abbidv	Could not format ( ( A e. No /\ B e. No ) -> { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } = { y | E. r e. ( _Right ` A ) y = ( r +s B ) } ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } = { y | E. r e. ( _Right ` A ) y = ( r +s B ) } ) with typecode |-
180	72	fveq2d	Could not format ( ( A e. No /\ B e. No ) -> ( _Right ` ( 2nd ` <. A , B >. ) ) = ( _Right ` B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( _Right ` ( 2nd ` <. A , B >. ) ) = ( _Right ` B ) ) with typecode |-
181	180	eleq2d	Could not format ( ( A e. No /\ B e. No ) -> ( r e. ( _Right ` ( 2nd ` <. A , B >. ) ) <-> r e. ( _Right ` B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( r e. ( _Right ` ( 2nd ` <. A , B >. ) ) <-> r e. ( _Right ` B ) ) ) with typecode |-
182	69	adantr	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( 1st ` <. A , B >. ) = A ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( 1st ` <. A , B >. ) = A ) with typecode |-
183	182	oveq1d	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) with typecode |-
184	114	adantr	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> A e. { A } ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> A e. { A } ) with typecode |-
185	184 115	syl	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> A e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> A e. ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) ) with typecode |-
186		elun2	Could not format ( r e. ( _Right ` B ) -> r e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( r e. ( _Right ` B ) -> r e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
187	186	adantl	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> r e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> r e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
188		elun1	Could not format ( r e. ( ( _Left ` B ) u. ( _Right ` B ) ) -> r e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) : No typesetting found for |- ( r e. ( ( _Left ` B ) u. ( _Right ` B ) ) -> r e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) with typecode |-
189	187 188	syl	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> r e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> r e. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) with typecode |-
190	185 189	opelxpd	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> <. A , r >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> <. A , r >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) ) with typecode |-
191		rightirr	Could not format -. B e. ( _Right ` B ) : No typesetting found for |- -. B e. ( _Right ` B ) with typecode |-
192	191	a1i	Could not format ( ( A e. No /\ B e. No ) -> -. B e. ( _Right ` B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> -. B e. ( _Right ` B ) ) with typecode |-
193		eleq1	Could not format ( r = B -> ( r e. ( _Right ` B ) <-> B e. ( _Right ` B ) ) ) : No typesetting found for |- ( r = B -> ( r e. ( _Right ` B ) <-> B e. ( _Right ` B ) ) ) with typecode |-
194	193	notbid	Could not format ( r = B -> ( -. r e. ( _Right ` B ) <-> -. B e. ( _Right ` B ) ) ) : No typesetting found for |- ( r = B -> ( -. r e. ( _Right ` B ) <-> -. B e. ( _Right ` B ) ) ) with typecode |-
195	192 194	syl5ibrcom	Could not format ( ( A e. No /\ B e. No ) -> ( r = B -> -. r e. ( _Right ` B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( r = B -> -. r e. ( _Right ` B ) ) ) with typecode |-
196	195	necon2ad	Could not format ( ( A e. No /\ B e. No ) -> ( r e. ( _Right ` B ) -> r =/= B ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( r e. ( _Right ` B ) -> r =/= B ) ) with typecode |-
197	196	imp	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> r =/= B ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> r =/= B ) with typecode |-
198	197	olcd	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( A =/= A \/ r =/= B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( A =/= A \/ r =/= B ) ) with typecode |-
199		opthneg	Could not format ( ( A e. No /\ r e. ( _Right ` B ) ) -> ( <. A , r >. =/= <. A , B >. <-> ( A =/= A \/ r =/= B ) ) ) : No typesetting found for |- ( ( A e. No /\ r e. ( _Right ` B ) ) -> ( <. A , r >. =/= <. A , B >. <-> ( A =/= A \/ r =/= B ) ) ) with typecode |-
200	199	adantlr	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( <. A , r >. =/= <. A , B >. <-> ( A =/= A \/ r =/= B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( <. A , r >. =/= <. A , B >. <-> ( A =/= A \/ r =/= B ) ) ) with typecode |-
201	198 200	mpbird	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> <. A , r >. =/= <. A , B >. ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> <. A , r >. =/= <. A , B >. ) with typecode |-
202		eldifsn	Could not format ( <. A , r >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. A , r >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) /\ <. A , r >. =/= <. A , B >. ) ) : No typesetting found for |- ( <. A , r >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) <-> ( <. A , r >. e. ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) /\ <. A , r >. =/= <. A , B >. ) ) with typecode |-
203	190 201 202	sylanbrc	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> <. A , r >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> <. A , r >. e. ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) with typecode |-
204	203	fvresd	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , r >. ) = ( +s ` <. A , r >. ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , r >. ) = ( +s ` <. A , r >. ) ) with typecode |-
205		df-ov	Could not format ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , r >. ) : No typesetting found for |- ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , r >. ) with typecode |-
206		df-ov	Could not format ( A +s r ) = ( +s ` <. A , r >. ) : No typesetting found for |- ( A +s r ) = ( +s ` <. A , r >. ) with typecode |-
207	204 205 206	3eqtr4g	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A +s r ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( A ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A +s r ) ) with typecode |-
208	183 207	eqtrd	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A +s r ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A +s r ) ) with typecode |-
209	208	eqeq2d	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> z = ( A +s r ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` B ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> z = ( A +s r ) ) ) with typecode |-
210	181 209	sylbida	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` ( 2nd ` <. A , B >. ) ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> z = ( A +s r ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _Right ` ( 2nd ` <. A , B >. ) ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> z = ( A +s r ) ) ) with typecode |-
211	180 210	rexeqbidva	Could not format ( ( A e. No /\ B e. No ) -> ( E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> E. r e. ( _Right ` B ) z = ( A +s r ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> E. r e. ( _Right ` B ) z = ( A +s r ) ) ) with typecode |-
212	211	abbidv	Could not format ( ( A e. No /\ B e. No ) -> { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } = { z | E. r e. ( _Right ` B ) z = ( A +s r ) } ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } = { z | E. r e. ( _Right ` B ) z = ( A +s r ) } ) with typecode |-
213	179 212	uneq12d	Could not format ( ( A e. No /\ B e. No ) -> ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) = ( { y | E. r e. ( _Right ` A ) y = ( r +s B ) } u. { z | E. r e. ( _Right ` B ) z = ( A +s r ) } ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) = ( { y | E. r e. ( _Right ` A ) y = ( r +s B ) } u. { z | E. r e. ( _Right ` B ) z = ( A +s r ) } ) ) with typecode |-
214	145 213	oveq12d	Could not format ( ( A e. No /\ B e. No ) -> ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. l e. ( _Left ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _Right ` A ) y = ( r +s B ) } u. { z | E. r e. ( _Right ` B ) z = ( A +s r ) } ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( { y | E. l e. ( _Left ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. l e. ( _Left ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _Right ` A ) y = ( r +s B ) } u. { z | E. r e. ( _Right ` B ) z = ( A +s r ) } ) ) ) with typecode |-
215	68 214	eqtrid	Could not format ( ( A e. No /\ B e. No ) -> ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. l e. ( _Left ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _Right ` A ) y = ( r +s B ) } u. { z | E. r e. ( _Right ` B ) z = ( A +s r ) } ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _Left ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _Left ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _Right ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _Right ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _Left ` A ) u. ( _Right ` A ) ) u. { A } ) X. ( ( ( _Left ` B ) u. ( _Right ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. l e. ( _Left ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _Right ` A ) y = ( r +s B ) } u. { z | E. r e. ( _Right ` B ) z = ( A +s r ) } ) ) ) with typecode |-
216	2 215	eqtrd	Could not format ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. l e. ( _Left ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _Right ` A ) y = ( r +s B ) } u. { z | E. r e. ( _Right ` B ) z = ( A +s r ) } ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { y | E. l e. ( _Left ` A ) y = ( l +s B ) } u. { z | E. l e. ( _Left ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _Right ` A ) y = ( r +s B ) } u. { z | E. r e. ( _Right ` B ) z = ( A +s r ) } ) ) ) with typecode |-