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 28003

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 6919	. . . . 5 ⊢ ( L ‘𝑋) ∈ V
2	1	abrexex 7987	. . . 4 ⊢ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∈ V
3	2	a1i 11	. . 3 ⊢ (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∈ V)
4		fvex 6919	. . . . 5 ⊢ ( L ‘𝑌) ∈ V
5	4	abrexex 7987	. . . 4 ⊢ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)} ∈ V
6	5	a1i 11	. . 3 ⊢ (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)} ∈ V)
7	3, 6	unexd 7774	. 2 ⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ∈ V)
8		fvex 6919	. . . . 5 ⊢ ( R ‘𝑋) ∈ V
9	8	abrexex 7987	. . . 4 ⊢ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∈ V
10	9	a1i 11	. . 3 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∈ V)
11		fvex 6919	. . . . 5 ⊢ ( R ‘𝑌) ∈ V
12	11	abrexex 7987	. . . 4 ⊢ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)} ∈ V
13	12	a1i 11	. . 3 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)} ∈ V)
14	10, 13	unexd 7774	. 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 27919	. . . . . . . . . 10 ⊢ ( L ‘𝑋) ⊆ No
18	17	sseli 3979	. . . . . . . . 9 ⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ No )
19	18	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 𝑙 ∈ No )
20		addsproplem2.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ No )
21	20	adantr 480	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 𝑌 ∈ No )
22		0sno 27871	. . . . . . . . 9 ⊢ 0_s ∈ No
23	22	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 0_s ∈ No )
24		bday0s 27873	. . . . . . . . . . . . 13 ⊢ ( bday ‘ 0_s ) = ∅
25	24	oveq2i 7442	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑙) +no ( bday ‘ 0_s )) = (( bday ‘𝑙) +no ∅)
26		bdayelon 27821	. . . . . . . . . . . . 13 ⊢ ( bday ‘𝑙) ∈ On
27		naddrid 8721	. . . . . . . . . . . . 13 ⊢ (( bday ‘𝑙) ∈ On → (( bday ‘𝑙) +no ∅) = ( bday ‘𝑙))
28	26, 27	ax-mp 5	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑙) +no ∅) = ( bday ‘𝑙)
29	25, 28	eqtri 2765	. . . . . . . . . . 11 ⊢ (( bday ‘𝑙) +no ( bday ‘ 0_s )) = ( bday ‘𝑙)
30	29	uneq2i 4165	. . . . . . . . . 10 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑙))
31		bdayelon 27821	. . . . . . . . . . . 12 ⊢ ( bday ‘𝑌) ∈ On
32		naddword1 8729	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑌) ∈ On) → ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑌)))
33	26, 31, 32	mp2an 692	. . . . . . . . . . 11 ⊢ ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑌))
34		ssequn2 4189	. . . . . . . . . . 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 2765	. . . . . . . . 9 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) = (( bday ‘𝑙) +no ( bday ‘𝑌))
37		leftssold 27917	. . . . . . . . . . . . . 14 ⊢ ( L ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
38	37	sseli 3979	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ ( O ‘( bday ‘𝑋)))
39		bdayelon 27821	. . . . . . . . . . . . . 14 ⊢ ( bday ‘𝑋) ∈ On
40		oldbday 27939	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑙 ∈ No ) → (𝑙 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑙) ∈ ( bday ‘𝑋)))
41	39, 18, 40	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ ( L ‘𝑋) → (𝑙 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑙) ∈ ( bday ‘𝑋)))
42	38, 41	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝑙 ∈ ( L ‘𝑋) → ( bday ‘𝑙) ∈ ( bday ‘𝑋))
43		naddel1 8725	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑙) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
44	26, 39, 31, 43	mp3an 1463	. . . . . . . . . . . 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 4182	. . . . . . . . . 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 2845	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
50	16, 19, 21, 23, 49	addsproplem1 28002	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → ((𝑙 +_s 𝑌) ∈ No ∧ (𝑌 <s 0_s → (𝑌 +_s 𝑙) <s ( 0_s +_s 𝑙))))
51	50	simpld 494	. . . . . 6 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (𝑙 +_s 𝑌) ∈ No )
52		eleq1a 2836	. . . . . 6 ⊢ ((𝑙 +_s 𝑌) ∈ No → (𝑝 = (𝑙 +_s 𝑌) → 𝑝 ∈ No ))
53	51, 52	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (𝑝 = (𝑙 +_s 𝑌) → 𝑝 ∈ No ))
54	53	rexlimdva 3155	. . . 4 ⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌) → 𝑝 ∈ No ))
55	54	abssdv 4068	. . 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 27919	. . . . . . . . . 10 ⊢ ( L ‘𝑌) ⊆ No
60	59	sseli 3979	. . . . . . . . 9 ⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ No )
61	60	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 𝑚 ∈ No )
62	22	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 0_s ∈ No )
63	24	oveq2i 7442	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑋) +no ( bday ‘ 0_s )) = (( bday ‘𝑋) +no ∅)
64		naddrid 8721	. . . . . . . . . . . . 13 ⊢ (( bday ‘𝑋) ∈ On → (( bday ‘𝑋) +no ∅) = ( bday ‘𝑋))
65	39, 64	ax-mp 5	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑋) +no ∅) = ( bday ‘𝑋)
66	63, 65	eqtri 2765	. . . . . . . . . . 11 ⊢ (( bday ‘𝑋) +no ( bday ‘ 0_s )) = ( bday ‘𝑋)
67	66	uneq2i 4165	. . . . . . . . . 10 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑋))
68		bdayelon 27821	. . . . . . . . . . . 12 ⊢ ( bday ‘𝑚) ∈ On
69		naddword1 8729	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑚) ∈ On) → ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑚)))
70	39, 68, 69	mp2an 692	. . . . . . . . . . 11 ⊢ ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑚))
71		ssequn2 4189	. . . . . . . . . . 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 2765	. . . . . . . . 9 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) = (( bday ‘𝑋) +no ( bday ‘𝑚))
74		leftssold 27917	. . . . . . . . . . . . . 14 ⊢ ( L ‘𝑌) ⊆ ( O ‘( bday ‘𝑌))
75	74	sseli 3979	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ ( O ‘( bday ‘𝑌)))
76		oldbday 27939	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑌) ∈ On ∧ 𝑚 ∈ No ) → (𝑚 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑚) ∈ ( bday ‘𝑌)))
77	31, 60, 76	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ( L ‘𝑌) → (𝑚 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑚) ∈ ( bday ‘𝑌)))
78	75, 77	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ( L ‘𝑌) → ( bday ‘𝑚) ∈ ( bday ‘𝑌))
79		naddel2 8726	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑚) ∈ ( bday ‘𝑌) ↔ (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
80	68, 31, 39, 79	mp3an 1463	. . . . . . . . . . . 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 4182	. . . . . . . . . 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 2845	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
86	56, 58, 61, 62, 85	addsproplem1 28002	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → ((𝑋 +_s 𝑚) ∈ No ∧ (𝑚 <s 0_s → (𝑚 +_s 𝑋) <s ( 0_s +_s 𝑋))))
87	86	simpld 494	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (𝑋 +_s 𝑚) ∈ No )
88		eleq1a 2836	. . . . . 6 ⊢ ((𝑋 +_s 𝑚) ∈ No → (𝑞 = (𝑋 +_s 𝑚) → 𝑞 ∈ No ))
89	87, 88	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (𝑞 = (𝑋 +_s 𝑚) → 𝑞 ∈ No ))
90	89	rexlimdva 3155	. . . 4 ⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚) → 𝑞 ∈ No ))
91	90	abssdv 4068	. . 3 ⊢ (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)} ⊆ No )
92	55, 91	unssd 4192	. 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 27920	. . . . . . . . . 10 ⊢ ( R ‘𝑋) ⊆ No
95	94	sseli 3979	. . . . . . . . 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 7442	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑟) +no ( bday ‘ 0_s )) = (( bday ‘𝑟) +no ∅)
100		bdayelon 27821	. . . . . . . . . . . . 13 ⊢ ( bday ‘𝑟) ∈ On
101		naddrid 8721	. . . . . . . . . . . . 13 ⊢ (( bday ‘𝑟) ∈ On → (( bday ‘𝑟) +no ∅) = ( bday ‘𝑟))
102	100, 101	ax-mp 5	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑟) +no ∅) = ( bday ‘𝑟)
103	99, 102	eqtri 2765	. . . . . . . . . . 11 ⊢ (( bday ‘𝑟) +no ( bday ‘ 0_s )) = ( bday ‘𝑟)
104	103	uneq2i 4165	. . . . . . . . . 10 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑟))
105		naddword1 8729	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑌) ∈ On) → ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑌)))
106	100, 31, 105	mp2an 692	. . . . . . . . . . 11 ⊢ ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑌))
107		ssequn2 4189	. . . . . . . . . . 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 2765	. . . . . . . . 9 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) = (( bday ‘𝑟) +no ( bday ‘𝑌))
110		rightssold 27918	. . . . . . . . . . . . . 14 ⊢ ( R ‘𝑋) ⊆ ( O ‘( bday ‘𝑋))
111	110	sseli 3979	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ ( O ‘( bday ‘𝑋)))
112		oldbday 27939	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑟 ∈ No ) → (𝑟 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑟) ∈ ( bday ‘𝑋)))
113	39, 95, 112	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ( R ‘𝑋) → (𝑟 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑟) ∈ ( bday ‘𝑋)))
114	111, 113	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ( R ‘𝑋) → ( bday ‘𝑟) ∈ ( bday ‘𝑋))
115		naddel1 8725	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑟) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
116	100, 39, 31, 115	mp3an 1463	. . . . . . . . . . . 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 4182	. . . . . . . . . 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 2845	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
122	93, 96, 97, 98, 121	addsproplem1 28002	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → ((𝑟 +_s 𝑌) ∈ No ∧ (𝑌 <s 0_s → (𝑌 +_s 𝑟) <s ( 0_s +_s 𝑟))))
123	122	simpld 494	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (𝑟 +_s 𝑌) ∈ No )
124		eleq1a 2836	. . . . . 6 ⊢ ((𝑟 +_s 𝑌) ∈ No → (𝑤 = (𝑟 +_s 𝑌) → 𝑤 ∈ No ))
125	123, 124	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (𝑤 = (𝑟 +_s 𝑌) → 𝑤 ∈ No ))
126	125	rexlimdva 3155	. . . 4 ⊢ (𝜑 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌) → 𝑤 ∈ No ))
127	126	abssdv 4068	. . 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 27920	. . . . . . . . . 10 ⊢ ( R ‘𝑌) ⊆ No
131	130	sseli 3979	. . . . . . . . 9 ⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ No )
132	131	adantl 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 𝑠 ∈ No )
133	22	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 0_s ∈ No )
134	66	uneq2i 4165	. . . . . . . . . 10 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑋))
135		bdayelon 27821	. . . . . . . . . . . 12 ⊢ ( bday ‘𝑠) ∈ On
136		naddword1 8729	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑠) ∈ On) → ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑠)))
137	39, 135, 136	mp2an 692	. . . . . . . . . . 11 ⊢ ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑠))
138		ssequn2 4189	. . . . . . . . . . 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 2765	. . . . . . . . 9 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) = (( bday ‘𝑋) +no ( bday ‘𝑠))
141		rightssold 27918	. . . . . . . . . . . . . 14 ⊢ ( R ‘𝑌) ⊆ ( O ‘( bday ‘𝑌))
142	141	sseli 3979	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ ( O ‘( bday ‘𝑌)))
143		oldbday 27939	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑌) ∈ On ∧ 𝑠 ∈ No ) → (𝑠 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑠) ∈ ( bday ‘𝑌)))
144	31, 131, 143	sylancr 587	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ( R ‘𝑌) → (𝑠 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑠) ∈ ( bday ‘𝑌)))
145	142, 144	mpbid 232	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ( R ‘𝑌) → ( bday ‘𝑠) ∈ ( bday ‘𝑌))
146		naddel2 8726	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑠) ∈ ( bday ‘𝑌) ↔ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
147	135, 31, 39, 146	mp3an 1463	. . . . . . . . . . . 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 4182	. . . . . . . . . 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 2845	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
153	128, 129, 132, 133, 152	addsproplem1 28002	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ((𝑋 +_s 𝑠) ∈ No ∧ (𝑠 <s 0_s → (𝑠 +_s 𝑋) <s ( 0_s +_s 𝑋))))
154	153	simpld 494	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (𝑋 +_s 𝑠) ∈ No )
155		eleq1a 2836	. . . . . 6 ⊢ ((𝑋 +_s 𝑠) ∈ No → (𝑡 = (𝑋 +_s 𝑠) → 𝑡 ∈ No ))
156	154, 155	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (𝑡 = (𝑋 +_s 𝑠) → 𝑡 ∈ No ))
157	156	rexlimdva 3155	. . . 4 ⊢ (𝜑 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠) → 𝑡 ∈ No ))
158	157	abssdv 4068	. . 3 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)} ⊆ No )
159	127, 158	unssd 4192	. 2 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)}) ⊆ No )
160		elun 4153	. . . . . . 7 ⊢ (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ↔ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}))
161		vex 3484	. . . . . . . . 9 ⊢ 𝑎 ∈ V
162		eqeq1 2741	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → (𝑝 = (𝑙 +_s 𝑌) ↔ 𝑎 = (𝑙 +_s 𝑌)))
163	162	rexbidv 3179	. . . . . . . . 9 ⊢ (𝑝 = 𝑎 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌) ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌)))
164	161, 163	elab 3679	. . . . . . . 8 ⊢ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌))
165		eqeq1 2741	. . . . . . . . . 10 ⊢ (𝑞 = 𝑎 → (𝑞 = (𝑋 +_s 𝑚) ↔ 𝑎 = (𝑋 +_s 𝑚)))
166	165	rexbidv 3179	. . . . . . . . 9 ⊢ (𝑞 = 𝑎 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚) ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚)))
167	161, 166	elab 3679	. . . . . . . 8 ⊢ (𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)} ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚))
168	164, 167	orbi12i 915	. . . . . . 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 4153	. . . . . . 7 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)}))
171		vex 3484	. . . . . . . . 9 ⊢ 𝑏 ∈ V
172		eqeq1 2741	. . . . . . . . . 10 ⊢ (𝑤 = 𝑏 → (𝑤 = (𝑟 +_s 𝑌) ↔ 𝑏 = (𝑟 +_s 𝑌)))
173	172	rexbidv 3179	. . . . . . . . 9 ⊢ (𝑤 = 𝑏 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌) ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)))
174	171, 173	elab 3679	. . . . . . . 8 ⊢ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌))
175		eqeq1 2741	. . . . . . . . . 10 ⊢ (𝑡 = 𝑏 → (𝑡 = (𝑋 +_s 𝑠) ↔ 𝑏 = (𝑋 +_s 𝑠)))
176	175	rexbidv 3179	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠) ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)))
177	171, 176	elab 3679	. . . . . . . 8 ⊢ (𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)} ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠))
178	174, 177	orbi12i 915	. . . . . . 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 628	. . . . 5 ⊢ ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)})) ↔ ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚)) ∧ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠))))
181		anddi 1013	. . . . 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 3229	. . . . . . 7 ⊢ (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)))
184		lltropt 27911	. . . . . . . . . . . 12 ⊢ ( L ‘𝑋) <<s ( R ‘𝑋)
185	184	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ( L ‘𝑋) <<s ( R ‘𝑋))
186		simprl 771	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ ( L ‘𝑋))
187		simprr 773	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ ( R ‘𝑋))
188	185, 186, 187	ssltsepcd 27839	. . . . . . . . . 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 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ No )
192	95	ad2antll 729	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ No )
193		naddcom 8720	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑌)))
194	31, 26, 193	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑌) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑌))
195	45	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
196	194, 195	eqeltrid 2845	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
197		naddcom 8720	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑌)))
198	31, 100, 197	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑌) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑌))
199	117	ad2antll 729	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
200	198, 199	eqeltrid 2845	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
201		naddcl 8715	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ On)
202	31, 26, 201	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ On
203		naddcl 8715	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ On)
204	31, 100, 203	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ On
205		naddcl 8715	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On)
206	39, 31, 205	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On
207		onunel 6489	. . . . . . . . . . . . . . 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 1463	. . . . . . . . . . . . . 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 583	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑌) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
210		elun1 4182	. . . . . . . . . . . . 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 28002	. . . . . . . . . . 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 5148	. . . . . . . . 9 ⊢ ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑙 +_s 𝑌) <s (𝑟 +_s 𝑌)))
216	214, 215	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
217	216	rexlimdvva 3213	. . . . . . 7 ⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
218	183, 217	biimtrrid 243	. . . . . 6 ⊢ (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
219		reeanv 3229	. . . . . . 7 ⊢ (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑋 +_s 𝑠)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)))
220	51	adantrr 717	. . . . . . . . . 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 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 ∈ No )
223	131	ad2antll 729	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ No )
224	22	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 0_s ∈ No )
225	29	uneq2i 4165	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑙))
226		naddword1 8729	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑠) ∈ On) → ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑠)))
227	26, 135, 226	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑠))
228		ssequn2 4189	. . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) = (( bday ‘𝑙) +no ( bday ‘𝑠))
231		naddel1 8725	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑠) ∈ On) → (( bday ‘𝑙) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠))))
232	26, 39, 135, 231	mp3an 1463	. . . . . . . . . . . . . . . . 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 728	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠)))
235	148	ad2antll 729	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
236		ontr1 6430	. . . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
239		elun1 4182	. . . . . . . . . . . . . 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 2845	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
242	221, 222, 223, 224, 241	addsproplem1 28002	. . . . . . . . . . 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 716	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +_s 𝑠) ∈ No )
245		rightval 27903	. . . . . . . . . . . . . . 15 ⊢ ( R ‘𝑌) = {𝑠 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑌 <s 𝑠}
246	245	reqabi 3460	. . . . . . . . . . . . . 14 ⊢ (𝑠 ∈ ( R ‘𝑌) ↔ (𝑠 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑌 <s 𝑠))
247	246	simprbi 496	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑌 <s 𝑠)
248	247	ad2antll 729	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 <s 𝑠)
249	20	adantr 480	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 ∈ No )
250	45	ad2antrl 728	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
251		naddcl 8715	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ On)
252	26, 31, 251	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ On
253		naddcl 8715	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑠) ∈ On) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ On)
254	26, 135, 253	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ On
255		onunel 6489	. . . . . . . . . . . . . . . . 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 1463	. . . . . . . . . . . . . . . 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 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
258		elun1 4182	. . . . . . . . . . . . . . 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 28002	. . . . . . . . . . . . 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 28000	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +_s 𝑌) = (𝑌 +_s 𝑙))
264	222, 223	addscomd 28000	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +_s 𝑠) = (𝑠 +_s 𝑙))
265	262, 263, 264	3brtr4d 5175	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +_s 𝑌) <s (𝑙 +_s 𝑠))
266		leftval 27902	. . . . . . . . . . . . . 14 ⊢ ( L ‘𝑋) = {𝑙 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑙 <s 𝑋}
267	266	reqabi 3460	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ ( L ‘𝑋) ↔ (𝑙 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑙 <s 𝑋))
268	267	simprbi 496	. . . . . . . . . . . 12 ⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 <s 𝑋)
269	268	ad2antrl 728	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 <s 𝑋)
270	57	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 ∈ No )
271		naddcom 8720	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑠)))
272	135, 26, 271	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑠) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑠))
273	272, 238	eqeltrid 2845	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
274		naddcom 8720	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑠)))
275	135, 39, 274	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑠) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑠))
276	275, 235	eqeltrid 2845	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
277		naddcl 8715	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ On)
278	135, 26, 277	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ On
279		naddcl 8715	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ On)
280	135, 39, 279	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ On
281		onunel 6489	. . . . . . . . . . . . . . . 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 1463	. . . . . . . . . . . . . . 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 583	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑠) +no ( bday ‘𝑋))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
284		elun1 4182	. . . . . . . . . . . . . 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 28002	. . . . . . . . . . . 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 27804	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +_s 𝑌) <s (𝑋 +_s 𝑠))
290		breq12 5148	. . . . . . . . 9 ⊢ ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑋 +_s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑙 +_s 𝑌) <s (𝑋 +_s 𝑠)))
291	289, 290	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
292	291	rexlimdvva 3213	. . . . . . 7 ⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
293	219, 292	biimtrrid 243	. . . . . 6 ⊢ (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
294	218, 293	jaod 860	. . . . 5 ⊢ (𝜑 → (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠))) → 𝑎 <s 𝑏))
295		reeanv 3229	. . . . . . 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 728	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ No )
299	22	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 0_s ∈ No )
300	81	ad2antrl 728	. . . . . . . . . . . . . 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 2845	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
303	296, 297, 298, 299, 302	addsproplem1 28002	. . . . . . . . . . 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 729	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ No )
306	103	uneq2i 4165	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑟))
307		naddword1 8729	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑚) ∈ On) → ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑚)))
308	100, 68, 307	mp2an 692	. . . . . . . . . . . . . . 15 ⊢ ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑚))
309		ssequn2 4189	. . . . . . . . . . . . . . 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 2765	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) = (( bday ‘𝑟) +no ( bday ‘𝑚))
312		naddel1 8725	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑚) ∈ On) → (( bday ‘𝑟) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚))))
313	100, 39, 68, 312	mp3an 1463	. . . . . . . . . . . . . . . . 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 729	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚)))
316		ontr1 6430	. . . . . . . . . . . . . . . 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 584	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
319		elun1 4182	. . . . . . . . . . . . . 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 2845	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
322	296, 305, 298, 299, 321	addsproplem1 28002	. . . . . . . . . . 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 729	. . . . . . . . . . . . . 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 2845	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
328	296, 305, 324, 299, 327	addsproplem1 28002	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +_s 𝑌) ∈ No ∧ (𝑌 <s 0_s → (𝑌 +_s 𝑟) <s ( 0_s +_s 𝑟))))
329	328	simpld 494	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +_s 𝑌) ∈ No )
330		rightval 27903	. . . . . . . . . . . . . . . 16 ⊢ ( R ‘𝑋) = {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟}
331	330	eleq2i 2833	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ ( R ‘𝑋) ↔ 𝑟 ∈ {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟})
332	331	biimpi 216	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟})
333	332	ad2antll 729	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟})
334		rabid 3458	. . . . . . . . . . . . 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 8720	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑚)))
338	68, 39, 337	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑚) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑚))
339	338, 300	eqeltrid 2845	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
340		naddcom 8720	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑚)))
341	68, 100, 340	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑚) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑚))
342	341, 318	eqeltrid 2845	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
343		naddcl 8715	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ On)
344	68, 39, 343	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ On
345		naddcl 8715	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ On)
346	68, 100, 345	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ On
347		onunel 6489	. . . . . . . . . . . . . . . 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 1463	. . . . . . . . . . . . . . 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 583	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday ‘𝑚) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
350		elun1 4182	. . . . . . . . . . . . . 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 28002	. . . . . . . . . . . 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 27902	. . . . . . . . . . . . . . . . 17 ⊢ ( L ‘𝑌) = {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌}
356	355	eleq2i 2833	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ( L ‘𝑌) ↔ 𝑚 ∈ {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌})
357	356	biimpi 216	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌})
358	357	ad2antrl 728	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌})
359		rabid 3458	. . . . . . . . . . . . . 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 8715	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑚) ∈ On) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ On)
363	100, 68, 362	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ On
364		naddcl 8715	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ On)
365	100, 31, 364	mp2an 692	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ On
366		onunel 6489	. . . . . . . . . . . . . . . . 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 1463	. . . . . . . . . . . . . . . 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 583	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘𝑌))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
369		elun1 4182	. . . . . . . . . . . . . . 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 28002	. . . . . . . . . . . . 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 28000	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +_s 𝑚) = (𝑚 +_s 𝑟))
375	305, 324	addscomd 28000	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +_s 𝑌) = (𝑌 +_s 𝑟))
376	373, 374, 375	3brtr4d 5175	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +_s 𝑚) <s (𝑟 +_s 𝑌))
377	304, 323, 329, 354, 376	slttrd 27804	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +_s 𝑚) <s (𝑟 +_s 𝑌))
378		breq12 5148	. . . . . . . . 9 ⊢ ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑟 +_s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑋 +_s 𝑚) <s (𝑟 +_s 𝑌)))
379	377, 378	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
380	379	rexlimdvva 3213	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
381	295, 380	biimtrrid 243	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
382		reeanv 3229	. . . . . . 7 ⊢ (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑋 +_s 𝑠)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)))
383		lltropt 27911	. . . . . . . . . . . . 13 ⊢ ( L ‘𝑌) <<s ( R ‘𝑌)
384	383	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ( L ‘𝑌) <<s ( R ‘𝑌))
385		simprl 771	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ ( L ‘𝑌))
386		simprr 773	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ ( R ‘𝑌))
387	384, 385, 386	ssltsepcd 27839	. . . . . . . . . . 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 728	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ No )
391	131	ad2antll 729	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ No )
392	81	ad2antrl 728	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
393	148	ad2antll 729	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
394		naddcl 8715	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑚) ∈ On) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ On)
395	39, 68, 394	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ On
396		naddcl 8715	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑠) ∈ On) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ On)
397	39, 135, 396	mp2an 692	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ On
398		onunel 6489	. . . . . . . . . . . . . . . 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 1463	. . . . . . . . . . . . . . 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 583	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
401		elun1 4182	. . . . . . . . . . . . . 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 28002	. . . . . . . . . . . 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 28000	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +_s 𝑚) = (𝑚 +_s 𝑋))
407	389, 391	addscomd 28000	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +_s 𝑠) = (𝑠 +_s 𝑋))
408	405, 406, 407	3brtr4d 5175	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +_s 𝑚) <s (𝑋 +_s 𝑠))
409		breq12 5148	. . . . . . . . 9 ⊢ ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑋 +_s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑋 +_s 𝑚) <s (𝑋 +_s 𝑠)))
410	408, 409	syl5ibrcom 247	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
411	410	rexlimdvva 3213	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
412	382, 411	biimtrrid 243	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
413	381, 412	jaod 860	. . . . 5 ⊢ (𝜑 → (((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠))) → 𝑎 <s 𝑏))
414	294, 413	jaod 860	. . . 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 1117	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)})) → 𝑎 <s 𝑏)
417	7, 14, 92, 159, 416	ssltd 27836	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 848 = wceq 1540 ∈ wcel 2108 {cab 2714 ∀wral 3061 ∃wrex 3070 {crab 3436 Vcvv 3480 ∪ cun 3949 ⊆ wss 3951 ∅c0 4333 class class class wbr 5143 Oncon0 6384 ‘cfv 6561 (class class class)co 7431 +no cnadd 8703 No csur 27684 <s cslt 27685 bday cbday 27686 <<s csslt 27825 0_s c0s 27867 O cold 27882 L cleft 27884 R cright 27885 +_s cadds 27992

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2708 ax-rep 5279 ax-sep 5296 ax-nul 5306 ax-pow 5365 ax-pr 5432 ax-un 7755

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3or 1088 df-3an 1089 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2540 df-eu 2569 df-clab 2715 df-cleq 2729 df-clel 2816 df-nfc 2892 df-ne 2941 df-ral 3062 df-rex 3071 df-rmo 3380 df-reu 3381 df-rab 3437 df-v 3482 df-sbc 3789 df-csb 3900 df-dif 3954 df-un 3956 df-in 3958 df-ss 3968 df-pss 3971 df-nul 4334 df-if 4526 df-pw 4602 df-sn 4627 df-pr 4629 df-tp 4631 df-op 4633 df-uni 4908 df-int 4947 df-iun 4993 df-br 5144 df-opab 5206 df-mpt 5226 df-tr 5260 df-id 5578 df-eprel 5584 df-po 5592 df-so 5593 df-fr 5637 df-se 5638 df-we 5639 df-xp 5691 df-rel 5692 df-cnv 5693 df-co 5694 df-dm 5695 df-rn 5696 df-res 5697 df-ima 5698 df-pred 6321 df-ord 6387 df-on 6388 df-suc 6390 df-iota 6514 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7388 df-ov 7434 df-oprab 7435 df-mpo 7436 df-1st 8014 df-2nd 8015 df-frecs 8306 df-wrecs 8337 df-recs 8411 df-1o 8506 df-2o 8507 df-nadd 8704 df-no 27687 df-slt 27688 df-bday 27689 df-sslt 27826 df-scut 27828 df-0s 27869 df-made 27886 df-old 27887 df-left 27889 df-right 27890 df-norec2 27982 df-adds 27993

This theorem is referenced by: addsproplem3 28004

W3C validator