Theorem negsproplem2

Description: Lemma for surreal negation. Show that the cut that defines negation is legitimate. (Contributed by Scott Fenton, 2-Feb-2025)

	Ref	Expression
Hypotheses	negsproplem.1	No typesetting found for |- ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
	negsproplem2.1	$$⊢\phi \to A\in \mathrm{No}$$
Assertion	negsproplem2	Could not format assertion : No typesetting found for |- ( ph -> ( -us " ( _Right ` A ) ) <

Proof

Step	Hyp	Ref	Expression
1		negsproplem.1	Could not format ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
2		negsproplem2.1	$$⊢\phi \to A\in \mathrm{No}$$
3		negsfn	Could not format -us Fn No : No typesetting found for |- -us Fn No with typecode |-
4		fnfun	Could not format ( -us Fn No -> Fun -us ) : No typesetting found for |- ( -us Fn No -> Fun -us ) with typecode |-
5	3 4	ax-mp	Could not format Fun -us : No typesetting found for |- Fun -us with typecode |-
6		fvex	Could not format ( _Right ` A ) e. _V : No typesetting found for |- ( _Right ` A ) e. _V with typecode |-
7	6	funimaex	Could not format ( Fun -us -> ( -us " ( _Right ` A ) ) e. _V ) : No typesetting found for |- ( Fun -us -> ( -us " ( _Right ` A ) ) e. _V ) with typecode |-
8	5 7	mp1i	Could not format ( ph -> ( -us " ( _Right ` A ) ) e. _V ) : No typesetting found for |- ( ph -> ( -us " ( _Right ` A ) ) e. _V ) with typecode |-
9		fvex	Could not format ( _Left ` A ) e. _V : No typesetting found for |- ( _Left ` A ) e. _V with typecode |-
10	9	funimaex	Could not format ( Fun -us -> ( -us " ( _Left ` A ) ) e. _V ) : No typesetting found for |- ( Fun -us -> ( -us " ( _Left ` A ) ) e. _V ) with typecode |-
11	5 10	mp1i	Could not format ( ph -> ( -us " ( _Left ` A ) ) e. _V ) : No typesetting found for |- ( ph -> ( -us " ( _Left ` A ) ) e. _V ) with typecode |-
12		rightssold	Could not format ( _Right ` A ) C_ ( _Old ` ( bday ` A ) ) : No typesetting found for |- ( _Right ` A ) C_ ( _Old ` ( bday ` A ) ) with typecode |-
13		imass2	Could not format ( ( _Right ` A ) C_ ( _Old ` ( bday ` A ) ) -> ( -us " ( _Right ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) ) ) : No typesetting found for |- ( ( _Right ` A ) C_ ( _Old ` ( bday ` A ) ) -> ( -us " ( _Right ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) ) ) with typecode |-
14	12 13	ax-mp	Could not format ( -us " ( _Right ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( -us " ( _Right ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) ) with typecode |-
15	1	adantr	Could not format ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
16		oldssno	$$⊢\mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\subseteq \mathrm{No}$$
17	16	sseli	$$⊢a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\to a\in \mathrm{No}$$
18	17	adantl	$$⊢\left(\phi \wedge a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right)\to a\in \mathrm{No}$$
19		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
20	19	a1i	Could not format ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> 0s e. No ) : No typesetting found for |- ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> 0s e. No ) with typecode |-
21		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
22	21	uneq2i	Could not format ( ( bday ` a ) u. ( bday ` 0s ) ) = ( ( bday ` a ) u. (/) ) : No typesetting found for |- ( ( bday ` a ) u. ( bday ` 0s ) ) = ( ( bday ` a ) u. (/) ) with typecode |-
23		un0	$$⊢\mathrm{bday}\left(a\right)\cup \varnothing =\mathrm{bday}\left(a\right)$$
24	22 23	eqtri	Could not format ( ( bday ` a ) u. ( bday ` 0s ) ) = ( bday ` a ) : No typesetting found for |- ( ( bday ` a ) u. ( bday ` 0s ) ) = ( bday ` a ) with typecode |-
25		oldbdayim	$$⊢a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\to \mathrm{bday}\left(a\right)\in \mathrm{bday}\left(A\right)$$
26	25	adantl	$$⊢\left(\phi \wedge a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right)\to \mathrm{bday}\left(a\right)\in \mathrm{bday}\left(A\right)$$
27		elun1	$$⊢\mathrm{bday}\left(a\right)\in \mathrm{bday}\left(A\right)\to \mathrm{bday}\left(a\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)$$
28	26 27	syl	$$⊢\left(\phi \wedge a\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\right)\to \mathrm{bday}\left(a\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)$$
29	24 28	eqeltrid	Could not format ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> ( ( bday ` a ) u. ( bday ` 0s ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) : No typesetting found for |- ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> ( ( bday ` a ) u. ( bday ` 0s ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) with typecode |-
30	15 18 20 29	negsproplem1	Could not format ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> ( ( -us ` a ) e. No /\ ( a ( -us ` 0s ) ( ( -us ` a ) e. No /\ ( a ( -us ` 0s )
31	30	simpld	Could not format ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> ( -us ` a ) e. No ) : No typesetting found for |- ( ( ph /\ a e. ( _Old ` ( bday ` A ) ) ) -> ( -us ` a ) e. No ) with typecode |-
32	31	ralrimiva	Could not format ( ph -> A. a e. ( _Old ` ( bday ` A ) ) ( -us ` a ) e. No ) : No typesetting found for |- ( ph -> A. a e. ( _Old ` ( bday ` A ) ) ( -us ` a ) e. No ) with typecode |-
33	3	fndmi	Could not format dom -us = No : No typesetting found for |- dom -us = No with typecode |-
34	16 33	sseqtrri	Could not format ( _Old ` ( bday ` A ) ) C_ dom -us : No typesetting found for |- ( _Old ` ( bday ` A ) ) C_ dom -us with typecode |-
35		funimass4	Could not format ( ( Fun -us /\ ( _Old ` ( bday ` A ) ) C_ dom -us ) -> ( ( -us " ( _Old ` ( bday ` A ) ) ) C_ No <-> A. a e. ( _Old ` ( bday ` A ) ) ( -us ` a ) e. No ) ) : No typesetting found for |- ( ( Fun -us /\ ( _Old ` ( bday ` A ) ) C_ dom -us ) -> ( ( -us " ( _Old ` ( bday ` A ) ) ) C_ No <-> A. a e. ( _Old ` ( bday ` A ) ) ( -us ` a ) e. No ) ) with typecode |-
36	5 34 35	mp2an	Could not format ( ( -us " ( _Old ` ( bday ` A ) ) ) C_ No <-> A. a e. ( _Old ` ( bday ` A ) ) ( -us ` a ) e. No ) : No typesetting found for |- ( ( -us " ( _Old ` ( bday ` A ) ) ) C_ No <-> A. a e. ( _Old ` ( bday ` A ) ) ( -us ` a ) e. No ) with typecode |-
37	32 36	sylibr	Could not format ( ph -> ( -us " ( _Old ` ( bday ` A ) ) ) C_ No ) : No typesetting found for |- ( ph -> ( -us " ( _Old ` ( bday ` A ) ) ) C_ No ) with typecode |-
38	14 37	sstrid	Could not format ( ph -> ( -us " ( _Right ` A ) ) C_ No ) : No typesetting found for |- ( ph -> ( -us " ( _Right ` A ) ) C_ No ) with typecode |-
39		leftssold	Could not format ( _Left ` A ) C_ ( _Old ` ( bday ` A ) ) : No typesetting found for |- ( _Left ` A ) C_ ( _Old ` ( bday ` A ) ) with typecode |-
40		imass2	Could not format ( ( _Left ` A ) C_ ( _Old ` ( bday ` A ) ) -> ( -us " ( _Left ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) ) ) : No typesetting found for |- ( ( _Left ` A ) C_ ( _Old ` ( bday ` A ) ) -> ( -us " ( _Left ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) ) ) with typecode |-
41	39 40	ax-mp	Could not format ( -us " ( _Left ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( -us " ( _Left ` A ) ) C_ ( -us " ( _Old ` ( bday ` A ) ) ) with typecode |-
42	41 37	sstrid	Could not format ( ph -> ( -us " ( _Left ` A ) ) C_ No ) : No typesetting found for |- ( ph -> ( -us " ( _Left ` A ) ) C_ No ) with typecode |-
43		rightssno	Could not format ( _Right ` A ) C_ No : No typesetting found for |- ( _Right ` A ) C_ No with typecode |-
44		fvelimab	Could not format ( ( -us Fn No /\ ( _Right ` A ) C_ No ) -> ( a e. ( -us " ( _Right ` A ) ) <-> E. xR e. ( _Right ` A ) ( -us ` xR ) = a ) ) : No typesetting found for |- ( ( -us Fn No /\ ( _Right ` A ) C_ No ) -> ( a e. ( -us " ( _Right ` A ) ) <-> E. xR e. ( _Right ` A ) ( -us ` xR ) = a ) ) with typecode |-
45	3 43 44	mp2an	Could not format ( a e. ( -us " ( _Right ` A ) ) <-> E. xR e. ( _Right ` A ) ( -us ` xR ) = a ) : No typesetting found for |- ( a e. ( -us " ( _Right ` A ) ) <-> E. xR e. ( _Right ` A ) ( -us ` xR ) = a ) with typecode |-
46		leftssno	Could not format ( _Left ` A ) C_ No : No typesetting found for |- ( _Left ` A ) C_ No with typecode |-
47		fvelimab	Could not format ( ( -us Fn No /\ ( _Left ` A ) C_ No ) -> ( b e. ( -us " ( _Left ` A ) ) <-> E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) : No typesetting found for |- ( ( -us Fn No /\ ( _Left ` A ) C_ No ) -> ( b e. ( -us " ( _Left ` A ) ) <-> E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) with typecode |-
48	3 46 47	mp2an	Could not format ( b e. ( -us " ( _Left ` A ) ) <-> E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) : No typesetting found for |- ( b e. ( -us " ( _Left ` A ) ) <-> E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) with typecode |-
49	45 48	anbi12i	Could not format ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) <-> ( E. xR e. ( _Right ` A ) ( -us ` xR ) = a /\ E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) : No typesetting found for |- ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) <-> ( E. xR e. ( _Right ` A ) ( -us ` xR ) = a /\ E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) with typecode |-
50		reeanv	Could not format ( E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) <-> ( E. xR e. ( _Right ` A ) ( -us ` xR ) = a /\ E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) : No typesetting found for |- ( E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) <-> ( E. xR e. ( _Right ` A ) ( -us ` xR ) = a /\ E. xL e. ( _Left ` A ) ( -us ` xL ) = b ) ) with typecode |-
51	49 50	bitr4i	Could not format ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) <-> E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) ) : No typesetting found for |- ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) <-> E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) ) with typecode |-
52		lltropt	Could not format ( _Left ` A ) <
53	52	a1i	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( _Left ` A ) < ( _Left ` A ) <
54		simprr	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. ( _Left ` A ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. ( _Left ` A ) ) with typecode |-
55		simprl	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. ( _Right ` A ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. ( _Right ` A ) ) with typecode |-
56	53 54 55	ssltsepcd	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL xL
57	1	adantr	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
58	46	sseli	Could not format ( xL e. ( _Left ` A ) -> xL e. No ) : No typesetting found for |- ( xL e. ( _Left ` A ) -> xL e. No ) with typecode |-
59	58	ad2antll	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. No ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. No ) with typecode |-
60	43	sseli	Could not format ( xR e. ( _Right ` A ) -> xR e. No ) : No typesetting found for |- ( xR e. ( _Right ` A ) -> xR e. No ) with typecode |-
61	60	adantr	Could not format ( ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) -> xR e. No ) : No typesetting found for |- ( ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) -> xR e. No ) with typecode |-
62	61	adantl	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. No ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. No ) with typecode |-
63	39	sseli	Could not format ( xL e. ( _Left ` A ) -> xL e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( xL e. ( _Left ` A ) -> xL e. ( _Old ` ( bday ` A ) ) ) with typecode |-
64	63	ad2antll	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xL e. ( _Old ` ( bday ` A ) ) ) with typecode |-
65		oldbdayim	Could not format ( xL e. ( _Old ` ( bday ` A ) ) -> ( bday ` xL ) e. ( bday ` A ) ) : No typesetting found for |- ( xL e. ( _Old ` ( bday ` A ) ) -> ( bday ` xL ) e. ( bday ` A ) ) with typecode |-
66	64 65	syl	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( bday ` xL ) e. ( bday ` A ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( bday ` xL ) e. ( bday ` A ) ) with typecode |-
67	12	a1i	Could not format ( ph -> ( _Right ` A ) C_ ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ph -> ( _Right ` A ) C_ ( _Old ` ( bday ` A ) ) ) with typecode |-
68	67	sselda	Could not format ( ( ph /\ xR e. ( _Right ` A ) ) -> xR e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ( ph /\ xR e. ( _Right ` A ) ) -> xR e. ( _Old ` ( bday ` A ) ) ) with typecode |-
69	68	adantrr	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> xR e. ( _Old ` ( bday ` A ) ) ) with typecode |-
70		oldbdayim	Could not format ( xR e. ( _Old ` ( bday ` A ) ) -> ( bday ` xR ) e. ( bday ` A ) ) : No typesetting found for |- ( xR e. ( _Old ` ( bday ` A ) ) -> ( bday ` xR ) e. ( bday ` A ) ) with typecode |-
71	69 70	syl	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( bday ` xR ) e. ( bday ` A ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( bday ` xR ) e. ( bday ` A ) ) with typecode |-
72		bdayelon	Could not format ( bday ` xL ) e. On : No typesetting found for |- ( bday ` xL ) e. On with typecode |-
73		bdayelon	Could not format ( bday ` xR ) e. On : No typesetting found for |- ( bday ` xR ) e. On with typecode |-
74		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
75		onunel	Could not format ( ( ( bday ` xL ) e. On /\ ( bday ` xR ) e. On /\ ( bday ` A ) e. On ) -> ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) <-> ( ( bday ` xL ) e. ( bday ` A ) /\ ( bday ` xR ) e. ( bday ` A ) ) ) ) : No typesetting found for |- ( ( ( bday ` xL ) e. On /\ ( bday ` xR ) e. On /\ ( bday ` A ) e. On ) -> ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) <-> ( ( bday ` xL ) e. ( bday ` A ) /\ ( bday ` xR ) e. ( bday ` A ) ) ) ) with typecode |-
76	72 73 74 75	mp3an	Could not format ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) <-> ( ( bday ` xL ) e. ( bday ` A ) /\ ( bday ` xR ) e. ( bday ` A ) ) ) : No typesetting found for |- ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) <-> ( ( bday ` xL ) e. ( bday ` A ) /\ ( bday ` xR ) e. ( bday ` A ) ) ) with typecode |-
77	66 71 76	sylanbrc	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) ) with typecode |-
78		elun1	Could not format ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) : No typesetting found for |- ( ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( bday ` A ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) with typecode |-
79	77 78	syl	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) : No typesetting found for |- ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( bday ` xL ) u. ( bday ` xR ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) with typecode |-
80	57 59 62 79	negsproplem1	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( -us ` xL ) e. No /\ ( xL ( -us ` xR ) ( ( -us ` xL ) e. No /\ ( xL ( -us ` xR )
81	80	simprd	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( xL ( -us ` xR ) ( xL ( -us ` xR )
82	56 81	mpd	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( -us ` xR ) ( -us ` xR )
83		breq12	Could not format ( ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> ( ( -us ` xR ) a ( ( -us ` xR ) a
84	82 83	syl5ibcom	Could not format ( ( ph /\ ( xR e. ( _Right ` A ) /\ xL e. ( _Left ` A ) ) ) -> ( ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> a ( ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> a
85	84	rexlimdvva	Could not format ( ph -> ( E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> a ( E. xR e. ( _Right ` A ) E. xL e. ( _Left ` A ) ( ( -us ` xR ) = a /\ ( -us ` xL ) = b ) -> a
86	51 85	biimtrid	Could not format ( ph -> ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) -> a ( ( a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) -> a
87	86	3impib	Could not format ( ( ph /\ a e. ( -us " ( _Right ` A ) ) /\ b e. ( -us " ( _Left ` A ) ) ) -> a a
88	8 11 38 42 87	ssltd	Could not format ( ph -> ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) <