Theorem addsov

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

	Ref	Expression
Assertion	addsov	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	$$⊢A\in \mathrm{No}\to \neg A\in L\left(A\right)$$
86	85	adantr	$$⊢\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	105	ex	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 |-
107	71 106	sylbid	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 |-
108	107	imp	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 |-
109	70 108	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 |-
110	109	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 |-
111	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)$$
112	111	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)$$
113	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$$
114	113	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 |-
115		snidg	$$⊢A\in \mathrm{No}\to A\in \left\{A\right\}$$
116	115	adantr	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to A\in \left\{A\right\}$$
117		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)$$
118	116 117	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)$$
119	118	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)$$
120		elun1	$$⊢l\in L\left(B\right)\to l\in \left(L\left(B\right)\cup R\left(B\right)\right)$$
121		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)$$
122	120 121	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)$$
123	122	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)$$
124	119 123	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)$$
125		leftirr	$$⊢B\in \mathrm{No}\to \neg B\in L\left(B\right)$$
126	125	adantl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \neg B\in L\left(B\right)$$
127		eleq1	$$⊢l=B\to \left(l\in L\left(B\right)\leftrightarrow B\in L\left(B\right)\right)$$
128	127	notbid	$$⊢l=B\to \left(\neg l\in L\left(B\right)\leftrightarrow \neg B\in L\left(B\right)\right)$$
129	126 128	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)$$
130	129	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)$$
131	130	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$$
132	131	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)$$
133		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)$$
134	133	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)$$
135	132 134	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⟩$$
136		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)$$
137	124 135 136	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)$$
138	137	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 |-
139		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 |-
140		df-ov	Could not format ( A +s l ) = ( +s ` <. A , l >. ) : No typesetting found for |- ( A +s l ) = ( +s ` <. A , l >. ) with typecode |-
141	138 139 140	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 |-
142	114 141	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 |-
143	142	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 |-
144	143	ex	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 |-
145	112 144	sylbid	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 |-
146	145	imp	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 |-
147	111 146	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 |-
148	147	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 |-
149	110 148	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 |-
150	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)$$
151	150	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)$$
152	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$$
153	152	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 |-
154		elun2	$$⊢r\in R\left(A\right)\to r\in \left(L\left(A\right)\cup R\left(A\right)\right)$$
155		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)$$
156	154 155	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)$$
157	156	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)$$
158	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)$$
159	157 158	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)$$
160		rightirr	$$⊢A\in \mathrm{No}\to \neg A\in R\left(A\right)$$
161	160	adantr	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \neg A\in R\left(A\right)$$
162		eleq1	$$⊢r=A\to \left(r\in R\left(A\right)\leftrightarrow A\in R\left(A\right)\right)$$
163	162	notbid	$$⊢r=A\to \left(\neg r\in R\left(A\right)\leftrightarrow \neg A\in R\left(A\right)\right)$$
164	161 163	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)$$
165	164	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)$$
166	165	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$$
167	166	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)$$
168		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)$$
169		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}$$
170		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)$$
171	168 169 170	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)$$
172	167 171	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⟩$$
173		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)$$
174	159 172 173	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)$$
175	174	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 |-
176		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 |-
177		df-ov	Could not format ( r +s B ) = ( +s ` <. r , B >. ) : No typesetting found for |- ( r +s B ) = ( +s ` <. r , B >. ) with typecode |-
178	175 176 177	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 |-
179	153 178	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 |-
180	179	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 |-
181	180	ex	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 |-
182	151 181	sylbid	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 |-
183	182	imp	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 |-
184	150 183	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 |-
185	184	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 |-
186	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)$$
187	186	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)$$
188	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$$
189	188	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 |-
190	116	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\}$$
191	190 117	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)$$
192		elun2	$$⊢r\in R\left(B\right)\to r\in \left(L\left(B\right)\cup R\left(B\right)\right)$$
193	192	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)$$
194		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)$$
195	193 194	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)$$
196	191 195	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)$$
197		rightirr	$$⊢B\in \mathrm{No}\to \neg B\in R\left(B\right)$$
198	197	adantl	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \neg B\in R\left(B\right)$$
199		eleq1	$$⊢r=B\to \left(r\in R\left(B\right)\leftrightarrow B\in R\left(B\right)\right)$$
200	199	notbid	$$⊢r=B\to \left(\neg r\in R\left(B\right)\leftrightarrow \neg B\in R\left(B\right)\right)$$
201	198 200	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)$$
202	201	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)$$
203	202	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$$
204	203	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)$$
205		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)$$
206	205	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)$$
207	204 206	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⟩$$
208		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)$$
209	196 207 208	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)$$
210	209	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 |-
211		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 |-
212		df-ov	Could not format ( A +s r ) = ( +s ` <. A , r >. ) : No typesetting found for |- ( A +s r ) = ( +s ` <. A , r >. ) with typecode |-
213	210 211 212	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 |-
214	189 213	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 |-
215	214	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 |-
216	215	ex	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 |-
217	187 216	sylbid	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 |-
218	217	imp	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 |-
219	186 218	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 |-
220	219	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 |-
221	185 220	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 |-
222	149 221	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 |-
223	68 222	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 |-
224	2 223	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 |-