Theorem negsproplem7

Description: Lemma for surreal negation. Show the second half of the inductive hypothesis unconditionally. (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$$
Assertion	negsproplem7	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		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
6	5	onordi	$$⊢\mathrm{Ord}\mathrm{bday}\left(A\right)$$
7		bdayelon	$$⊢\mathrm{bday}\left(B\right)\in \mathrm{On}$$
8	7	onordi	$$⊢\mathrm{Ord}\mathrm{bday}\left(B\right)$$
9		ordtri3or	$$⊢\left(\mathrm{Ord}\mathrm{bday}\left(A\right)\wedge \mathrm{Ord}\mathrm{bday}\left(B\right)\right)\to \left(\mathrm{bday}\left(A\right)\in \mathrm{bday}\left(B\right)\vee \mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\vee \mathrm{bday}\left(B\right)\in \mathrm{bday}\left(A\right)\right)$$
10	6 8 9	mp2an	$$⊢\left(\mathrm{bday}\left(A\right)\in \mathrm{bday}\left(B\right)\vee \mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\vee \mathrm{bday}\left(B\right)\in \mathrm{bday}\left(A\right)\right)$$
11	1	adantr	Could not format ( ( ph /\ ( bday ` A ) e. ( bday ` B ) ) -> 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 )
12	2	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(A\right)\in \mathrm{bday}\left(B\right)\right)\to A\in \mathrm{No}$$
13	3	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(A\right)\in \mathrm{bday}\left(B\right)\right)\to B\in \mathrm{No}$$
14	4	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(A\right)\in \mathrm{bday}\left(B\right)\right)\to A{<}_{s}B$$
15		simpr	$$⊢\left(\phi \wedge \mathrm{bday}\left(A\right)\in \mathrm{bday}\left(B\right)\right)\to \mathrm{bday}\left(A\right)\in \mathrm{bday}\left(B\right)$$
16	11 12 13 14 15	negsproplem4	Could not format ( ( ph /\ ( bday ` A ) e. ( bday ` B ) ) -> ( -us ` B ) ( -us ` B )
17	16	ex	Could not format ( ph -> ( ( bday ` A ) e. ( bday ` B ) -> ( -us ` B ) ( ( bday ` A ) e. ( bday ` B ) -> ( -us ` B )
18	1	adantr	Could not format ( ( ph /\ ( bday ` A ) = ( bday ` B ) ) -> 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 )
19	2	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\right)\to A\in \mathrm{No}$$
20	3	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\right)\to B\in \mathrm{No}$$
21	4	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\right)\to A{<}_{s}B$$
22		simpr	$$⊢\left(\phi \wedge \mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)\right)\to \mathrm{bday}\left(A\right)=\mathrm{bday}\left(B\right)$$
23	18 19 20 21 22	negsproplem6	Could not format ( ( ph /\ ( bday ` A ) = ( bday ` B ) ) -> ( -us ` B ) ( -us ` B )
24	23	ex	Could not format ( ph -> ( ( bday ` A ) = ( bday ` B ) -> ( -us ` B ) ( ( bday ` A ) = ( bday ` B ) -> ( -us ` B )
25	1	adantr	Could not format ( ( ph /\ ( bday ` B ) e. ( 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 )
26	2	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(B\right)\in \mathrm{bday}\left(A\right)\right)\to A\in \mathrm{No}$$
27	3	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(B\right)\in \mathrm{bday}\left(A\right)\right)\to B\in \mathrm{No}$$
28	4	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(B\right)\in \mathrm{bday}\left(A\right)\right)\to A{<}_{s}B$$
29		simpr	$$⊢\left(\phi \wedge \mathrm{bday}\left(B\right)\in \mathrm{bday}\left(A\right)\right)\to \mathrm{bday}\left(B\right)\in \mathrm{bday}\left(A\right)$$
30	25 26 27 28 29	negsproplem5	Could not format ( ( ph /\ ( bday ` B ) e. ( bday ` A ) ) -> ( -us ` B ) ( -us ` B )
31	30	ex	Could not format ( ph -> ( ( bday ` B ) e. ( bday ` A ) -> ( -us ` B ) ( ( bday ` B ) e. ( bday ` A ) -> ( -us ` B )
32	17 24 31	3jaod	Could not format ( ph -> ( ( ( bday ` A ) e. ( bday ` B ) \/ ( bday ` A ) = ( bday ` B ) \/ ( bday ` B ) e. ( bday ` A ) ) -> ( -us ` B ) ( ( ( bday ` A ) e. ( bday ` B ) \/ ( bday ` A ) = ( bday ` B ) \/ ( bday ` B ) e. ( bday ` A ) ) -> ( -us ` B )
33	10 32	mpi	Could not format ( ph -> ( -us ` B ) ( -us ` B )