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 28389

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

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∨ wo 861 = wceq 1570 ∈ wcel 2147 {cab 2741 ∀wral 3080 ∃wrex 3090 {crab 3416 Vcvv 3454 ⊆ wss 3900 ∪ cun 4152 ∅c0 4281 class class class wbr 5106 Oncon0 6383 ‘cfv 6561 (class class class)co 7446 +no cnadd 8705 Nocsur 28030 <s clts 28031 bdaycbday 28032 <<s cslts 28176 0_s c0s 28224 Ocold 28242 Lcleft 28244 Rcright 28245 +_s cadds 28378

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5236 ax-sep 5253 ax-nul 5264 ax-pow 5332 ax-pr 5396 ax-un 7778

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-uni 4871 df-int 4911 df-iun 4956 df-br 5107 df-opab 5172 df-mpt 5191 df-tr 5217 df-id 5551 df-eprel 5556 df-po 5564 df-so 5565 df-fr 5609 df-se 5610 df-we 5611 df-xp 5662 df-rel 5663 df-cnv 5664 df-co 5665 df-dm 5666 df-rn 5667 df-res 5668 df-ima 5669 df-pred 6325 df-ord 6386 df-on 6387 df-suc 6389 df-iota 6515 df-fun 6563 df-fn 6564 df-f 6565 df-f1 6566 df-fo 6567 df-f1o 6568 df-fv 6569 df-riota 7403 df-ov 7449 df-oprab 7450 df-mpo 7451 df-1st 8028 df-2nd 8029 df-frecs 8330 df-wrecs 8361 df-recs 8410 df-1o 8507 df-2o 8508 df-nadd 8706 df-no 28033 df-lts 28034 df-bday 28035 df-slts 28177 df-cuts 28179 df-0s 28226 df-made 28246 df-old 28247 df-left 28249 df-right 28250 df-norec2 28368 df-adds 28379

This theorem is used by: addsproplem3 28390

W3C validator