Theorem addsproplem7

Description: Lemma for surreal addition properties. Putting together the three previous lemmas, we now show the second half of the inductive hypothesis unconditionally. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addsproplem.1	No typesetting found for |- ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
	addspropord.2	$$⊢\phi \to X\in \mathrm{No}$$
	addspropord.3	$$⊢\phi \to Y\in \mathrm{No}$$
	addspropord.4	$$⊢\phi \to Z\in \mathrm{No}$$
	addspropord.5	$$⊢\phi \to Y{<}_{s}Z$$
Assertion	addsproplem7	Could not format assertion : No typesetting found for |- ( ph -> ( Y +s X )

Proof

Step	Hyp	Ref	Expression
1		addsproplem.1	Could not format ( ph -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
2		addspropord.2	$$⊢\phi \to X\in \mathrm{No}$$
3		addspropord.3	$$⊢\phi \to Y\in \mathrm{No}$$
4		addspropord.4	$$⊢\phi \to Z\in \mathrm{No}$$
5		addspropord.5	$$⊢\phi \to Y{<}_{s}Z$$
6		bdayelon	$$⊢\mathrm{bday}\left(Y\right)\in \mathrm{On}$$
7		fvex	$$⊢\mathrm{bday}\left(Y\right)\in \mathrm{V}$$
8	7	elon	$$⊢\mathrm{bday}\left(Y\right)\in \mathrm{On}\leftrightarrow \mathrm{Ord}\mathrm{bday}\left(Y\right)$$
9	6 8	mpbi	$$⊢\mathrm{Ord}\mathrm{bday}\left(Y\right)$$
10		bdayelon	$$⊢\mathrm{bday}\left(Z\right)\in \mathrm{On}$$
11		fvex	$$⊢\mathrm{bday}\left(Z\right)\in \mathrm{V}$$
12	11	elon	$$⊢\mathrm{bday}\left(Z\right)\in \mathrm{On}\leftrightarrow \mathrm{Ord}\mathrm{bday}\left(Z\right)$$
13	10 12	mpbi	$$⊢\mathrm{Ord}\mathrm{bday}\left(Z\right)$$
14		ordtri3or	$$⊢\left(\mathrm{Ord}\mathrm{bday}\left(Y\right)\wedge \mathrm{Ord}\mathrm{bday}\left(Z\right)\right)\to \left(\mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)\vee \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)\vee \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)\right)$$
15	9 13 14	mp2an	$$⊢\left(\mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)\vee \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)\vee \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)\right)$$
16		simpl	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)\right)\to \phi$$
17	16 1	syl	Could not format ( ( ph /\ ( bday ` Y ) e. ( bday ` Z ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
18	16 2	syl	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)\right)\to X\in \mathrm{No}$$
19	16 3	syl	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)\right)\to Y\in \mathrm{No}$$
20	16 4	syl	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)\right)\to Z\in \mathrm{No}$$
21	16 5	syl	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)\right)\to Y{<}_{s}Z$$
22		simpr	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)\right)\to \mathrm{bday}\left(Y\right)\in \mathrm{bday}\left(Z\right)$$
23	17 18 19 20 21 22	addsproplem4	Could not format ( ( ph /\ ( bday ` Y ) e. ( bday ` Z ) ) -> ( Y +s X ) ( Y +s X )
24	23	ex	Could not format ( ph -> ( ( bday ` Y ) e. ( bday ` Z ) -> ( Y +s X ) ( ( bday ` Y ) e. ( bday ` Z ) -> ( Y +s X )
25		simpl	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)\right)\to \phi$$
26	25 1	syl	Could not format ( ( ph /\ ( bday ` Y ) = ( bday ` Z ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
27	25 2	syl	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)\right)\to X\in \mathrm{No}$$
28	25 3	syl	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)\right)\to Y\in \mathrm{No}$$
29	25 4	syl	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)\right)\to Z\in \mathrm{No}$$
30	25 5	syl	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)\right)\to Y{<}_{s}Z$$
31		simpr	$$⊢\left(\phi \wedge \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)\right)\to \mathrm{bday}\left(Y\right)=\mathrm{bday}\left(Z\right)$$
32	26 27 28 29 30 31	addsproplem6	Could not format ( ( ph /\ ( bday ` Y ) = ( bday ` Z ) ) -> ( Y +s X ) ( Y +s X )
33	32	ex	Could not format ( ph -> ( ( bday ` Y ) = ( bday ` Z ) -> ( Y +s X ) ( ( bday ` Y ) = ( bday ` Z ) -> ( Y +s X )
34	1	adantr	Could not format ( ( ph /\ ( bday ` Z ) e. ( bday ` Y ) ) -> A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x ) A. x e. No A. y e. No A. z e. No ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( x +s y ) e. No /\ ( y ( y +s x )
35	2	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)\right)\to X\in \mathrm{No}$$
36	3	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)\right)\to Y\in \mathrm{No}$$
37	4	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)\right)\to Z\in \mathrm{No}$$
38	5	adantr	$$⊢\left(\phi \wedge \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)\right)\to Y{<}_{s}Z$$
39		simpr	$$⊢\left(\phi \wedge \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)\right)\to \mathrm{bday}\left(Z\right)\in \mathrm{bday}\left(Y\right)$$
40	34 35 36 37 38 39	addsproplem5	Could not format ( ( ph /\ ( bday ` Z ) e. ( bday ` Y ) ) -> ( Y +s X ) ( Y +s X )
41	40	ex	Could not format ( ph -> ( ( bday ` Z ) e. ( bday ` Y ) -> ( Y +s X ) ( ( bday ` Z ) e. ( bday ` Y ) -> ( Y +s X )
42	24 33 41	3jaod	Could not format ( ph -> ( ( ( bday ` Y ) e. ( bday ` Z ) \/ ( bday ` Y ) = ( bday ` Z ) \/ ( bday ` Z ) e. ( bday ` Y ) ) -> ( Y +s X ) ( ( ( bday ` Y ) e. ( bday ` Z ) \/ ( bday ` Y ) = ( bday ` Z ) \/ ( bday ` Z ) e. ( bday ` Y ) ) -> ( Y +s X )
43	15 42	mpi	Could not format ( ph -> ( Y +s X ) ( Y +s X )