Theorem negsproplem6

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis when A is the same age as B . (Contributed by Scott Fenton, 3-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 )
	negsproplem4.1	$$⊢\phi \to A\in \mathrm{No}$$
	negsproplem4.2	$$⊢\phi \to B\in \mathrm{No}$$
	negsproplem4.3	$$⊢\phi \to A{<}_{s}B$$
	negsproplem6.4	$$⊢\phi \to \mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)$$
Assertion	negsproplem6	Could not format assertion : No typesetting found for |- ( ph -> ( -us ` B )

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		negsproplem4.1	$$⊢\phi \to A\in \mathrm{No}$$
3		negsproplem4.2	$$⊢\phi \to B\in \mathrm{No}$$
4		negsproplem4.3	$$⊢\phi \to A{<}_{s}B$$
5		negsproplem6.4	$$⊢\phi \to \mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)$$
6		nodense	$$⊢\left(\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\wedge \left(\mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\wedge A{<}_{s}B\right)\right)\to \exists d\in \mathrm{No}\left(\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\wedge A{<}_{s}d\wedge d{<}_{s}B\right)$$
7	2 3 5 4 6	syl22anc	$$⊢\phi \to \exists d\in \mathrm{No}\left(\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\wedge A{<}_{s}d\wedge d{<}_{s}B\right)$$
8		uncom	$$⊢\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)=\mathrm{bday}\left(B\right)\cup \mathrm{bday}\left(A\right)$$
9	8	eleq2i	$$⊢\mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)\leftrightarrow \mathrm{bday}\left(x\right)\cup \mathrm{bday}\left(y\right)\in \left(\mathrm{bday}\left(B\right)\cup \mathrm{bday}\left(A\right)\right)$$
10	9	imbi1i	Could not format ( ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
11	10	2ralbii	Could not format ( 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 ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
12	1 11	sylib	Could not format ( ph -> A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y ) A. x e. No A. y e. No ( ( ( bday ` x ) u. ( bday ` y ) ) e. ( ( bday ` B ) u. ( bday ` A ) ) -> ( ( -us ` x ) e. No /\ ( x ( -us ` y )
13	12 3	negsproplem3	Could not format ( ph -> ( ( -us ` B ) e. No /\ ( -us " ( _Right ` B ) ) < ( ( -us ` B ) e. No /\ ( -us " ( _Right ` B ) ) <
14	13	simp1d	Could not format ( ph -> ( -us ` B ) e. No ) : No typesetting found for |- ( ph -> ( -us ` B ) e. No ) with typecode |-
15	14	adantr	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` B ) e. No ) : No typesetting found for |- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` B ) e. No ) with typecode |-
16	1	adantr	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ 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 )
17		simprl	$$⊢\left(\phi \wedge \left(d\in \mathrm{No}\wedge \left(\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\wedge A{<}_{s}d\wedge d{<}_{s}B\right)\right)\right)\to d\in \mathrm{No}$$
18		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
19	18	a1i	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A 0s e. No ) : No typesetting found for |- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A 0s e. No ) with typecode |-
20		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
21	20	uneq2i	Could not format ( ( bday ` d ) u. ( bday ` 0s ) ) = ( ( bday ` d ) u. (/) ) : No typesetting found for |- ( ( bday ` d ) u. ( bday ` 0s ) ) = ( ( bday ` d ) u. (/) ) with typecode |-
22		un0	$$⊢\mathrm{bday}\left(d\right)\cup \varnothing =\mathrm{bday}\left(d\right)$$
23	21 22	eqtri	Could not format ( ( bday ` d ) u. ( bday ` 0s ) ) = ( bday ` d ) : No typesetting found for |- ( ( bday ` d ) u. ( bday ` 0s ) ) = ( bday ` d ) with typecode |-
24		simprr1	$$⊢\left(\phi \wedge \left(d\in \mathrm{No}\wedge \left(\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\wedge A{<}_{s}d\wedge d{<}_{s}B\right)\right)\right)\to \mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)$$
25		elun1	$$⊢\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\to \mathrm{bday}\left(d\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)$$
26	24 25	syl	$$⊢\left(\phi \wedge \left(d\in \mathrm{No}\wedge \left(\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\wedge A{<}_{s}d\wedge d{<}_{s}B\right)\right)\right)\to \mathrm{bday}\left(d\right)\in \left(\mathrm{bday}\left(A\right)\cup \mathrm{bday}\left(B\right)\right)$$
27	23 26	eqeltrid	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( ( bday ` d ) u. ( bday ` 0s ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) : No typesetting found for |- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( ( bday ` d ) u. ( bday ` 0s ) ) e. ( ( bday ` A ) u. ( bday ` B ) ) ) with typecode |-
28	16 17 19 27	negsproplem1	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( ( -us ` d ) e. No /\ ( d ( -us ` 0s ) ( ( -us ` d ) e. No /\ ( d ( -us ` 0s )
29	28	simpld	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` d ) e. No ) : No typesetting found for |- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` d ) e. No ) with typecode |-
30	1 2	negsproplem3	Could not format ( ph -> ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) < ( ( -us ` A ) e. No /\ ( -us " ( _Right ` A ) ) <
31	30	simp1d	Could not format ( ph -> ( -us ` A ) e. No ) : No typesetting found for |- ( ph -> ( -us ` A ) e. No ) with typecode |-
32	31	adantr	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` A ) e. No ) : No typesetting found for |- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` A ) e. No ) with typecode |-
33	13	simp3d	Could not format ( ph -> { ( -us ` B ) } < { ( -us ` B ) } <
34	33	adantr	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A { ( -us ` B ) } < { ( -us ` B ) } <
35		fvex	Could not format ( -us ` B ) e. _V : No typesetting found for |- ( -us ` B ) e. _V with typecode |-
36	35	snid	Could not format ( -us ` B ) e. { ( -us ` B ) } : No typesetting found for |- ( -us ` B ) e. { ( -us ` B ) } with typecode |-
37	36	a1i	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` B ) e. { ( -us ` B ) } ) : No typesetting found for |- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` B ) e. { ( -us ` B ) } ) with typecode |-
38		negsfn	Could not format -us Fn No : No typesetting found for |- -us Fn No with typecode |-
39		leftssno	Could not format ( _Left ` B ) C_ No : No typesetting found for |- ( _Left ` B ) C_ No with typecode |-
40		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
41		oldbday	$$⊢\left(\mathrm{bday}\left(A\right)\in \mathrm{On}\wedge d\in \mathrm{No}\right)\to \left(d\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\leftrightarrow \mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\right)$$
42	40 17 41	sylancr	$$⊢\left(\phi \wedge \left(d\in \mathrm{No}\wedge \left(\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\wedge A{<}_{s}d\wedge d{<}_{s}B\right)\right)\right)\to \left(d\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)\leftrightarrow \mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\right)$$
43	24 42	mpbird	$$⊢\left(\phi \wedge \left(d\in \mathrm{No}\wedge \left(\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\wedge A{<}_{s}d\wedge d{<}_{s}B\right)\right)\right)\to d\in \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)$$
44	5	fveq2d	$$⊢\phi \to \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)=\mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
45	44	adantr	$$⊢\left(\phi \wedge \left(d\in \mathrm{No}\wedge \left(\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\wedge A{<}_{s}d\wedge d{<}_{s}B\right)\right)\right)\to \mathrm{Old}\left(\mathrm{bday}\left(A\right)\right)=\mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
46	43 45	eleqtrd	$$⊢\left(\phi \wedge \left(d\in \mathrm{No}\wedge \left(\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\wedge A{<}_{s}d\wedge d{<}_{s}B\right)\right)\right)\to d\in \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
47		simprr3	$$⊢\left(\phi \wedge \left(d\in \mathrm{No}\wedge \left(\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\wedge A{<}_{s}d\wedge d{<}_{s}B\right)\right)\right)\to d{<}_{s}B$$
48		leftval	Could not format ( _Left ` B ) = { d e. ( _Old ` ( bday ` B ) ) | d
49	48	reqabi	Could not format ( d e. ( _Left ` B ) <-> ( d e. ( _Old ` ( bday ` B ) ) /\ d ( d e. ( _Old ` ( bday ` B ) ) /\ d
50	46 47 49	sylanbrc	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A d e. ( _Left ` B ) ) : No typesetting found for |- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A d e. ( _Left ` B ) ) with typecode |-
51		fnfvima	Could not format ( ( -us Fn No /\ ( _Left ` B ) C_ No /\ d e. ( _Left ` B ) ) -> ( -us ` d ) e. ( -us " ( _Left ` B ) ) ) : No typesetting found for |- ( ( -us Fn No /\ ( _Left ` B ) C_ No /\ d e. ( _Left ` B ) ) -> ( -us ` d ) e. ( -us " ( _Left ` B ) ) ) with typecode |-
52	38 39 50 51	mp3an12i	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` d ) e. ( -us " ( _Left ` B ) ) ) : No typesetting found for |- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` d ) e. ( -us " ( _Left ` B ) ) ) with typecode |-
53	34 37 52	ssltsepcd	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` B ) ( -us ` B )
54	30	simp2d	Could not format ( ph -> ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) <
55	54	adantr	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us " ( _Right ` A ) ) < ( -us " ( _Right ` A ) ) <
56		rightssno	Could not format ( _Right ` A ) C_ No : No typesetting found for |- ( _Right ` A ) C_ No with typecode |-
57		simprr2	$$⊢\left(\phi \wedge \left(d\in \mathrm{No}\wedge \left(\mathrm{bday}\left(d\right)\in \mathrm{bday}\left(A\right)\wedge A{<}_{s}d\wedge d{<}_{s}B\right)\right)\right)\to A{<}_{s}d$$
58		rightval	Could not format ( _Right ` A ) = { d e. ( _Old ` ( bday ` A ) ) | A
59	58	reqabi	Could not format ( d e. ( _Right ` A ) <-> ( d e. ( _Old ` ( bday ` A ) ) /\ A ( d e. ( _Old ` ( bday ` A ) ) /\ A
60	43 57 59	sylanbrc	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A d e. ( _Right ` A ) ) : No typesetting found for |- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A d e. ( _Right ` A ) ) with typecode |-
61		fnfvima	Could not format ( ( -us Fn No /\ ( _Right ` A ) C_ No /\ d e. ( _Right ` A ) ) -> ( -us ` d ) e. ( -us " ( _Right ` A ) ) ) : No typesetting found for |- ( ( -us Fn No /\ ( _Right ` A ) C_ No /\ d e. ( _Right ` A ) ) -> ( -us ` d ) e. ( -us " ( _Right ` A ) ) ) with typecode |-
62	38 56 60 61	mp3an12i	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` d ) e. ( -us " ( _Right ` A ) ) ) : No typesetting found for |- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` d ) e. ( -us " ( _Right ` A ) ) ) with typecode |-
63		fvex	Could not format ( -us ` A ) e. _V : No typesetting found for |- ( -us ` A ) e. _V with typecode |-
64	63	snid	Could not format ( -us ` A ) e. { ( -us ` A ) } : No typesetting found for |- ( -us ` A ) e. { ( -us ` A ) } with typecode |-
65	64	a1i	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` A ) e. { ( -us ` A ) } ) : No typesetting found for |- ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` A ) e. { ( -us ` A ) } ) with typecode |-
66	55 62 65	ssltsepcd	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` d ) ( -us ` d )
67	15 29 32 53 66	slttrd	Could not format ( ( ph /\ ( d e. No /\ ( ( bday ` d ) e. ( bday ` A ) /\ A ( -us ` B ) ( -us ` B )
68	7 67	rexlimddv	Could not format ( ph -> ( -us ` B ) ( -us ` B )