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	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 )
	addsproplem1.2	$$⊢\phi \to A\in \mathrm{No}$$
	addsproplem1.3	$$⊢\phi \to B\in \mathrm{No}$$
	addsproplem1.4	$$⊢\phi \to C\in \mathrm{No}$$
	addsproplem1.5	No typesetting found for |- ( ph -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` C ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
Assertion	addsproplem1	Could not format assertion : No typesetting found for |- ( ph -> ( ( A +s B ) e. No /\ ( B ( B +s A )

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		addsproplem1.2	$$⊢\phi \to A\in \mathrm{No}$$
3		addsproplem1.3	$$⊢\phi \to B\in \mathrm{No}$$
4		addsproplem1.4	$$⊢\phi \to C\in \mathrm{No}$$
5		addsproplem1.5	Could not format ( ph -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` C ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) : No typesetting found for |- ( ph -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` C ) ) ) e. ( ( ( bday ` X ) +no ( bday ` Y ) ) u. ( ( bday ` X ) +no ( bday ` Z ) ) ) ) with typecode |-
6	2 3 4	3jca	$$⊢\phi \to \left(A\in \mathrm{No}\wedge B\in \mathrm{No}\wedge C\in \mathrm{No}\right)$$
7		fveq2	$$⊢x=A\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(A\right)$$
8	7	oveq1d	Could not format ( x = A -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` A ) +no ( bday ` y ) ) ) : No typesetting found for |- ( x = A -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` A ) +no ( bday ` y ) ) ) with typecode |-
9	7	oveq1d	Could not format ( x = A -> ( ( bday ` x ) +no ( bday ` z ) ) = ( ( bday ` A ) +no ( bday ` z ) ) ) : No typesetting found for |- ( x = A -> ( ( bday ` x ) +no ( bday ` z ) ) = ( ( bday ` A ) +no ( bday ` z ) ) ) with typecode |-
10	8 9	uneq12d	Could not format ( x = A -> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) = ( ( ( bday ` A ) +no ( bday ` y ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) ) : No typesetting found for |- ( x = A -> ( ( ( bday ` x ) +no ( bday ` y ) ) u. ( ( bday ` x ) +no ( bday ` z ) ) ) = ( ( ( bday ` A ) +no ( bday ` y ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) ) with typecode |-
11	10	eleq1d	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
12		oveq1	Could not format ( x = A -> ( x +s y ) = ( A +s y ) ) : No typesetting found for |- ( x = A -> ( x +s y ) = ( A +s y ) ) with typecode |-
13	12	eleq1d	Could not format ( x = A -> ( ( x +s y ) e. No <-> ( A +s y ) e. No ) ) : No typesetting found for |- ( x = A -> ( ( x +s y ) e. No <-> ( A +s y ) e. No ) ) with typecode |-
14		oveq2	Could not format ( x = A -> ( y +s x ) = ( y +s A ) ) : No typesetting found for |- ( x = A -> ( y +s x ) = ( y +s A ) ) with typecode |-
15		oveq2	Could not format ( x = A -> ( z +s x ) = ( z +s A ) ) : No typesetting found for |- ( x = A -> ( z +s x ) = ( z +s A ) ) with typecode |-
16	14 15	breq12d	Could not format ( x = A -> ( ( y +s x ) ( y +s A ) ( ( y +s x ) ( y +s A )
17	16	imbi2d	Could not format ( x = A -> ( ( y ( y +s x ) ( y ( y +s A ) ( ( y ( y +s x ) ( y ( y +s A )
18	13 17	anbi12d	Could not format ( x = A -> ( ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( A +s y ) e. No /\ ( y ( y +s A ) ( ( ( x +s y ) e. No /\ ( y ( y +s x ) ( ( A +s y ) e. No /\ ( y ( y +s A )
19	11 18	imbi12d	Could not format ( 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 ) ( ( ( ( ( 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\to \mathrm{bday}\left(y\right)=\mathrm{bday}\left(B\right)$$
21	20	oveq2d	Could not format ( y = B -> ( ( bday ` A ) +no ( bday ` y ) ) = ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( y = B -> ( ( bday ` A ) +no ( bday ` y ) ) = ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
22	21	uneq1d	Could not format ( y = B -> ( ( ( bday ` A ) +no ( bday ` y ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) ) : No typesetting found for |- ( y = B -> ( ( ( bday ` A ) +no ( bday ` y ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) ) with typecode |-
23	22	eleq1d	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
24		oveq2	Could not format ( y = B -> ( A +s y ) = ( A +s B ) ) : No typesetting found for |- ( y = B -> ( A +s y ) = ( A +s B ) ) with typecode |-
25	24	eleq1d	Could not format ( y = B -> ( ( A +s y ) e. No <-> ( A +s B ) e. No ) ) : No typesetting found for |- ( y = B -> ( ( A +s y ) e. No <-> ( A +s B ) e. No ) ) with typecode |-
26		breq1	$$⊢y=B\to \left(y{<}_{s}z\leftrightarrow B{<}_{s}z\right)$$
27		oveq1	Could not format ( y = B -> ( y +s A ) = ( B +s A ) ) : No typesetting found for |- ( y = B -> ( y +s A ) = ( B +s A ) ) with typecode |-
28	27	breq1d	Could not format ( y = B -> ( ( y +s A ) ( B +s A ) ( ( y +s A ) ( B +s A )
29	26 28	imbi12d	Could not format ( y = B -> ( ( y ( y +s A ) ( B ( B +s A ) ( ( y ( y +s A ) ( B ( B +s A )
30	25 29	anbi12d	Could not format ( y = B -> ( ( ( A +s y ) e. No /\ ( y ( y +s A ) ( ( A +s B ) e. No /\ ( B ( B +s A ) ( ( ( A +s y ) e. No /\ ( y ( y +s A ) ( ( A +s B ) e. No /\ ( B ( B +s A )
31	23 30	imbi12d	Could not format ( 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 ) ( ( ( ( ( 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\to \mathrm{bday}\left(z\right)=\mathrm{bday}\left(C\right)$$
33	32	oveq2d	Could not format ( z = C -> ( ( bday ` A ) +no ( bday ` z ) ) = ( ( bday ` A ) +no ( bday ` C ) ) ) : No typesetting found for |- ( z = C -> ( ( bday ` A ) +no ( bday ` z ) ) = ( ( bday ` A ) +no ( bday ` C ) ) ) with typecode |-
34	33	uneq2d	Could not format ( z = C -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` C ) ) ) ) : No typesetting found for |- ( z = C -> ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` z ) ) ) = ( ( ( bday ` A ) +no ( bday ` B ) ) u. ( ( bday ` A ) +no ( bday ` C ) ) ) ) with typecode |-
35	34	eleq1d	Could not format ( 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 ) ) ) ) ) : No typesetting found for |- ( 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 ) ) ) ) ) with typecode |-
36		breq2	$$⊢z=C\to \left(B{<}_{s}z\leftrightarrow B{<}_{s}C\right)$$
37		oveq1	Could not format ( z = C -> ( z +s A ) = ( C +s A ) ) : No typesetting found for |- ( z = C -> ( z +s A ) = ( C +s A ) ) with typecode |-
38	37	breq2d	Could not format ( z = C -> ( ( B +s A ) ( B +s A ) ( ( B +s A ) ( B +s A )
39	36 38	imbi12d	Could not format ( z = C -> ( ( B ( B +s A ) ( B ( B +s A ) ( ( B ( B +s A ) ( B ( B +s A )
40	39	anbi2d	Could not format ( z = C -> ( ( ( A +s B ) e. No /\ ( B ( B +s A ) ( ( A +s B ) e. No /\ ( B ( B +s A ) ( ( ( A +s B ) e. No /\ ( B ( B +s A ) ( ( A +s B ) e. No /\ ( B ( B +s A )
41	35 40	imbi12d	Could not format ( 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 ) ( ( ( ( ( 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	Could not format ( ( 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 ) ( 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	Could not format ( ph -> ( ( A +s B ) e. No /\ ( B ( B +s A ) ( ( A +s B ) e. No /\ ( B ( B +s A )