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. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` 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. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ) : No typesetting found for |- +s = norec2 ( ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 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. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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	$$⊢L\left(A\right)\in \mathrm{V}$$
8		fvex	$$⊢R\left(A\right)\in \mathrm{V}$$
9	7 8	unex	$$⊢L\left(A\right)\cup R\left(A\right)\in \mathrm{V}$$
10		snex	$$⊢\left\{A\right\}\in \mathrm{V}$$
11	9 10	unex	$$⊢\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\in \mathrm{V}$$
12		fvex	$$⊢L\left(B\right)\in \mathrm{V}$$
13		fvex	$$⊢R\left(B\right)\in \mathrm{V}$$
14	12 13	unex	$$⊢L\left(B\right)\cup R\left(B\right)\in \mathrm{V}$$
15		snex	$$⊢\left\{B\right\}\in \mathrm{V}$$
16	14 15	unex	$$⊢\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\in \mathrm{V}$$
17	11 16	xpex	$$⊢\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\in \mathrm{V}$$
18	17	difexi	$$⊢\left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\setminus \left\{⟨A,B⟩\right\}\in \mathrm{V}$$
19		resfunexg	Could not format ( ( Fun +s /\ ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) e. _V ) -> ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V ) : No typesetting found for |- ( ( Fun +s /\ ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) e. _V ) -> ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V ) with typecode |-
20	6 18 19	mp2an	Could not format ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V : No typesetting found for |- ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V with typecode |-
21		2fveq3	$$⊢x=⟨A,B⟩\to L\left(1^{st}\left(x\right)\right)=L\left(1^{st}\left(⟨A,B⟩\right)\right)$$
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	$$⊢x=⟨A,B⟩\to \left(\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)\leftrightarrow \exists l\in L\left(1^{st}\left(⟨A,B⟩\right)\right)y=la{2}^{nd}\left(⟨A,B⟩\right)\right)$$
26	25	abbidv	$$⊢x=⟨A,B⟩\to \left\{y|\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)\right\}=\left\{y|\exists l\in L\left(1^{st}\left(⟨A,B⟩\right)\right)y=la{2}^{nd}\left(⟨A,B⟩\right)\right\}$$
27		2fveq3	$$⊢x=⟨A,B⟩\to L\left(2^{nd}\left(x\right)\right)=L\left(2^{nd}\left(⟨A,B⟩\right)\right)$$
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	$$⊢x=⟨A,B⟩\to \left(\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al\leftrightarrow \exists l\in L\left(2^{nd}\left(⟨A,B⟩\right)\right)z=1^{st}\left(⟨A,B⟩\right)al\right)$$
32	31	abbidv	$$⊢x=⟨A,B⟩\to \left\{z|\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al\right\}=\left\{z|\exists l\in L\left(2^{nd}\left(⟨A,B⟩\right)\right)z=1^{st}\left(⟨A,B⟩\right)al\right\}$$
33	26 32	uneq12d	$$⊢x=⟨A,B⟩\to \left\{y|\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al\right\}=\left\{y|\exists l\in L\left(1^{st}\left(⟨A,B⟩\right)\right)y=la{2}^{nd}\left(⟨A,B⟩\right)\right\}\cup \left\{z|\exists l\in L\left(2^{nd}\left(⟨A,B⟩\right)\right)z=1^{st}\left(⟨A,B⟩\right)al\right\}$$
34		2fveq3	$$⊢x=⟨A,B⟩\to R\left(1^{st}\left(x\right)\right)=R\left(1^{st}\left(⟨A,B⟩\right)\right)$$
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	$$⊢x=⟨A,B⟩\to \left(\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)\leftrightarrow \exists r\in R\left(1^{st}\left(⟨A,B⟩\right)\right)y=ra{2}^{nd}\left(⟨A,B⟩\right)\right)$$
38	37	abbidv	$$⊢x=⟨A,B⟩\to \left\{y|\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)\right\}=\left\{y|\exists r\in R\left(1^{st}\left(⟨A,B⟩\right)\right)y=ra{2}^{nd}\left(⟨A,B⟩\right)\right\}$$
39		2fveq3	$$⊢x=⟨A,B⟩\to R\left(2^{nd}\left(x\right)\right)=R\left(2^{nd}\left(⟨A,B⟩\right)\right)$$
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	$$⊢x=⟨A,B⟩\to \left(\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar\leftrightarrow \exists r\in R\left(2^{nd}\left(⟨A,B⟩\right)\right)z=1^{st}\left(⟨A,B⟩\right)ar\right)$$
43	42	abbidv	$$⊢x=⟨A,B⟩\to \left\{z|\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar\right\}=\left\{z|\exists r\in R\left(2^{nd}\left(⟨A,B⟩\right)\right)z=1^{st}\left(⟨A,B⟩\right)ar\right\}$$
44	38 43	uneq12d	$$⊢x=⟨A,B⟩\to \left\{y|\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar\right\}=\left\{y|\exists r\in R\left(1^{st}\left(⟨A,B⟩\right)\right)y=ra{2}^{nd}\left(⟨A,B⟩\right)\right\}\cup \left\{z|\exists r\in R\left(2^{nd}\left(⟨A,B⟩\right)\right)z=1^{st}\left(⟨A,B⟩\right)ar\right\}$$
45	33 44	oveq12d	$$⊢x=⟨A,B⟩\to \left(\left\{y|\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al\right\}\right){|}_s\left(\left\{y|\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar\right\}\right)=\left(\left\{y|\exists l\in L\left(1^{st}\left(⟨A,B⟩\right)\right)y=la{2}^{nd}\left(⟨A,B⟩\right)\right\}\cup \left\{z|\exists l\in L\left(2^{nd}\left(⟨A,B⟩\right)\right)z=1^{st}\left(⟨A,B⟩\right)al\right\}\right){|}_s\left(\left\{y|\exists r\in R\left(1^{st}\left(⟨A,B⟩\right)\right)y=ra{2}^{nd}\left(⟨A,B⟩\right)\right\}\cup \left\{z|\exists r\in R\left(2^{nd}\left(⟨A,B⟩\right)\right)z=1^{st}\left(⟨A,B⟩\right)ar\right\}\right)$$
46		oveq	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( l a ( 2nd ` <. A , B >. ) ) = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( l a ( 2nd ` <. A , B >. ) ) = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) with typecode |-
47	46	eqeq2d	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( y = ( l a ( 2nd ` <. A , B >. ) ) <-> y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( y = ( l a ( 2nd ` <. A , B >. ) ) <-> y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) with typecode |-
48	47	rexbidv	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) <-> E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) <-> E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) with typecode |-
49	48	abbidv	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } = { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } = { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } ) with typecode |-
50		oveq	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( 1st ` <. A , B >. ) a l ) = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( 1st ` <. A , B >. ) a l ) = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) with typecode |-
51	50	eqeq2d	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( z = ( ( 1st ` <. A , B >. ) a l ) <-> z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( z = ( ( 1st ` <. A , B >. ) a l ) <-> z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) ) with typecode |-
52	51	rexbidv	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) <-> E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) <-> E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) ) with typecode |-
53	52	abbidv	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } = { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } = { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) with typecode |-
54	49 53	uneq12d	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) = ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) = ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) ) with typecode |-
55		oveq	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( r a ( 2nd ` <. A , B >. ) ) = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( r a ( 2nd ` <. A , B >. ) ) = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) with typecode |-
56	55	eqeq2d	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( y = ( r a ( 2nd ` <. A , B >. ) ) <-> y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( y = ( r a ( 2nd ` <. A , B >. ) ) <-> y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) with typecode |-
57	56	rexbidv	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) <-> E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) <-> E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) ) ) with typecode |-
58	57	abbidv	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } = { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } = { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } ) with typecode |-
59		oveq	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( 1st ` <. A , B >. ) a r ) = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( 1st ` <. A , B >. ) a r ) = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) with typecode |-
60	59	eqeq2d	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( z = ( ( 1st ` <. A , B >. ) a r ) <-> z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( z = ( ( 1st ` <. A , B >. ) a r ) <-> z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) ) with typecode |-
61	60	rexbidv	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) <-> E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) <-> E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) ) with typecode |-
62	61	abbidv	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } = { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } = { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) with typecode |-
63	58 62	uneq12d	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) = ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) = ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) with typecode |-
64	54 63	oveq12d	Could not format ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) ) = ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) ) : No typesetting found for |- ( a = ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) -> ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l a ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r a ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) a r ) } ) ) = ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) ) with typecode |-
65		eqid	$$⊢\left(x\in \mathrm{V},a\in \mathrm{V}⟼\left(\left\{y|\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al\right\}\right){|}_s\left(\left\{y|\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar\right\}\right)\right)=\left(x\in \mathrm{V},a\in \mathrm{V}⟼\left(\left\{y|\exists l\in L\left(1^{st}\left(x\right)\right)y=la{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists l\in L\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)al\right\}\right){|}_s\left(\left\{y|\exists r\in R\left(1^{st}\left(x\right)\right)y=ra{2}^{nd}\left(x\right)\right\}\cup \left\{z|\exists r\in R\left(2^{nd}\left(x\right)\right)z=1^{st}\left(x\right)ar\right\}\right)\right)$$
66		ovex	Could not format ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) e. _V : No typesetting found for |- ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) e. _V with typecode |-
67	45 64 65 66	ovmpo	Could not format ( ( <. A , B >. e. _V /\ ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V ) -> ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) ) : No typesetting found for |- ( ( <. A , B >. e. _V /\ ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) e. _V ) -> ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) : No typesetting found for |- ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to L\left(1^{st}\left(⟨A,B⟩\right)\right)=L\left(A\right)$$
71	70	eleq2d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(l\in L\left(1^{st}\left(⟨A,B⟩\right)\right)\leftrightarrow l\in L\left(A\right)\right)$$
72		op2ndg	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to 2^{nd}\left(⟨A,B⟩\right)=B$$
73	72	adantr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(A\right)\right)\to 2^{nd}\left(⟨A,B⟩\right)=B$$
74	73	oveq2d	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) ) with typecode |-
75		elun1	$$⊢l\in L\left(A\right)\to l\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
76		elun1	$$⊢l\in \left(L\left(A\right)\cup R\left(A\right)\right)\to l\in \left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)$$
77	75 76	syl	$$⊢l\in L\left(A\right)\to l\in \left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)$$
78	77	adantl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(A\right)\right)\to l\in \left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)$$
79		snidg	$$⊢B\in \mathrm{No}\to B\in \left\{B\right\}$$
80		elun2	$$⊢B\in \left\{B\right\}\to B\in \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)$$
81	79 80	syl	$$⊢B\in \mathrm{No}\to B\in \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)$$
82	81	adantl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to B\in \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)$$
83	82	adantr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(A\right)\right)\to B\in \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)$$
84	78 83	opelxpd	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(A\right)\right)\to ⟨l,B⟩\in \left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)$$
85		leftirr	$$⊢\neg A\in L\left(A\right)$$
86	85	a1i	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \neg A\in L\left(A\right)$$
87		eleq1	$$⊢l=A\to \left(l\in L\left(A\right)\leftrightarrow A\in L\left(A\right)\right)$$
88	87	notbid	$$⊢l=A\to \left(\neg l\in L\left(A\right)\leftrightarrow \neg A\in L\left(A\right)\right)$$
89	86 88	syl5ibrcom	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(l=A\to \neg l\in L\left(A\right)\right)$$
90	89	necon2ad	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(l\in L\left(A\right)\to l\ne A\right)$$
91	90	imp	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(A\right)\right)\to l\ne A$$
92	91	orcd	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(A\right)\right)\to \left(l\ne A\vee B\ne B\right)$$
93		simpr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(A\right)\right)\to l\in L\left(A\right)$$
94		simplr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(A\right)\right)\to B\in \mathrm{No}$$
95		opthneg	$$⊢\left(l\in L\left(A\right)\wedge B\in \mathrm{No}\right)\to \left(⟨l,B⟩\ne ⟨A,B⟩\leftrightarrow \left(l\ne A\vee B\ne B\right)\right)$$
96	93 94 95	syl2anc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(A\right)\right)\to \left(⟨l,B⟩\ne ⟨A,B⟩\leftrightarrow \left(l\ne A\vee B\ne B\right)\right)$$
97	92 96	mpbird	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(A\right)\right)\to ⟨l,B⟩\ne ⟨A,B⟩$$
98		eldifsn	$$⊢⟨l,B⟩\in \left(\left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\setminus \left\{⟨A,B⟩\right\}\right)\leftrightarrow \left(⟨l,B⟩\in \left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\wedge ⟨l,B⟩\ne ⟨A,B⟩\right)$$
99	84 97 98	sylanbrc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(A\right)\right)\to ⟨l,B⟩\in \left(\left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\setminus \left\{⟨A,B⟩\right\}\right)$$
100	99	fvresd	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. l , B >. ) = ( +s ` <. l , B >. ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. l , B >. ) = ( +s ` <. l , B >. ) ) with typecode |-
101		df-ov	Could not format ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. l , B >. ) : No typesetting found for |- ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` A ) ) -> ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( l +s B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` A ) ) -> ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( l +s B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` A ) ) -> ( y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( l +s B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` A ) ) -> ( y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` ( 1st ` <. A , B >. ) ) ) -> ( y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( l +s B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` ( 1st ` <. A , B >. ) ) ) -> ( y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> E. l e. ( _L ` A ) y = ( l +s B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> E. l e. ( _L ` A ) y = ( l +s B ) ) ) with typecode |-
108	107	abbidv	Could not format ( ( A e. No /\ B e. No ) -> { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } = { y | E. l e. ( _L ` A ) y = ( l +s B ) } ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } = { y | E. l e. ( _L ` A ) y = ( l +s B ) } ) with typecode |-
109	72	fveq2d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to L\left(2^{nd}\left(⟨A,B⟩\right)\right)=L\left(B\right)$$
110	109	eleq2d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(l\in L\left(2^{nd}\left(⟨A,B⟩\right)\right)\leftrightarrow l\in L\left(B\right)\right)$$
111	69	adantr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(B\right)\right)\to 1^{st}\left(⟨A,B⟩\right)=A$$
112	111	oveq1d	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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	$$⊢A\in \left\{A\right\}\to A\in \left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)$$
116	114 115	syl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A\in \left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)$$
117	116	adantr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(B\right)\right)\to A\in \left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)$$
118		elun1	$$⊢l\in L\left(B\right)\to l\in \left(L\left(B\right)\cup R\left(B\right)\right)$$
119		elun1	$$⊢l\in \left(L\left(B\right)\cup R\left(B\right)\right)\to l\in \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)$$
120	118 119	syl	$$⊢l\in L\left(B\right)\to l\in \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)$$
121	120	adantl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(B\right)\right)\to l\in \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)$$
122	117 121	opelxpd	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(B\right)\right)\to ⟨A,l⟩\in \left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)$$
123		leftirr	$$⊢\neg B\in L\left(B\right)$$
124	123	a1i	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \neg B\in L\left(B\right)$$
125		eleq1	$$⊢l=B\to \left(l\in L\left(B\right)\leftrightarrow B\in L\left(B\right)\right)$$
126	125	notbid	$$⊢l=B\to \left(\neg l\in L\left(B\right)\leftrightarrow \neg B\in L\left(B\right)\right)$$
127	124 126	syl5ibrcom	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(l=B\to \neg l\in L\left(B\right)\right)$$
128	127	necon2ad	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(l\in L\left(B\right)\to l\ne B\right)$$
129	128	imp	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(B\right)\right)\to l\ne B$$
130	129	olcd	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(B\right)\right)\to \left(A\ne A\vee l\ne B\right)$$
131		opthneg	$$⊢\left(A\in \mathrm{No}\wedge l\in L\left(B\right)\right)\to \left(⟨A,l⟩\ne ⟨A,B⟩\leftrightarrow \left(A\ne A\vee l\ne B\right)\right)$$
132	131	adantlr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(B\right)\right)\to \left(⟨A,l⟩\ne ⟨A,B⟩\leftrightarrow \left(A\ne A\vee l\ne B\right)\right)$$
133	130 132	mpbird	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(B\right)\right)\to ⟨A,l⟩\ne ⟨A,B⟩$$
134		eldifsn	$$⊢⟨A,l⟩\in \left(\left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\setminus \left\{⟨A,B⟩\right\}\right)\leftrightarrow \left(⟨A,l⟩\in \left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\wedge ⟨A,l⟩\ne ⟨A,B⟩\right)$$
135	122 133 134	sylanbrc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge l\in L\left(B\right)\right)\to ⟨A,l⟩\in \left(\left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\setminus \left\{⟨A,B⟩\right\}\right)$$
136	135	fvresd	Could not format ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , l >. ) = ( +s ` <. A , l >. ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , l >. ) = ( +s ` <. A , l >. ) ) with typecode |-
137		df-ov	Could not format ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , l >. ) : No typesetting found for |- ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` B ) ) -> ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A +s l ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) = ( A +s l ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` B ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> z = ( A +s l ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` B ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` ( 2nd ` <. A , B >. ) ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> z = ( A +s l ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ l e. ( _L ` ( 2nd ` <. A , B >. ) ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> E. l e. ( _L ` B ) z = ( A +s l ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) <-> E. l e. ( _L ` B ) z = ( A +s l ) ) ) with typecode |-
144	143	abbidv	Could not format ( ( A e. No /\ B e. No ) -> { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } = { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } = { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) with typecode |-
145	108 144	uneq12d	Could not format ( ( A e. No /\ B e. No ) -> ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) = ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) = ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) ) with typecode |-
146	69	fveq2d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to R\left(1^{st}\left(⟨A,B⟩\right)\right)=R\left(A\right)$$
147	146	eleq2d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(r\in R\left(1^{st}\left(⟨A,B⟩\right)\right)\leftrightarrow r\in R\left(A\right)\right)$$
148	72	adantr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(A\right)\right)\to 2^{nd}\left(⟨A,B⟩\right)=B$$
149	148	oveq2d	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) ) with typecode |-
150		elun2	$$⊢r\in R\left(A\right)\to r\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
151		elun1	$$⊢r\in \left(L\left(A\right)\cup R\left(A\right)\right)\to r\in \left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)$$
152	150 151	syl	$$⊢r\in R\left(A\right)\to r\in \left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)$$
153	152	adantl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(A\right)\right)\to r\in \left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)$$
154	82	adantr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(A\right)\right)\to B\in \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)$$
155	153 154	opelxpd	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(A\right)\right)\to ⟨r,B⟩\in \left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)$$
156		rightirr	$$⊢\neg A\in R\left(A\right)$$
157	156	a1i	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \neg A\in R\left(A\right)$$
158		eleq1	$$⊢r=A\to \left(r\in R\left(A\right)\leftrightarrow A\in R\left(A\right)\right)$$
159	158	notbid	$$⊢r=A\to \left(\neg r\in R\left(A\right)\leftrightarrow \neg A\in R\left(A\right)\right)$$
160	157 159	syl5ibrcom	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(r=A\to \neg r\in R\left(A\right)\right)$$
161	160	necon2ad	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(r\in R\left(A\right)\to r\ne A\right)$$
162	161	imp	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(A\right)\right)\to r\ne A$$
163	162	orcd	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(A\right)\right)\to \left(r\ne A\vee B\ne B\right)$$
164		simpr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(A\right)\right)\to r\in R\left(A\right)$$
165		simplr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(A\right)\right)\to B\in \mathrm{No}$$
166		opthneg	$$⊢\left(r\in R\left(A\right)\wedge B\in \mathrm{No}\right)\to \left(⟨r,B⟩\ne ⟨A,B⟩\leftrightarrow \left(r\ne A\vee B\ne B\right)\right)$$
167	164 165 166	syl2anc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(A\right)\right)\to \left(⟨r,B⟩\ne ⟨A,B⟩\leftrightarrow \left(r\ne A\vee B\ne B\right)\right)$$
168	163 167	mpbird	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(A\right)\right)\to ⟨r,B⟩\ne ⟨A,B⟩$$
169		eldifsn	$$⊢⟨r,B⟩\in \left(\left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\setminus \left\{⟨A,B⟩\right\}\right)\leftrightarrow \left(⟨r,B⟩\in \left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\wedge ⟨r,B⟩\ne ⟨A,B⟩\right)$$
170	155 168 169	sylanbrc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(A\right)\right)\to ⟨r,B⟩\in \left(\left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\setminus \left\{⟨A,B⟩\right\}\right)$$
171	170	fvresd	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. r , B >. ) = ( +s ` <. r , B >. ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. r , B >. ) = ( +s ` <. r , B >. ) ) with typecode |-
172		df-ov	Could not format ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. r , B >. ) : No typesetting found for |- ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _R ` A ) ) -> ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) B ) = ( r +s B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _R ` A ) ) -> ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) = ( r +s B ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _R ` A ) ) -> ( y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( r +s B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` A ) ) -> ( y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _R ` ( 1st ` <. A , B >. ) ) ) -> ( y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> y = ( r +s B ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` ( 1st ` <. A , B >. ) ) ) -> ( y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> E. r e. ( _R ` A ) y = ( r +s B ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) <-> E. r e. ( _R ` A ) y = ( r +s B ) ) ) with typecode |-
179	178	abbidv	Could not format ( ( A e. No /\ B e. No ) -> { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } = { y | E. r e. ( _R ` A ) y = ( r +s B ) } ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } = { y | E. r e. ( _R ` A ) y = ( r +s B ) } ) with typecode |-
180	72	fveq2d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to R\left(2^{nd}\left(⟨A,B⟩\right)\right)=R\left(B\right)$$
181	180	eleq2d	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(r\in R\left(2^{nd}\left(⟨A,B⟩\right)\right)\leftrightarrow r\in R\left(B\right)\right)$$
182	69	adantr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(B\right)\right)\to 1^{st}\left(⟨A,B⟩\right)=A$$
183	182	oveq1d	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) ) with typecode |-
184	114	adantr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(B\right)\right)\to A\in \left\{A\right\}$$
185	184 115	syl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(B\right)\right)\to A\in \left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)$$
186		elun2	$$⊢r\in R\left(B\right)\to r\in \left(L\left(B\right)\cup R\left(B\right)\right)$$
187	186	adantl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(B\right)\right)\to r\in \left(L\left(B\right)\cup R\left(B\right)\right)$$
188		elun1	$$⊢r\in \left(L\left(B\right)\cup R\left(B\right)\right)\to r\in \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)$$
189	187 188	syl	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(B\right)\right)\to r\in \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)$$
190	185 189	opelxpd	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(B\right)\right)\to ⟨A,r⟩\in \left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)$$
191		rightirr	$$⊢\neg B\in R\left(B\right)$$
192	191	a1i	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \neg B\in R\left(B\right)$$
193		eleq1	$$⊢r=B\to \left(r\in R\left(B\right)\leftrightarrow B\in R\left(B\right)\right)$$
194	193	notbid	$$⊢r=B\to \left(\neg r\in R\left(B\right)\leftrightarrow \neg B\in R\left(B\right)\right)$$
195	192 194	syl5ibrcom	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(r=B\to \neg r\in R\left(B\right)\right)$$
196	195	necon2ad	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \left(r\in R\left(B\right)\to r\ne B\right)$$
197	196	imp	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(B\right)\right)\to r\ne B$$
198	197	olcd	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(B\right)\right)\to \left(A\ne A\vee r\ne B\right)$$
199		opthneg	$$⊢\left(A\in \mathrm{No}\wedge r\in R\left(B\right)\right)\to \left(⟨A,r⟩\ne ⟨A,B⟩\leftrightarrow \left(A\ne A\vee r\ne B\right)\right)$$
200	199	adantlr	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(B\right)\right)\to \left(⟨A,r⟩\ne ⟨A,B⟩\leftrightarrow \left(A\ne A\vee r\ne B\right)\right)$$
201	198 200	mpbird	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(B\right)\right)\to ⟨A,r⟩\ne ⟨A,B⟩$$
202		eldifsn	$$⊢⟨A,r⟩\in \left(\left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\setminus \left\{⟨A,B⟩\right\}\right)\leftrightarrow \left(⟨A,r⟩\in \left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\wedge ⟨A,r⟩\ne ⟨A,B⟩\right)$$
203	190 201 202	sylanbrc	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge r\in R\left(B\right)\right)\to ⟨A,r⟩\in \left(\left(\left(\left(L\left(A\right)\cup R\left(A\right)\right)\cup \left\{A\right\}\right)\times \left(\left(L\left(B\right)\cup R\left(B\right)\right)\cup \left\{B\right\}\right)\right)\setminus \left\{⟨A,B⟩\right\}\right)$$
204	203	fvresd	Could not format ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , r >. ) = ( +s ` <. A , r >. ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , r >. ) = ( +s ` <. A , r >. ) ) with typecode |-
205		df-ov	Could not format ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ` <. A , r >. ) : No typesetting found for |- ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _R ` B ) ) -> ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A +s r ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( A ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _R ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) = ( A +s r ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _R ` B ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> z = ( A +s r ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` B ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _R ` ( 2nd ` <. A , B >. ) ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> z = ( A +s r ) ) ) : No typesetting found for |- ( ( ( A e. No /\ B e. No ) /\ r e. ( _R ` ( 2nd ` <. A , B >. ) ) ) -> ( z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` 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. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> E. r e. ( _R ` B ) z = ( A +s r ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) <-> E. r e. ( _R ` B ) z = ( A +s r ) ) ) with typecode |-
212	211	abbidv	Could not format ( ( A e. No /\ B e. No ) -> { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } = { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } = { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) with typecode |-
213	179 212	uneq12d	Could not format ( ( A e. No /\ B e. No ) -> ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) = ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) = ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) ) with typecode |-
214	145 213	oveq12d	Could not format ( ( A e. No /\ B e. No ) -> ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) = ( ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( ( { y | E. l e. ( _L ` ( 1st ` <. A , B >. ) ) y = ( l ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. l e. ( _L ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` <. A , B >. ) ) y = ( r ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ( 2nd ` <. A , B >. ) ) } u. { z | E. r e. ( _R ` ( 2nd ` <. A , B >. ) ) z = ( ( 1st ` <. A , B >. ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) r ) } ) ) = ( ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) ) ) with typecode |-
215	68 214	syl5eq	Could not format ( ( A e. No /\ B e. No ) -> ( <. A , B >. ( x e. _V , a e. _V |-> ( ( { y | E. l e. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` 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. ( _L ` ( 1st ` x ) ) y = ( l a ( 2nd ` x ) ) } u. { z | E. l e. ( _L ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a l ) } ) |s ( { y | E. r e. ( _R ` ( 1st ` x ) ) y = ( r a ( 2nd ` x ) ) } u. { z | E. r e. ( _R ` ( 2nd ` x ) ) z = ( ( 1st ` x ) a r ) } ) ) ) ( +s |` ( ( ( ( ( _L ` A ) u. ( _R ` A ) ) u. { A } ) X. ( ( ( _L ` B ) u. ( _R ` B ) ) u. { B } ) ) \ { <. A , B >. } ) ) ) = ( ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` 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. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) ) ) : No typesetting found for |- ( ( A e. No /\ B e. No ) -> ( A +s B ) = ( ( { y | E. l e. ( _L ` A ) y = ( l +s B ) } u. { z | E. l e. ( _L ` B ) z = ( A +s l ) } ) |s ( { y | E. r e. ( _R ` A ) y = ( r +s B ) } u. { z | E. r e. ( _R ` B ) z = ( A +s r ) } ) ) ) with typecode |-