Theorem addsproplem1

Description: Lemma for surreal addition properties. To prove closure on surreal addition we need to prove that addition is compatible with order at the same time. We do this by inducting over the maximum of two natural sums of the birthdays of surreals numbers. In the final step we will loop around and use tfr3 to prove this of all surreals. This first lemma just instantiates the inductive hypothesis so we do not need to do it continuously throughout the proof. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addsproplem.1	|- ( 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 )
	addsproplem1.2	|- ( ph -> A e. No )
	addsproplem1.3	|- ( ph -> B e. No )
	addsproplem1.4	|- ( ph -> C e. No )
	addsproplem1.5	|- ( ph -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` C ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
Assertion	addsproplem1	|- ( ph -> ( ( A +s B ) e. No /\ ( B ( B +s A )

Proof

Step	Hyp	Ref	Expression
1		addsproplem.1	|- ( 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 )
2		addsproplem1.2	|- ( ph -> A e. No )
3		addsproplem1.3	|- ( ph -> B e. No )
4		addsproplem1.4	|- ( ph -> C e. No )
5		addsproplem1.5	|- ( ph -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` C ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) )
6	2 3 4	3jca	|- ( ph -> ( A e. No /\ B e. No /\ C e. No ) )
7		fveq2	|- ( x = A -> ( bday ` x ) = ( bday ` A ) )
8	7	oveq1d	|- ( x = A -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` A ) +no ( bday ` y ) ) )
9	7	oveq1d	|- ( x = A -> ( ( bday ` x ) +no ( bday ` z ) ) = ( ( bday ` A ) +no ( bday ` z ) ) )
10	8 9	uneq12d	|- ( x = A -> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) = ( ( ( bday ` A ) +no ( bday ` y ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) )
11	10	eleq1d	|- ( x = A -> ( ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) <-> ( ( ( bday ` A ) +no ( bday ` y ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) )
12		oveq1	|- ( x = A -> ( x +s y ) = ( A +s y ) )
13	12	eleq1d	|- ( x = A -> ( ( x +s y ) e. No <-> ( A +s y ) e. No ) )
14		oveq2	|- ( x = A -> ( y +s x ) = ( y +s A ) )
15		oveq2	|- ( x = A -> ( z +s x ) = ( z +s A ) )
16	14 15	breq12d	|- ( x = A -> ( ( y +s x ) ( y +s A )
17	16	imbi2d	|- ( x = A -> ( ( y ( y +s x ) ( y ( y +s A )
18	13 17	anbi12d	|- ( x = A -> ( ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( A +s y ) e. No /\ ( y ( y +s A )
19	11 18	imbi12d	|- ( x = A -> ( ( ( ( ( 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 ) ( ( ( ( bday ` A ) +no ( bday ` y ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( A +s y ) e. No /\ ( y ( y +s A )
20		fveq2	|- ( y = B -> ( bday ` y ) = ( bday ` B ) )
21	20	oveq2d	|- ( y = B -> ( ( bday ` A ) +no ( bday ` y ) ) = ( ( bday ` A ) +no ( bday ` B ) ) )
22	21	uneq1d	|- ( y = B -> ( ( ( bday ` A ) +no ( bday ` y ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) )
23	22	eleq1d	|- ( y = B -> ( ( ( ( bday ` A ) +no ( bday ` y ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) <-> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) )
24		oveq2	|- ( y = B -> ( A +s y ) = ( A +s B ) )
25	24	eleq1d	|- ( y = B -> ( ( A +s y ) e. No <-> ( A +s B ) e. No ) )
26		breq1	|- ( y = B -> ( y B
27		oveq1	|- ( y = B -> ( y +s A ) = ( B +s A ) )
28	27	breq1d	|- ( y = B -> ( ( y +s A ) ( B +s A )
29	26 28	imbi12d	|- ( y = B -> ( ( y ( y +s A ) ( B ( B +s A )
30	25 29	anbi12d	|- ( y = B -> ( ( ( A +s y ) e. No /\ ( y ( y +s A ) ( ( A +s B ) e. No /\ ( B ( B +s A )
31	23 30	imbi12d	|- ( y = B -> ( ( ( ( ( bday ` A ) +no ( bday ` y ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( A +s y ) e. No /\ ( y ( y +s A ) ( ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( A +s B ) e. No /\ ( B ( B +s A )
32		fveq2	|- ( z = C -> ( bday ` z ) = ( bday ` C ) )
33	32	oveq2d	|- ( z = C -> ( ( bday ` A ) +no ( bday ` z ) ) = ( ( bday ` A ) +no ( bday ` C ) ) )
34	33	uneq2d	|- ( z = C -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` C ) ) ) )
35	34	eleq1d	|- ( z = C -> ( ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) <-> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` C ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) )
36		breq2	|- ( z = C -> ( B B
37		oveq1	|- ( z = C -> ( z +s A ) = ( C +s A ) )
38	37	breq2d	|- ( z = C -> ( ( B +s A ) ( B +s A )
39	36 38	imbi12d	|- ( z = C -> ( ( B ( B +s A ) ( B ( B +s A )
40	39	anbi2d	|- ( z = C -> ( ( ( A +s B ) e. No /\ ( B ( B +s A ) ( ( A +s B ) e. No /\ ( B ( B +s A )
41	35 40	imbi12d	|- ( z = C -> ( ( ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( A +s B ) e. No /\ ( B ( B +s A ) ( ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` C ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( A +s B ) e. No /\ ( B ( B +s A )
42	19 31 41	rspc3v	|- ( ( A e. No /\ B e. No /\ C e. No ) -> ( 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 ) ( ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` C ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) -> ( ( A +s B ) e. No /\ ( B ( B +s A )
43	6 1 5 42	syl3c	|- ( ph -> ( ( A +s B ) e. No /\ ( B ( B +s A )