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 27979

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 394 ∨ wo 845 = wceq 1534 ∈ wcel 2099 {cab 2703 ∀wral 3051 ∃wrex 3060 {crab 3420 Vcvv 3463 ∪ cun 3945 ⊆ wss 3947 ∅c0 4323 class class class wbr 5144 Oncon0 6366 ‘cfv 6544 (class class class)co 7414 +no cnadd 8685 No csur 27664 <s cslt 27665 bday cbday 27666 <<s csslt 27805 0_s c0s 27847 O cold 27862 L cleft 27864 R cright 27865 +_s cadds 27968

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-10 2130 ax-11 2147 ax-12 2167 ax-ext 2697 ax-rep 5281 ax-sep 5295 ax-nul 5302 ax-pow 5360 ax-pr 5424 ax-un 7736

This theorem depends on definitions: df-bi 206 df-an 395 df-or 846 df-3or 1085 df-3an 1086 df-tru 1537 df-fal 1547 df-ex 1775 df-nf 1779 df-sb 2061 df-mo 2529 df-eu 2558 df-clab 2704 df-cleq 2718 df-clel 2803 df-nfc 2878 df-ne 2931 df-ral 3052 df-rex 3061 df-rmo 3365 df-reu 3366 df-rab 3421 df-v 3465 df-sbc 3777 df-csb 3893 df-dif 3950 df-un 3952 df-in 3954 df-ss 3964 df-pss 3967 df-nul 4324 df-if 4525 df-pw 4600 df-sn 4625 df-pr 4627 df-tp 4629 df-op 4631 df-uni 4907 df-int 4948 df-iun 4996 df-br 5145 df-opab 5207 df-mpt 5228 df-tr 5262 df-id 5571 df-eprel 5577 df-po 5585 df-so 5586 df-fr 5628 df-se 5629 df-we 5630 df-xp 5679 df-rel 5680 df-cnv 5681 df-co 5682 df-dm 5683 df-rn 5684 df-res 5685 df-ima 5686 df-pred 6303 df-ord 6369 df-on 6370 df-suc 6372 df-iota 6496 df-fun 6546 df-fn 6547 df-f 6548 df-f1 6549 df-fo 6550 df-f1o 6551 df-fv 6552 df-riota 7370 df-ov 7417 df-oprab 7418 df-mpo 7419 df-1st 7993 df-2nd 7994 df-frecs 8286 df-wrecs 8317 df-recs 8391 df-1o 8486 df-2o 8487 df-nadd 8686 df-no 27667 df-slt 27668 df-bday 27669 df-sslt 27806 df-scut 27808 df-0s 27849 df-made 27866 df-old 27867 df-left 27869 df-right 27870 df-norec2 27958 df-adds 27969

This theorem is referenced by: addsproplem3 27980

W3C validator