addsproplem2 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > addsproplem2		Structured version Visualization version GIF version

Theorem addsproplem2 28021

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.)

**Hypotheses**
Ref	Expression
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**
Ref	Expression
addsproplem2	⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)}))

Distinct variable groups: 𝑋,𝑙,𝑚 𝑋,𝑝,𝑞,𝑟 𝑋,𝑠,𝑡,𝑟 𝑤,𝑋 𝑥,𝑋,𝑦,𝑧 𝑌,𝑙,𝑚 𝑌,𝑝,𝑞,𝑟 𝑌,𝑠,𝑡 𝑤,𝑌 𝑥,𝑌,𝑦,𝑧 𝑥,𝑍,𝑦,𝑧 𝜑,𝑙,𝑚 𝜑,𝑝,𝑞,𝑟 𝜑,𝑠,𝑡 𝑝,𝑙,𝑟 𝑠,𝑙,𝑥,𝑦,𝑧 𝑚,𝑞,𝑟,𝑠 𝑥,𝑚,𝑦,𝑧 𝜑,𝑤,𝑟 𝑥,𝑟,𝑦,𝑧,𝑠 𝑞,𝑙 𝑟,𝑝,𝑞 𝑤,𝑝 𝑠,𝑞,𝑡 Allowed substitution hints: 𝜑(𝑥,𝑦,𝑧) 𝑍(𝑤,𝑡,𝑚,𝑠,𝑟,𝑞,𝑝,𝑙)

Proof of Theorem addsproplem2 Dummy variables 𝑎 𝑏 are mutually distinct and distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 ∨ wo 846 = wceq 1537 ∈ wcel 2108 {cab 2717 ∀wral 3067 ∃wrex 3076 {crab 3443 Vcvv 3488 ∪ cun 3974 ⊆ wss 3976 ∅c0 4352 class class class wbr 5166 Oncon0 6395 ‘cfv 6573 (class class class)co 7448 +no cnadd 8721 No csur 27702 <s cslt 27703 bday cbday 27704 <<s csslt 27843 0_s c0s 27885 O cold 27900 L cleft 27902 R cright 27903 +_s cadds 28010

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2158 ax-12 2178 ax-ext 2711 ax-rep 5303 ax-sep 5317 ax-nul 5324 ax-pow 5383 ax-pr 5447 ax-un 7770

This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2543 df-eu 2572 df-clab 2718 df-cleq 2732 df-clel 2819 df-nfc 2895 df-ne 2947 df-ral 3068 df-rex 3077 df-rmo 3388 df-reu 3389 df-rab 3444 df-v 3490 df-sbc 3805 df-csb 3922 df-dif 3979 df-un 3981 df-in 3983 df-ss 3993 df-pss 3996 df-nul 4353 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4971 df-iun 5017 df-br 5167 df-opab 5229 df-mpt 5250 df-tr 5284 df-id 5593 df-eprel 5599 df-po 5607 df-so 5608 df-fr 5652 df-se 5653 df-we 5654 df-xp 5706 df-rel 5707 df-cnv 5708 df-co 5709 df-dm 5710 df-rn 5711 df-res 5712 df-ima 5713 df-pred 6332 df-ord 6398 df-on 6399 df-suc 6401 df-iota 6525 df-fun 6575 df-fn 6576 df-f 6577 df-f1 6578 df-fo 6579 df-f1o 6580 df-fv 6581 df-riota 7404 df-ov 7451 df-oprab 7452 df-mpo 7453 df-1st 8030 df-2nd 8031 df-frecs 8322 df-wrecs 8353 df-recs 8427 df-1o 8522 df-2o 8523 df-nadd 8722 df-no 27705 df-slt 27706 df-bday 27707 df-sslt 27844 df-scut 27846 df-0s 27887 df-made 27904 df-old 27905 df-left 27907 df-right 27908 df-norec2 28000 df-adds 28011

This theorem is referenced by: addsproplem3 28022

W3C validator