Theorem mulsrid

Description: Surreal one is a right identity element for multiplication. (Contributed by Scott Fenton, 4-Feb-2025)

	Ref	Expression
Assertion	mulsrid	Could not format assertion : No typesetting found for |- ( A e. No -> ( A x.s 1s ) = A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		oveq1	Could not format ( x = xO -> ( x x.s 1s ) = ( xO x.s 1s ) ) : No typesetting found for |- ( x = xO -> ( x x.s 1s ) = ( xO x.s 1s ) ) with typecode |-
2		id	Could not format ( x = xO -> x = xO ) : No typesetting found for |- ( x = xO -> x = xO ) with typecode |-
3	1 2	eqeq12d	Could not format ( x = xO -> ( ( x x.s 1s ) = x <-> ( xO x.s 1s ) = xO ) ) : No typesetting found for |- ( x = xO -> ( ( x x.s 1s ) = x <-> ( xO x.s 1s ) = xO ) ) with typecode |-
4		oveq1	Could not format ( x = A -> ( x x.s 1s ) = ( A x.s 1s ) ) : No typesetting found for |- ( x = A -> ( x x.s 1s ) = ( A x.s 1s ) ) with typecode |-
5		id	$$⊢x=A\to x=A$$
6	4 5	eqeq12d	Could not format ( x = A -> ( ( x x.s 1s ) = x <-> ( A x.s 1s ) = A ) ) : No typesetting found for |- ( x = A -> ( ( x x.s 1s ) = x <-> ( A x.s 1s ) = A ) ) with typecode |-
7		1sno	Could not format 1s e. No : No typesetting found for |- 1s e. No with typecode |-
8		mulsval	Could not format ( ( x e. No /\ 1s e. No ) -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) : No typesetting found for |- ( ( x e. No /\ 1s e. No ) -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) with typecode |-
9	7 8	mpan2	Could not format ( x e. No -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) : No typesetting found for |- ( x e. No -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) with typecode |-
10	9	adantr	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) ) with typecode |-
11		elun1	Could not format ( p e. ( _Left ` x ) -> p e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( p e. ( _Left ` x ) -> p e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
12		oveq1	Could not format ( xO = p -> ( xO x.s 1s ) = ( p x.s 1s ) ) : No typesetting found for |- ( xO = p -> ( xO x.s 1s ) = ( p x.s 1s ) ) with typecode |-
13		id	Could not format ( xO = p -> xO = p ) : No typesetting found for |- ( xO = p -> xO = p ) with typecode |-
14	12 13	eqeq12d	Could not format ( xO = p -> ( ( xO x.s 1s ) = xO <-> ( p x.s 1s ) = p ) ) : No typesetting found for |- ( xO = p -> ( ( xO x.s 1s ) = xO <-> ( p x.s 1s ) = p ) ) with typecode |-
15	14	rspcva	Could not format ( ( p e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( p e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) with typecode |-
16	11 15	sylan	Could not format ( ( p e. ( _Left ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( p e. ( _Left ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( p x.s 1s ) = p ) with typecode |-
17	16	ancoms	Could not format ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) with typecode |-
18	17	adantll	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 1s ) = p ) with typecode |-
19		muls01	Could not format ( x e. No -> ( x x.s 0s ) = 0s ) : No typesetting found for |- ( x e. No -> ( x x.s 0s ) = 0s ) with typecode |-
20	19	adantr	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 0s ) = 0s ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 0s ) = 0s ) with typecode |-
21	20	adantr	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( x x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( x x.s 0s ) = 0s ) with typecode |-
22	18 21	oveq12d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = ( p +s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = ( p +s 0s ) ) with typecode |-
23		leftssno	Could not format ( _Left ` x ) C_ No : No typesetting found for |- ( _Left ` x ) C_ No with typecode |-
24	23	sseli	Could not format ( p e. ( _Left ` x ) -> p e. No ) : No typesetting found for |- ( p e. ( _Left ` x ) -> p e. No ) with typecode |-
25	24	adantl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> p e. No ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> p e. No ) with typecode |-
26	25	addsridd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p +s 0s ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p +s 0s ) = p ) with typecode |-
27	22 26	eqtrd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( p x.s 1s ) +s ( x x.s 0s ) ) = p ) with typecode |-
28		muls01	Could not format ( p e. No -> ( p x.s 0s ) = 0s ) : No typesetting found for |- ( p e. No -> ( p x.s 0s ) = 0s ) with typecode |-
29	25 28	syl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p x.s 0s ) = 0s ) with typecode |-
30	27 29	oveq12d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = ( p -s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = ( p -s 0s ) ) with typecode |-
31		subsid1	Could not format ( p e. No -> ( p -s 0s ) = p ) : No typesetting found for |- ( p e. No -> ( p -s 0s ) = p ) with typecode |-
32	25 31	syl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p -s 0s ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( p -s 0s ) = p ) with typecode |-
33	30 32	eqtrd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = p ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) = p ) with typecode |-
34	33	eqeq2d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> a = p ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> a = p ) ) with typecode |-
35		equcom	$$⊢a=p\leftrightarrow p=a$$
36	34 35	bitrdi	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> p = a ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ p e. ( _Left ` x ) ) -> ( a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> p = a ) ) with typecode |-
37	36	rexbidva	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> E. p e. ( _Left ` x ) p = a ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) <-> E. p e. ( _Left ` x ) p = a ) ) with typecode |-
38		left1s	Could not format ( _Left ` 1s ) = { 0s } : No typesetting found for |- ( _Left ` 1s ) = { 0s } with typecode |-
39	38	rexeqi	Could not format ( E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. q e. { 0s } a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) ) : No typesetting found for |- ( E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. q e. { 0s } a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) ) with typecode |-
40		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
41	40	elexi	Could not format 0s e. _V : No typesetting found for |- 0s e. _V with typecode |-
42		oveq2	Could not format ( q = 0s -> ( x x.s q ) = ( x x.s 0s ) ) : No typesetting found for |- ( q = 0s -> ( x x.s q ) = ( x x.s 0s ) ) with typecode |-
43	42	oveq2d	Could not format ( q = 0s -> ( ( p x.s 1s ) +s ( x x.s q ) ) = ( ( p x.s 1s ) +s ( x x.s 0s ) ) ) : No typesetting found for |- ( q = 0s -> ( ( p x.s 1s ) +s ( x x.s q ) ) = ( ( p x.s 1s ) +s ( x x.s 0s ) ) ) with typecode |-
44		oveq2	Could not format ( q = 0s -> ( p x.s q ) = ( p x.s 0s ) ) : No typesetting found for |- ( q = 0s -> ( p x.s q ) = ( p x.s 0s ) ) with typecode |-
45	43 44	oveq12d	Could not format ( q = 0s -> ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) ) : No typesetting found for |- ( q = 0s -> ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) ) with typecode |-
46	45	eqeq2d	Could not format ( q = 0s -> ( a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) ) ) : No typesetting found for |- ( q = 0s -> ( a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) ) ) with typecode |-
47	41 46	rexsn	Could not format ( E. q e. { 0s } a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) ) : No typesetting found for |- ( E. q e. { 0s } a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) ) with typecode |-
48	39 47	bitri	Could not format ( E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) ) : No typesetting found for |- ( E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) ) with typecode |-
49	48	rexbii	Could not format ( E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` x ) a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) ) : No typesetting found for |- ( E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> E. p e. ( _Left ` x ) a = ( ( ( p x.s 1s ) +s ( x x.s 0s ) ) -s ( p x.s 0s ) ) ) with typecode |-
50		risset	Could not format ( a e. ( _Left ` x ) <-> E. p e. ( _Left ` x ) p = a ) : No typesetting found for |- ( a e. ( _Left ` x ) <-> E. p e. ( _Left ` x ) p = a ) with typecode |-
51	37 49 50	3bitr4g	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a e. ( _Left ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) <-> a e. ( _Left ` x ) ) ) with typecode |-
52	51	eqabcdv	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } = ( _Left ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } = ( _Left ` x ) ) with typecode |-
53		rex0	Could not format -. E. s e. (/) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) : No typesetting found for |- -. E. s e. (/) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) with typecode |-
54		right1s	Could not format ( _Right ` 1s ) = (/) : No typesetting found for |- ( _Right ` 1s ) = (/) with typecode |-
55	54	rexeqi	Could not format ( E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> E. s e. (/) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) ) : No typesetting found for |- ( E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) <-> E. s e. (/) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) ) with typecode |-
56	53 55	mtbir	Could not format -. E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) : No typesetting found for |- -. E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) with typecode |-
57	56	a1i	Could not format ( r e. ( _Right ` x ) -> -. E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) ) : No typesetting found for |- ( r e. ( _Right ` x ) -> -. E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) ) with typecode |-
58	57	nrex	Could not format -. E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) : No typesetting found for |- -. E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) with typecode |-
59	58	abf	Could not format { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = (/) : No typesetting found for |- { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = (/) with typecode |-
60	59	a1i	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = (/) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } = (/) ) with typecode |-
61	52 60	uneq12d	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( ( _Left ` x ) u. (/) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( ( _Left ` x ) u. (/) ) ) with typecode |-
62		un0	Could not format ( ( _Left ` x ) u. (/) ) = ( _Left ` x ) : No typesetting found for |- ( ( _Left ` x ) u. (/) ) = ( _Left ` x ) with typecode |-
63	61 62	eqtrdi	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( _Left ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) = ( _Left ` x ) ) with typecode |-
64		rex0	Could not format -. E. u e. (/) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) : No typesetting found for |- -. E. u e. (/) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) with typecode |-
65	54	rexeqi	Could not format ( E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> E. u e. (/) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) ) : No typesetting found for |- ( E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) <-> E. u e. (/) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) ) with typecode |-
66	64 65	mtbir	Could not format -. E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) : No typesetting found for |- -. E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) with typecode |-
67	66	a1i	Could not format ( t e. ( _Left ` x ) -> -. E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) ) : No typesetting found for |- ( t e. ( _Left ` x ) -> -. E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) ) with typecode |-
68	67	nrex	Could not format -. E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) : No typesetting found for |- -. E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) with typecode |-
69	68	abf	Could not format { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = (/) : No typesetting found for |- { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = (/) with typecode |-
70	69	a1i	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = (/) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } = (/) ) with typecode |-
71		elun2	Could not format ( v e. ( _Right ` x ) -> v e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) : No typesetting found for |- ( v e. ( _Right ` x ) -> v e. ( ( _Left ` x ) u. ( _Right ` x ) ) ) with typecode |-
72		oveq1	Could not format ( xO = v -> ( xO x.s 1s ) = ( v x.s 1s ) ) : No typesetting found for |- ( xO = v -> ( xO x.s 1s ) = ( v x.s 1s ) ) with typecode |-
73		id	Could not format ( xO = v -> xO = v ) : No typesetting found for |- ( xO = v -> xO = v ) with typecode |-
74	72 73	eqeq12d	Could not format ( xO = v -> ( ( xO x.s 1s ) = xO <-> ( v x.s 1s ) = v ) ) : No typesetting found for |- ( xO = v -> ( ( xO x.s 1s ) = xO <-> ( v x.s 1s ) = v ) ) with typecode |-
75	74	rspcva	Could not format ( ( v e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( v e. ( ( _Left ` x ) u. ( _Right ` x ) ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) with typecode |-
76	71 75	sylan	Could not format ( ( v e. ( _Right ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( v e. ( _Right ` x ) /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( v x.s 1s ) = v ) with typecode |-
77	76	ancoms	Could not format ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) with typecode |-
78	77	adantll	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 1s ) = v ) with typecode |-
79	20	adantr	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( x x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( x x.s 0s ) = 0s ) with typecode |-
80	78 79	oveq12d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = ( v +s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = ( v +s 0s ) ) with typecode |-
81		rightssno	Could not format ( _Right ` x ) C_ No : No typesetting found for |- ( _Right ` x ) C_ No with typecode |-
82	81	sseli	Could not format ( v e. ( _Right ` x ) -> v e. No ) : No typesetting found for |- ( v e. ( _Right ` x ) -> v e. No ) with typecode |-
83	82	adantl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> v e. No ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> v e. No ) with typecode |-
84	83	addsridd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v +s 0s ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v +s 0s ) = v ) with typecode |-
85	80 84	eqtrd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( v x.s 1s ) +s ( x x.s 0s ) ) = v ) with typecode |-
86		muls01	Could not format ( v e. No -> ( v x.s 0s ) = 0s ) : No typesetting found for |- ( v e. No -> ( v x.s 0s ) = 0s ) with typecode |-
87	83 86	syl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 0s ) = 0s ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v x.s 0s ) = 0s ) with typecode |-
88	85 87	oveq12d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = ( v -s 0s ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = ( v -s 0s ) ) with typecode |-
89		subsid1	Could not format ( v e. No -> ( v -s 0s ) = v ) : No typesetting found for |- ( v e. No -> ( v -s 0s ) = v ) with typecode |-
90	83 89	syl	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v -s 0s ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( v -s 0s ) = v ) with typecode |-
91	88 90	eqtrd	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = v ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) = v ) with typecode |-
92	91	eqeq2d	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) <-> d = v ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) <-> d = v ) ) with typecode |-
93	38	rexeqi	Could not format ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. w e. { 0s } d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) ) : No typesetting found for |- ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. w e. { 0s } d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) ) with typecode |-
94		oveq2	Could not format ( w = 0s -> ( x x.s w ) = ( x x.s 0s ) ) : No typesetting found for |- ( w = 0s -> ( x x.s w ) = ( x x.s 0s ) ) with typecode |-
95	94	oveq2d	Could not format ( w = 0s -> ( ( v x.s 1s ) +s ( x x.s w ) ) = ( ( v x.s 1s ) +s ( x x.s 0s ) ) ) : No typesetting found for |- ( w = 0s -> ( ( v x.s 1s ) +s ( x x.s w ) ) = ( ( v x.s 1s ) +s ( x x.s 0s ) ) ) with typecode |-
96		oveq2	Could not format ( w = 0s -> ( v x.s w ) = ( v x.s 0s ) ) : No typesetting found for |- ( w = 0s -> ( v x.s w ) = ( v x.s 0s ) ) with typecode |-
97	95 96	oveq12d	Could not format ( w = 0s -> ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) ) : No typesetting found for |- ( w = 0s -> ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) ) with typecode |-
98	97	eqeq2d	Could not format ( w = 0s -> ( d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) ) ) : No typesetting found for |- ( w = 0s -> ( d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) ) ) with typecode |-
99	41 98	rexsn	Could not format ( E. w e. { 0s } d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) ) : No typesetting found for |- ( E. w e. { 0s } d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) ) with typecode |-
100	93 99	bitri	Could not format ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) ) : No typesetting found for |- ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d = ( ( ( v x.s 1s ) +s ( x x.s 0s ) ) -s ( v x.s 0s ) ) ) with typecode |-
101		equcom	$$⊢v=d\leftrightarrow d=v$$
102	92 100 101	3bitr4g	Could not format ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> v = d ) ) : No typesetting found for |- ( ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) /\ v e. ( _Right ` x ) ) -> ( E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> v = d ) ) with typecode |-
103	102	rexbidva	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` x ) v = d ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> E. v e. ( _Right ` x ) v = d ) ) with typecode |-
104		risset	Could not format ( d e. ( _Right ` x ) <-> E. v e. ( _Right ` x ) v = d ) : No typesetting found for |- ( d e. ( _Right ` x ) <-> E. v e. ( _Right ` x ) v = d ) with typecode |-
105	103 104	bitr4di	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d e. ( _Right ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) <-> d e. ( _Right ` x ) ) ) with typecode |-
106	105	eqabcdv	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } = ( _Right ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } = ( _Right ` x ) ) with typecode |-
107	70 106	uneq12d	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( (/) u. ( _Right ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( (/) u. ( _Right ` x ) ) ) with typecode |-
108		0un	Could not format ( (/) u. ( _Right ` x ) ) = ( _Right ` x ) : No typesetting found for |- ( (/) u. ( _Right ` x ) ) = ( _Right ` x ) with typecode |-
109	107 108	eqtrdi	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( _Right ` x ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) = ( _Right ` x ) ) with typecode |-
110	63 109	oveq12d	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) = ( ( _Left ` x ) |s ( _Right ` x ) ) ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( { a | E. p e. ( _Left ` x ) E. q e. ( _Left ` 1s ) a = ( ( ( p x.s 1s ) +s ( x x.s q ) ) -s ( p x.s q ) ) } u. { b | E. r e. ( _Right ` x ) E. s e. ( _Right ` 1s ) b = ( ( ( r x.s 1s ) +s ( x x.s s ) ) -s ( r x.s s ) ) } ) |s ( { c | E. t e. ( _Left ` x ) E. u e. ( _Right ` 1s ) c = ( ( ( t x.s 1s ) +s ( x x.s u ) ) -s ( t x.s u ) ) } u. { d | E. v e. ( _Right ` x ) E. w e. ( _Left ` 1s ) d = ( ( ( v x.s 1s ) +s ( x x.s w ) ) -s ( v x.s w ) ) } ) ) = ( ( _Left ` x ) |s ( _Right ` x ) ) ) with typecode |-
111		lrcut	Could not format ( x e. No -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) : No typesetting found for |- ( x e. No -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) with typecode |-
112	111	adantr	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) with typecode |-
113	10 110 112	3eqtrd	Could not format ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = x ) : No typesetting found for |- ( ( x e. No /\ A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO ) -> ( x x.s 1s ) = x ) with typecode |-
114	113	ex	Could not format ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO -> ( x x.s 1s ) = x ) ) : No typesetting found for |- ( x e. No -> ( A. xO e. ( ( _Left ` x ) u. ( _Right ` x ) ) ( xO x.s 1s ) = xO -> ( x x.s 1s ) = x ) ) with typecode |-
115	3 6 114	noinds	Could not format ( A e. No -> ( A x.s 1s ) = A ) : No typesetting found for |- ( A e. No -> ( A x.s 1s ) = A ) with typecode |-