Theorem addsproplem2

Description: Lemma for surreal addition properties. When proving closure for operations defined using norec and norec2 , it is a strictly stronger statement to say that the cut defined is actually a cut than it is to say that the operation is closed. We will often prove this stronger statement. Here, we do so for the cut involved in surreal addition. (Contributed by Scott Fenton, 21-Jan-2025)

	Ref	Expression
Hypotheses	addsproplem.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
	addsproplem2.2	⊢ ( 𝜑 → 𝑋 ∈ No )
	addsproplem2.3	⊢ ( 𝜑 → 𝑌 ∈ No )
Assertion	addsproplem2	⊢ ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) )

Proof

Step	Hyp	Ref	Expression
1		addsproplem.1	⊢ ( 𝜑 → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
2		addsproplem2.2	⊢ ( 𝜑 → 𝑋 ∈ No )
3		addsproplem2.3	⊢ ( 𝜑 → 𝑌 ∈ No )
4		fvex	⊢ ( L ‘ 𝑋 ) ∈ V
5	4	abrexex	⊢ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∈ V
6	5	a1i	⊢ ( 𝜑 → { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∈ V )
7		fvex	⊢ ( L ‘ 𝑌 ) ∈ V
8	7	abrexex	⊢ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ∈ V
9	8	a1i	⊢ ( 𝜑 → { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ∈ V )
10	6 9	unexd	⊢ ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∈ V )
11		fvex	⊢ ( R ‘ 𝑋 ) ∈ V
12	11	abrexex	⊢ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∈ V
13	12	a1i	⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∈ V )
14		fvex	⊢ ( R ‘ 𝑌 ) ∈ V
15	14	abrexex	⊢ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ∈ V
16	15	a1i	⊢ ( 𝜑 → { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ∈ V )
17	13 16	unexd	⊢ ( 𝜑 → ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ∈ V )
18	1	adantr	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
19		leftssno	⊢ ( L ‘ 𝑋 ) ⊆ No
20	19	sseli	⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → 𝑙 ∈ No )
21	20	adantl	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → 𝑙 ∈ No )
22	3	adantr	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → 𝑌 ∈ No )
23		0sno	⊢ 0s ∈ No
24	23	a1i	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → 0s ∈ No )
25		bday0s	⊢ ( bday ‘ 0s ) = ∅
26	25	oveq2i	⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) = ( ( bday ‘ 𝑙 ) +no ∅ )
27		bdayelon	⊢ ( bday ‘ 𝑙 ) ∈ On
28		naddrid	⊢ ( ( bday ‘ 𝑙 ) ∈ On → ( ( bday ‘ 𝑙 ) +no ∅ ) = ( bday ‘ 𝑙 ) )
29	27 28	ax-mp	⊢ ( ( bday ‘ 𝑙 ) +no ∅ ) = ( bday ‘ 𝑙 )
30	26 29	eqtri	⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) = ( bday ‘ 𝑙 )
31	30	uneq2i	⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑙 ) )
32		bdayelon	⊢ ( bday ‘ 𝑌 ) ∈ On
33		naddword1	⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) )
34	27 32 33	mp2an	⊢ ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
35		ssequn2	⊢ ( ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) )
36	34 35	mpbi	⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
37	31 36	eqtri	⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
38		leftssold	⊢ ( L ‘ 𝑋 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) )
39	38	sseli	⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
40		bdayelon	⊢ ( bday ‘ 𝑋 ) ∈ On
41		oldbday	⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝑙 ∈ No ) → ( 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ) )
42	40 20 41	sylancr	⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ) )
43	39 42	mpbid	⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) )
44		naddel1	⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
45	27 40 32 44	mp3an	⊢ ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
46	43 45	sylib	⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
47	46	adantl	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
48		elun1	⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
49	47 48	syl	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
50	37 49	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
51	18 21 22 24 50	addsproplem1	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( ( 𝑙 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 0s → ( 𝑌 +s 𝑙 ) <s ( 0s +s 𝑙 ) ) ) )
52	51	simpld	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( 𝑙 +s 𝑌 ) ∈ No )
53		eleq1a	⊢ ( ( 𝑙 +s 𝑌 ) ∈ No → ( 𝑝 = ( 𝑙 +s 𝑌 ) → 𝑝 ∈ No ) )
54	52 53	syl	⊢ ( ( 𝜑 ∧ 𝑙 ∈ ( L ‘ 𝑋 ) ) → ( 𝑝 = ( 𝑙 +s 𝑌 ) → 𝑝 ∈ No ) )
55	54	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) → 𝑝 ∈ No ) )
56	55	abssdv	⊢ ( 𝜑 → { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ⊆ No )
57	1	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
58	2	adantr	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → 𝑋 ∈ No )
59		leftssno	⊢ ( L ‘ 𝑌 ) ⊆ No
60	59	sseli	⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → 𝑚 ∈ No )
61	60	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → 𝑚 ∈ No )
62	23	a1i	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → 0s ∈ No )
63	25	oveq2i	⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) = ( ( bday ‘ 𝑋 ) +no ∅ )
64		naddrid	⊢ ( ( bday ‘ 𝑋 ) ∈ On → ( ( bday ‘ 𝑋 ) +no ∅ ) = ( bday ‘ 𝑋 ) )
65	40 64	ax-mp	⊢ ( ( bday ‘ 𝑋 ) +no ∅ ) = ( bday ‘ 𝑋 )
66	63 65	eqtri	⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) = ( bday ‘ 𝑋 )
67	66	uneq2i	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑋 ) )
68		bdayelon	⊢ ( bday ‘ 𝑚 ) ∈ On
69		naddword1	⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
70	40 68 69	mp2an	⊢ ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
71		ssequn2	⊢ ( ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
72	70 71	mpbi	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
73	67 72	eqtri	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
74		leftssold	⊢ ( L ‘ 𝑌 ) ⊆ ( O ‘ ( bday ‘ 𝑌 ) )
75	74	sseli	⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) )
76		oldbday	⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ 𝑚 ∈ No ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ) )
77	32 60 76	sylancr	⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ) )
78	75 77	mpbid	⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) )
79		naddel2	⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
80	68 32 40 79	mp3an	⊢ ( ( bday ‘ 𝑚 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
81	78 80	sylib	⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
82	81	adantl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
83		elun1	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
84	82 83	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
85	73 84	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
86	57 58 61 62 85	addsproplem1	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( ( 𝑋 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 0s → ( 𝑚 +s 𝑋 ) <s ( 0s +s 𝑋 ) ) ) )
87	86	simpld	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( 𝑋 +s 𝑚 ) ∈ No )
88		eleq1a	⊢ ( ( 𝑋 +s 𝑚 ) ∈ No → ( 𝑞 = ( 𝑋 +s 𝑚 ) → 𝑞 ∈ No ) )
89	87 88	syl	⊢ ( ( 𝜑 ∧ 𝑚 ∈ ( L ‘ 𝑌 ) ) → ( 𝑞 = ( 𝑋 +s 𝑚 ) → 𝑞 ∈ No ) )
90	89	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) → 𝑞 ∈ No ) )
91	90	abssdv	⊢ ( 𝜑 → { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ⊆ No )
92	56 91	unssd	⊢ ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ⊆ No )
93	1	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
94		rightssno	⊢ ( R ‘ 𝑋 ) ⊆ No
95	94	sseli	⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → 𝑟 ∈ No )
96	95	adantl	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → 𝑟 ∈ No )
97	3	adantr	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → 𝑌 ∈ No )
98	23	a1i	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → 0s ∈ No )
99	25	oveq2i	⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) = ( ( bday ‘ 𝑟 ) +no ∅ )
100		bdayelon	⊢ ( bday ‘ 𝑟 ) ∈ On
101		naddrid	⊢ ( ( bday ‘ 𝑟 ) ∈ On → ( ( bday ‘ 𝑟 ) +no ∅ ) = ( bday ‘ 𝑟 ) )
102	100 101	ax-mp	⊢ ( ( bday ‘ 𝑟 ) +no ∅ ) = ( bday ‘ 𝑟 )
103	99 102	eqtri	⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) = ( bday ‘ 𝑟 )
104	103	uneq2i	⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑟 ) )
105		naddword1	⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) )
106	100 32 105	mp2an	⊢ ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
107		ssequn2	⊢ ( ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) )
108	106 107	mpbi	⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
109	104 108	eqtri	⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
110		rightssold	⊢ ( R ‘ 𝑋 ) ⊆ ( O ‘ ( bday ‘ 𝑋 ) )
111	110	sseli	⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) )
112		oldbday	⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝑟 ∈ No ) → ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ) )
113	40 95 112	sylancr	⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ↔ ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ) )
114	111 113	mpbid	⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) )
115		naddel1	⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
116	100 40 32 115	mp3an	⊢ ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
117	114 116	sylib	⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
118	117	adantl	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
119		elun1	⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
120	118 119	syl	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
121	109 120	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
122	93 96 97 98 121	addsproplem1	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( ( 𝑟 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 0s → ( 𝑌 +s 𝑟 ) <s ( 0s +s 𝑟 ) ) ) )
123	122	simpld	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( 𝑟 +s 𝑌 ) ∈ No )
124		eleq1a	⊢ ( ( 𝑟 +s 𝑌 ) ∈ No → ( 𝑤 = ( 𝑟 +s 𝑌 ) → 𝑤 ∈ No ) )
125	123 124	syl	⊢ ( ( 𝜑 ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) → ( 𝑤 = ( 𝑟 +s 𝑌 ) → 𝑤 ∈ No ) )
126	125	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) → 𝑤 ∈ No ) )
127	126	abssdv	⊢ ( 𝜑 → { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ⊆ No )
128	1	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
129	2	adantr	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → 𝑋 ∈ No )
130		rightssno	⊢ ( R ‘ 𝑌 ) ⊆ No
131	130	sseli	⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → 𝑠 ∈ No )
132	131	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → 𝑠 ∈ No )
133	23	a1i	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → 0s ∈ No )
134	66	uneq2i	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑋 ) )
135		bdayelon	⊢ ( bday ‘ 𝑠 ) ∈ On
136		naddword1	⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
137	40 135 136	mp2an	⊢ ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
138		ssequn2	⊢ ( ( bday ‘ 𝑋 ) ⊆ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
139	137 138	mpbi	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
140	134 139	eqtri	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
141		rightssold	⊢ ( R ‘ 𝑌 ) ⊆ ( O ‘ ( bday ‘ 𝑌 ) )
142	141	sseli	⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) )
143		oldbday	⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ 𝑠 ∈ No ) → ( 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ) )
144	32 131 143	sylancr	⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → ( 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ↔ ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ) )
145	142 144	mpbid	⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) )
146		naddel2	⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
147	135 32 40 146	mp3an	⊢ ( ( bday ‘ 𝑠 ) ∈ ( bday ‘ 𝑌 ) ↔ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
148	145 147	sylib	⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
149	148	adantl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
150		elun1	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
151	149 150	syl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
152	140 151	eqeltrid	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
153	128 129 132 133 152	addsproplem1	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( ( 𝑋 +s 𝑠 ) ∈ No ∧ ( 𝑠 <s 0s → ( 𝑠 +s 𝑋 ) <s ( 0s +s 𝑋 ) ) ) )
154	153	simpld	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( 𝑋 +s 𝑠 ) ∈ No )
155		eleq1a	⊢ ( ( 𝑋 +s 𝑠 ) ∈ No → ( 𝑡 = ( 𝑋 +s 𝑠 ) → 𝑡 ∈ No ) )
156	154 155	syl	⊢ ( ( 𝜑 ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) → ( 𝑡 = ( 𝑋 +s 𝑠 ) → 𝑡 ∈ No ) )
157	156	rexlimdva	⊢ ( 𝜑 → ( ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) → 𝑡 ∈ No ) )
158	157	abssdv	⊢ ( 𝜑 → { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ⊆ No )
159	127 158	unssd	⊢ ( 𝜑 → ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ⊆ No )
160		elun	⊢ ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ↔ ( 𝑎 ∈ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∨ 𝑎 ∈ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) )
161		vex	⊢ 𝑎 ∈ V
162		eqeq1	⊢ ( 𝑝 = 𝑎 → ( 𝑝 = ( 𝑙 +s 𝑌 ) ↔ 𝑎 = ( 𝑙 +s 𝑌 ) ) )
163	162	rexbidv	⊢ ( 𝑝 = 𝑎 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) ↔ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ) )
164	161 163	elab	⊢ ( 𝑎 ∈ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ↔ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) )
165		eqeq1	⊢ ( 𝑞 = 𝑎 → ( 𝑞 = ( 𝑋 +s 𝑚 ) ↔ 𝑎 = ( 𝑋 +s 𝑚 ) ) )
166	165	rexbidv	⊢ ( 𝑞 = 𝑎 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) ↔ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) )
167	161 166	elab	⊢ ( 𝑎 ∈ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ↔ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) )
168	164 167	orbi12i	⊢ ( ( 𝑎 ∈ { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∨ 𝑎 ∈ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) )
169	160 168	bitri	⊢ ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) )
170		elun	⊢ ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ↔ ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∨ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) )
171		vex	⊢ 𝑏 ∈ V
172		eqeq1	⊢ ( 𝑤 = 𝑏 → ( 𝑤 = ( 𝑟 +s 𝑌 ) ↔ 𝑏 = ( 𝑟 +s 𝑌 ) ) )
173	172	rexbidv	⊢ ( 𝑤 = 𝑏 → ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) ↔ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) )
174	171 173	elab	⊢ ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ↔ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) )
175		eqeq1	⊢ ( 𝑡 = 𝑏 → ( 𝑡 = ( 𝑋 +s 𝑠 ) ↔ 𝑏 = ( 𝑋 +s 𝑠 ) ) )
176	175	rexbidv	⊢ ( 𝑡 = 𝑏 → ( ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) ↔ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
177	171 176	elab	⊢ ( 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ↔ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) )
178	174 177	orbi12i	⊢ ( ( 𝑏 ∈ { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∨ 𝑏 ∈ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ↔ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
179	170 178	bitri	⊢ ( 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ↔ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
180	169 179	anbi12i	⊢ ( ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) ↔ ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) ∧ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) )
181		anddi	⊢ ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∨ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ) ∧ ( ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ∨ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ↔ ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ∨ ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ) )
182	180 181	bitri	⊢ ( ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) ↔ ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ∨ ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ) )
183		reeanv	⊢ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) )
184		lltropt	⊢ ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 )
185	184	a1i	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( L ‘ 𝑋 ) <<s ( R ‘ 𝑋 ) )
186		simprl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑙 ∈ ( L ‘ 𝑋 ) )
187		simprr	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ ( R ‘ 𝑋 ) )
188	185 186 187	ssltsepcd	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑙 <s 𝑟 )
189	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
190	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑌 ∈ No )
191	20	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑙 ∈ No )
192	95	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ No )
193		naddcom	⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) )
194	32 27 193	mp2an	⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) )
195	46	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
196	194 195	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
197		naddcom	⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) )
198	32 100 197	mp2an	⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) )
199	117	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
200	198 199	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
201		naddcl	⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ On )
202	32 27 201	mp2an	⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ On
203		naddcl	⊢ ( ( ( bday ‘ 𝑌 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ On )
204	32 100 203	mp2an	⊢ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ On
205		naddcl	⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On )
206	40 32 205	mp2an	⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On
207		onunel	⊢ ( ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ On ∧ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
208	202 204 206 207	mp3an	⊢ ( ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
209	196 200 208	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
210		elun1	⊢ ( ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
211	209 210	syl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑌 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
212	189 190 191 192 211	addsproplem1	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑌 +s 𝑙 ) ∈ No ∧ ( 𝑙 <s 𝑟 → ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) ) ) )
213	212	simprd	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑙 <s 𝑟 → ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) ) )
214	188 213	mpd	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) )
215		breq12	⊢ ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑙 +s 𝑌 ) <s ( 𝑟 +s 𝑌 ) ) )
216	214 215	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
217	216	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
218	183 217	biimtrrid	⊢ ( 𝜑 → ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
219		reeanv	⊢ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) ↔ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
220	52	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) ∈ No )
221	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
222	20	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑙 ∈ No )
223	131	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑠 ∈ No )
224	23	a1i	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 0s ∈ No )
225	30	uneq2i	⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑙 ) )
226		naddword1	⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) )
227	27 135 226	mp2an	⊢ ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
228		ssequn2	⊢ ( ( bday ‘ 𝑙 ) ⊆ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ↔ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) )
229	227 228	mpbi	⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
230	225 229	eqtri	⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
231		naddel1	⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) )
232	27 40 135 231	mp3an	⊢ ( ( bday ‘ 𝑙 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
233	43 232	sylib	⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
234	233	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
235	148	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
236		ontr1	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On → ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
237	206 236	ax-mp	⊢ ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
238	234 235 237	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
239		elun1	⊢ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
240	238 239	syl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
241	230 240	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
242	221 222 223 224 241	addsproplem1	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑙 +s 𝑠 ) ∈ No ∧ ( 𝑠 <s 0s → ( 𝑠 +s 𝑙 ) <s ( 0s +s 𝑙 ) ) ) )
243	242	simpld	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑠 ) ∈ No )
244	154	adantrl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑠 ) ∈ No )
245		rightval	⊢ ( R ‘ 𝑌 ) = { 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑌 <s 𝑠 }
246	245	reqabi	⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) ↔ ( 𝑠 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑌 <s 𝑠 ) )
247	246	simprbi	⊢ ( 𝑠 ∈ ( R ‘ 𝑌 ) → 𝑌 <s 𝑠 )
248	247	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑌 <s 𝑠 )
249	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑌 ∈ No )
250	46	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
251		naddcl	⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ On )
252	27 32 251	mp2an	⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ On
253		naddcl	⊢ ( ( ( bday ‘ 𝑙 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ On )
254	27 135 253	mp2an	⊢ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ On
255		onunel	⊢ ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ On ∧ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
256	252 254 206 255	mp3an	⊢ ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
257	250 238 256	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
258		elun1	⊢ ( ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
259	257 258	syl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
260	221 222 249 223 259	addsproplem1	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑙 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 𝑠 → ( 𝑌 +s 𝑙 ) <s ( 𝑠 +s 𝑙 ) ) ) )
261	260	simprd	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑌 <s 𝑠 → ( 𝑌 +s 𝑙 ) <s ( 𝑠 +s 𝑙 ) ) )
262	248 261	mpd	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑌 +s 𝑙 ) <s ( 𝑠 +s 𝑙 ) )
263	222 249	addscomd	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) = ( 𝑌 +s 𝑙 ) )
264	222 223	addscomd	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑠 ) = ( 𝑠 +s 𝑙 ) )
265	262 263 264	3brtr4d	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) <s ( 𝑙 +s 𝑠 ) )
266		leftval	⊢ ( L ‘ 𝑋 ) = { 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑙 <s 𝑋 }
267	266	reqabi	⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) ↔ ( 𝑙 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑙 <s 𝑋 ) )
268	267	simprbi	⊢ ( 𝑙 ∈ ( L ‘ 𝑋 ) → 𝑙 <s 𝑋 )
269	268	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑙 <s 𝑋 )
270	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑋 ∈ No )
271		naddcom	⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) ) )
272	135 27 271	mp2an	⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) = ( ( bday ‘ 𝑙 ) +no ( bday ‘ 𝑠 ) )
273	272 238	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
274		naddcom	⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) )
275	135 40 274	mp2an	⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) )
276	275 235	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
277		naddcl	⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑙 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ On )
278	135 27 277	mp2an	⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ On
279		naddcl	⊢ ( ( ( bday ‘ 𝑠 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ On )
280	135 40 279	mp2an	⊢ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ On
281		onunel	⊢ ( ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ On ∧ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
282	278 280 206 281	mp3an	⊢ ( ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
283	273 276 282	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
284		elun1	⊢ ( ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
285	283 284	syl	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑙 ) ) ∪ ( ( bday ‘ 𝑠 ) +no ( bday ‘ 𝑋 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
286	221 223 222 270 285	addsproplem1	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑠 +s 𝑙 ) ∈ No ∧ ( 𝑙 <s 𝑋 → ( 𝑙 +s 𝑠 ) <s ( 𝑋 +s 𝑠 ) ) ) )
287	286	simprd	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 <s 𝑋 → ( 𝑙 +s 𝑠 ) <s ( 𝑋 +s 𝑠 ) ) )
288	269 287	mpd	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑠 ) <s ( 𝑋 +s 𝑠 ) )
289	220 243 244 265 288	slttrd	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑙 +s 𝑌 ) <s ( 𝑋 +s 𝑠 ) )
290		breq12	⊢ ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑙 +s 𝑌 ) <s ( 𝑋 +s 𝑠 ) ) )
291	289 290	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑙 ∈ ( L ‘ 𝑋 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
292	291	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑙 +s 𝑌 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
293	219 292	biimtrrid	⊢ ( 𝜑 → ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
294	218 293	jaod	⊢ ( 𝜑 → ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) → 𝑎 <s 𝑏 ) )
295		reeanv	⊢ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) ↔ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) )
296	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
297	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑋 ∈ No )
298	60	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑚 ∈ No )
299	23	a1i	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 0s ∈ No )
300	81	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
301	300 83	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
302	73 301	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
303	296 297 298 299 302	addsproplem1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑋 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 0s → ( 𝑚 +s 𝑋 ) <s ( 0s +s 𝑋 ) ) ) )
304	303	simpld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 +s 𝑚 ) ∈ No )
305	95	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ No )
306	103	uneq2i	⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑟 ) )
307		naddword1	⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) )
308	100 68 307	mp2an	⊢ ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
309		ssequn2	⊢ ( ( bday ‘ 𝑟 ) ⊆ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ↔ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) )
310	308 309	mpbi	⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
311	306 310	eqtri	⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
312		naddel1	⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ) )
313	100 40 68 312	mp3an	⊢ ( ( bday ‘ 𝑟 ) ∈ ( bday ‘ 𝑋 ) ↔ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
314	114 313	sylib	⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
315	314	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
316		ontr1	⊢ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On → ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
317	206 316	ax-mp	⊢ ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
318	315 300 317	syl2anc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
319		elun1	⊢ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
320	318 319	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
321	311 320	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
322	296 305 298 299 321	addsproplem1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑟 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 0s → ( 𝑚 +s 𝑟 ) <s ( 0s +s 𝑟 ) ) ) )
323	322	simpld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑚 ) ∈ No )
324	3	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑌 ∈ No )
325	117	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
326	325 119	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
327	109 326	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 0s ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
328	296 305 324 299 327	addsproplem1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑟 +s 𝑌 ) ∈ No ∧ ( 𝑌 <s 0s → ( 𝑌 +s 𝑟 ) <s ( 0s +s 𝑟 ) ) ) )
329	328	simpld	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑌 ) ∈ No )
330		rightval	⊢ ( R ‘ 𝑋 ) = { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 }
331	330	eleq2i	⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) ↔ 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } )
332	331	biimpi	⊢ ( 𝑟 ∈ ( R ‘ 𝑋 ) → 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } )
333	332	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } )
334		rabid	⊢ ( 𝑟 ∈ { 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∣ 𝑋 <s 𝑟 } ↔ ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑟 ) )
335	333 334	sylib	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 ∈ ( O ‘ ( bday ‘ 𝑋 ) ) ∧ 𝑋 <s 𝑟 ) )
336	335	simprd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑋 <s 𝑟 )
337		naddcom	⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) )
338	68 40 337	mp2an	⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) = ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) )
339	338 300	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
340		naddcom	⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) )
341	68 100 340	mp2an	⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) = ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) )
342	341 318	eqeltrid	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
343		naddcl	⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑋 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ On )
344	68 40 343	mp2an	⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ On
345		naddcl	⊢ ( ( ( bday ‘ 𝑚 ) ∈ On ∧ ( bday ‘ 𝑟 ) ∈ On ) → ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ On )
346	68 100 345	mp2an	⊢ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ On
347		onunel	⊢ ( ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ On ∧ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
348	344 346 206 347	mp3an	⊢ ( ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
349	339 342 348	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
350		elun1	⊢ ( ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
351	349 350	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑋 ) ) ∪ ( ( bday ‘ 𝑚 ) +no ( bday ‘ 𝑟 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
352	296 298 297 305 351	addsproplem1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑚 +s 𝑋 ) ∈ No ∧ ( 𝑋 <s 𝑟 → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑚 ) ) ) )
353	352	simprd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 <s 𝑟 → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑚 ) ) )
354	336 353	mpd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑚 ) )
355		leftval	⊢ ( L ‘ 𝑌 ) = { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 }
356	355	eleq2i	⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) ↔ 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } )
357	356	biimpi	⊢ ( 𝑚 ∈ ( L ‘ 𝑌 ) → 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } )
358	357	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } )
359		rabid	⊢ ( 𝑚 ∈ { 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∣ 𝑚 <s 𝑌 } ↔ ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑚 <s 𝑌 ) )
360	358 359	sylib	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑚 ∈ ( O ‘ ( bday ‘ 𝑌 ) ) ∧ 𝑚 <s 𝑌 ) )
361	360	simprd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → 𝑚 <s 𝑌 )
362		naddcl	⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ On )
363	100 68 362	mp2an	⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ On
364		naddcl	⊢ ( ( ( bday ‘ 𝑟 ) ∈ On ∧ ( bday ‘ 𝑌 ) ∈ On ) → ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ On )
365	100 32 364	mp2an	⊢ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ On
366		onunel	⊢ ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ On ∧ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
367	363 365 206 366	mp3an	⊢ ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
368	318 325 367	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
369		elun1	⊢ ( ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
370	368 369	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑟 ) +no ( bday ‘ 𝑌 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
371	296 305 298 324 370	addsproplem1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑟 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 𝑌 → ( 𝑚 +s 𝑟 ) <s ( 𝑌 +s 𝑟 ) ) ) )
372	371	simprd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑚 <s 𝑌 → ( 𝑚 +s 𝑟 ) <s ( 𝑌 +s 𝑟 ) ) )
373	361 372	mpd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑚 +s 𝑟 ) <s ( 𝑌 +s 𝑟 ) )
374	305 298	addscomd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑚 ) = ( 𝑚 +s 𝑟 ) )
375	305 324	addscomd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑌 ) = ( 𝑌 +s 𝑟 ) )
376	373 374 375	3brtr4d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑟 +s 𝑚 ) <s ( 𝑟 +s 𝑌 ) )
377	304 323 329 354 376	slttrd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑌 ) )
378		breq12	⊢ ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑋 +s 𝑚 ) <s ( 𝑟 +s 𝑌 ) ) )
379	377 378	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑟 ∈ ( R ‘ 𝑋 ) ) ) → ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
380	379	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑟 ∈ ( R ‘ 𝑋 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
381	295 380	biimtrrid	⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) → 𝑎 <s 𝑏 ) )
382		reeanv	⊢ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) ↔ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) )
383		lltropt	⊢ ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 )
384	383	a1i	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( L ‘ 𝑌 ) <<s ( R ‘ 𝑌 ) )
385		simprl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑚 ∈ ( L ‘ 𝑌 ) )
386		simprr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑠 ∈ ( R ‘ 𝑌 ) )
387	384 385 386	ssltsepcd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑚 <s 𝑠 )
388	1	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ∀ 𝑥 ∈ No ∀ 𝑦 ∈ No ∀ 𝑧 ∈ No ( ( ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑦 ) ) ∪ ( ( bday ‘ 𝑥 ) +no ( bday ‘ 𝑧 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) → ( ( 𝑥 +s 𝑦 ) ∈ No ∧ ( 𝑦 <s 𝑧 → ( 𝑦 +s 𝑥 ) <s ( 𝑧 +s 𝑥 ) ) ) ) )
389	2	adantr	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑋 ∈ No )
390	60	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑚 ∈ No )
391	131	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → 𝑠 ∈ No )
392	81	ad2antrl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
393	148	ad2antll	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
394		naddcl	⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑚 ) ∈ On ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ On )
395	40 68 394	mp2an	⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ On
396		naddcl	⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ ( bday ‘ 𝑠 ) ∈ On ) → ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ On )
397	40 135 396	mp2an	⊢ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ On
398		onunel	⊢ ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ On ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∈ On ) → ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) ) )
399	395 397 206 398	mp3an	⊢ ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ↔ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∧ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ) )
400	392 393 399	sylanbrc	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) )
401		elun1	⊢ ( ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
402	400 401	syl	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑚 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑠 ) ) ) ∈ ( ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑌 ) ) ∪ ( ( bday ‘ 𝑋 ) +no ( bday ‘ 𝑍 ) ) ) )
403	388 389 390 391 402	addsproplem1	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑋 +s 𝑚 ) ∈ No ∧ ( 𝑚 <s 𝑠 → ( 𝑚 +s 𝑋 ) <s ( 𝑠 +s 𝑋 ) ) ) )
404	403	simprd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑚 <s 𝑠 → ( 𝑚 +s 𝑋 ) <s ( 𝑠 +s 𝑋 ) ) )
405	387 404	mpd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑚 +s 𝑋 ) <s ( 𝑠 +s 𝑋 ) )
406	389 390	addscomd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑚 ) = ( 𝑚 +s 𝑋 ) )
407	389 391	addscomd	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑠 ) = ( 𝑠 +s 𝑋 ) )
408	405 406 407	3brtr4d	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( 𝑋 +s 𝑚 ) <s ( 𝑋 +s 𝑠 ) )
409		breq12	⊢ ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → ( 𝑎 <s 𝑏 ↔ ( 𝑋 +s 𝑚 ) <s ( 𝑋 +s 𝑠 ) ) )
410	408 409	syl5ibrcom	⊢ ( ( 𝜑 ∧ ( 𝑚 ∈ ( L ‘ 𝑌 ) ∧ 𝑠 ∈ ( R ‘ 𝑌 ) ) ) → ( ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
411	410	rexlimdvva	⊢ ( 𝜑 → ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) ∃ 𝑠 ∈ ( R ‘ 𝑌 ) ( 𝑎 = ( 𝑋 +s 𝑚 ) ∧ 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
412	382 411	biimtrrid	⊢ ( 𝜑 → ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) → 𝑎 <s 𝑏 ) )
413	381 412	jaod	⊢ ( 𝜑 → ( ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) → 𝑎 <s 𝑏 ) )
414	294 413	jaod	⊢ ( 𝜑 → ( ( ( ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑎 = ( 𝑙 +s 𝑌 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ∨ ( ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑏 = ( 𝑟 +s 𝑌 ) ) ∨ ( ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑎 = ( 𝑋 +s 𝑚 ) ∧ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑏 = ( 𝑋 +s 𝑠 ) ) ) ) → 𝑎 <s 𝑏 ) )
415	182 414	biimtrid	⊢ ( 𝜑 → ( ( 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) → 𝑎 <s 𝑏 ) )
416	415	3impib	⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) ∧ 𝑏 ∈ ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) ) → 𝑎 <s 𝑏 )
417	10 17 92 159 416	ssltd	⊢ ( 𝜑 → ( { 𝑝 ∣ ∃ 𝑙 ∈ ( L ‘ 𝑋 ) 𝑝 = ( 𝑙 +s 𝑌 ) } ∪ { 𝑞 ∣ ∃ 𝑚 ∈ ( L ‘ 𝑌 ) 𝑞 = ( 𝑋 +s 𝑚 ) } ) <<s ( { 𝑤 ∣ ∃ 𝑟 ∈ ( R ‘ 𝑋 ) 𝑤 = ( 𝑟 +s 𝑌 ) } ∪ { 𝑡 ∣ ∃ 𝑠 ∈ ( R ‘ 𝑌 ) 𝑡 = ( 𝑋 +s 𝑠 ) } ) )