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 28362

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 6899	. . . . 5 ⊢ (L‘𝑋) ∈ V
2	1	abrexex 7975	. . . 4 ⊢ {𝑝 ∣ ∃𝑙 ∈ (L‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∈ V
3	2	a1i 11	. . 3 ⊢ (𝜑 → {𝑝 ∣ ∃𝑙 ∈ (L‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∈ V)
4		fvex 6899	. . . . 5 ⊢ (L‘𝑌) ∈ V
5	4	abrexex 7975	. . . 4 ⊢ {𝑞 ∣ ∃𝑚 ∈ (L‘𝑌)𝑞 = (𝑋 +_s 𝑚)} ∈ V
6	5	a1i 11	. . 3 ⊢ (𝜑 → {𝑞 ∣ ∃𝑚 ∈ (L‘𝑌)𝑞 = (𝑋 +_s 𝑚)} ∈ V)
7	3, 6	unexd 7769	. 2 ⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ (L‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ (L‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ∈ V)
8		fvex 6899	. . . . 5 ⊢ (R‘𝑋) ∈ V
9	8	abrexex 7975	. . . 4 ⊢ {𝑤 ∣ ∃𝑟 ∈ (R‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∈ V
10	9	a1i 11	. . 3 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ (R‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∈ V)
11		fvex 6899	. . . . 5 ⊢ (R‘𝑌) ∈ V
12	11	abrexex 7975	. . . 4 ⊢ {𝑡 ∣ ∃𝑠 ∈ (R‘𝑌)𝑡 = (𝑋 +_s 𝑠)} ∈ V
13	12	a1i 11	. . 3 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ (R‘𝑌)𝑡 = (𝑋 +_s 𝑠)} ∈ V)
14	10, 13	unexd 7769	. 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 28269	. . . . . . . . 9 ⊢ (𝑙 ∈ (L‘𝑋) → 𝑙 ∈ No)
18	17	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ (L‘𝑋)) → 𝑙 ∈ No)
19		addsproplem2.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ No)
20	19	adantr 486	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ (L‘𝑋)) → 𝑌 ∈ No)
21		0no 28201	. . . . . . . . 9 ⊢ 0_s ∈ No
22	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ (L‘𝑋)) → 0_s ∈ No)
23		bday0 28203	. . . . . . . . . . . . 13 ⊢ (bday‘ 0_s ) = ∅
24	23	oveq2i 7432	. . . . . . . . . . . 12 ⊢ ((bday‘𝑙) +no (bday‘ 0_s )) = ((bday‘𝑙) +no ∅)
25		bdayon 28144	. . . . . . . . . . . . 13 ⊢ (bday‘𝑙) ∈ On
26		naddrid 8697	. . . . . . . . . . . . 13 ⊢ ((bday‘𝑙) ∈ On → ((bday‘𝑙) +no ∅) = (bday‘𝑙))
27	25, 26	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((bday‘𝑙) +no ∅) = (bday‘𝑙)
28	24, 27	eqtri 2783	. . . . . . . . . . 11 ⊢ ((bday‘𝑙) +no (bday‘ 0_s )) = (bday‘𝑙)
29	28	uneq2i 4164	. . . . . . . . . 10 ⊢ (((bday‘𝑙) +no (bday‘𝑌)) ∪ ((bday‘𝑙) +no (bday‘ 0_s ))) = (((bday‘𝑙) +no (bday‘𝑌)) ∪ (bday‘𝑙))
30		bdayon 28144	. . . . . . . . . . . 12 ⊢ (bday‘𝑌) ∈ On
31		naddword1 8705	. . . . . . . . . . . 12 ⊢ (((bday‘𝑙) ∈ On ∧ (bday‘𝑌) ∈ On) → (bday‘𝑙) ⊆ ((bday‘𝑙) +no (bday‘𝑌)))
32	25, 30, 31	mp2an 705	. . . . . . . . . . 11 ⊢ (bday‘𝑙) ⊆ ((bday‘𝑙) +no (bday‘𝑌))
33		ssequn2 4187	. . . . . . . . . . 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 2783	. . . . . . . . 9 ⊢ (((bday‘𝑙) +no (bday‘𝑌)) ∪ ((bday‘𝑙) +no (bday‘ 0_s ))) = ((bday‘𝑙) +no (bday‘𝑌))
36		leftold 28267	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ (L‘𝑋) → 𝑙 ∈ (O‘(bday‘𝑋)))
37		bdayon 28144	. . . . . . . . . . . . . 14 ⊢ (bday‘𝑋) ∈ On
38		oldbday 28293	. . . . . . . . . . . . . 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 8701	. . . . . . . . . . . . 13 ⊢ (((bday‘𝑙) ∈ On ∧ (bday‘𝑋) ∈ On ∧ (bday‘𝑌) ∈ On) → ((bday‘𝑙) ∈ (bday‘𝑋) ↔ ((bday‘𝑙) +no (bday‘𝑌)) ∈ ((bday‘𝑋) +no (bday‘𝑌))))
42	25, 37, 30, 41	mp3an 1490	. . . . . . . . . . . 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 4180	. . . . . . . . . 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 2864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ (L‘𝑋)) → (((bday‘𝑙) +no (bday‘𝑌)) ∪ ((bday‘𝑙) +no (bday‘ 0_s ))) ∈ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((bday‘𝑋) +no (bday‘𝑍))))
48	16, 18, 20, 22, 47	addsproplem1 28361	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ (L‘𝑋)) → ((𝑙 +_s 𝑌) ∈ No ∧ (𝑌 <s 0_s → (𝑌 +_s 𝑙) <s ( 0_s +_s 𝑙))))
49	48	simpld 500	. . . . . 6 ⊢ ((𝜑 ∧ 𝑙 ∈ (L‘𝑋)) → (𝑙 +_s 𝑌) ∈ No)
50		eleq1a 2855	. . . . . 6 ⊢ ((𝑙 +_s 𝑌) ∈ No → (𝑝 = (𝑙 +_s 𝑌) → 𝑝 ∈ No))
51	49, 50	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑙 ∈ (L‘𝑋)) → (𝑝 = (𝑙 +_s 𝑌) → 𝑝 ∈ No))
52	51	rexlimdva 3163	. . . 4 ⊢ (𝜑 → (∃𝑙 ∈ (L‘𝑋)𝑝 = (𝑙 +_s 𝑌) → 𝑝 ∈ No))
53	52	abssdv 3992	. . 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 28269	. . . . . . . . 9 ⊢ (𝑚 ∈ (L‘𝑌) → 𝑚 ∈ No)
58	57	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (L‘𝑌)) → 𝑚 ∈ No)
59	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (L‘𝑌)) → 0_s ∈ No)
60	23	oveq2i 7432	. . . . . . . . . . . 12 ⊢ ((bday‘𝑋) +no (bday‘ 0_s )) = ((bday‘𝑋) +no ∅)
61		naddrid 8697	. . . . . . . . . . . . 13 ⊢ ((bday‘𝑋) ∈ On → ((bday‘𝑋) +no ∅) = (bday‘𝑋))
62	37, 61	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((bday‘𝑋) +no ∅) = (bday‘𝑋)
63	60, 62	eqtri 2783	. . . . . . . . . . 11 ⊢ ((bday‘𝑋) +no (bday‘ 0_s )) = (bday‘𝑋)
64	63	uneq2i 4164	. . . . . . . . . 10 ⊢ (((bday‘𝑋) +no (bday‘𝑚)) ∪ ((bday‘𝑋) +no (bday‘ 0_s ))) = (((bday‘𝑋) +no (bday‘𝑚)) ∪ (bday‘𝑋))
65		bdayon 28144	. . . . . . . . . . . 12 ⊢ (bday‘𝑚) ∈ On
66		naddword1 8705	. . . . . . . . . . . 12 ⊢ (((bday‘𝑋) ∈ On ∧ (bday‘𝑚) ∈ On) → (bday‘𝑋) ⊆ ((bday‘𝑋) +no (bday‘𝑚)))
67	37, 65, 66	mp2an 705	. . . . . . . . . . 11 ⊢ (bday‘𝑋) ⊆ ((bday‘𝑋) +no (bday‘𝑚))
68		ssequn2 4187	. . . . . . . . . . 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 2783	. . . . . . . . 9 ⊢ (((bday‘𝑋) +no (bday‘𝑚)) ∪ ((bday‘𝑋) +no (bday‘ 0_s ))) = ((bday‘𝑋) +no (bday‘𝑚))
71		leftold 28267	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ (L‘𝑌) → 𝑚 ∈ (O‘(bday‘𝑌)))
72		oldbday 28293	. . . . . . . . . . . . . 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 8702	. . . . . . . . . . . . 13 ⊢ (((bday‘𝑚) ∈ On ∧ (bday‘𝑌) ∈ On ∧ (bday‘𝑋) ∈ On) → ((bday‘𝑚) ∈ (bday‘𝑌) ↔ ((bday‘𝑋) +no (bday‘𝑚)) ∈ ((bday‘𝑋) +no (bday‘𝑌))))
76	65, 30, 37, 75	mp3an 1490	. . . . . . . . . . . 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 4180	. . . . . . . . . 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 2864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ (L‘𝑌)) → (((bday‘𝑋) +no (bday‘𝑚)) ∪ ((bday‘𝑋) +no (bday‘ 0_s ))) ∈ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((bday‘𝑋) +no (bday‘𝑍))))
82	54, 56, 58, 59, 81	addsproplem1 28361	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ (L‘𝑌)) → ((𝑋 +_s 𝑚) ∈ No ∧ (𝑚 <s 0_s → (𝑚 +_s 𝑋) <s ( 0_s +_s 𝑋))))
83	82	simpld 500	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ (L‘𝑌)) → (𝑋 +_s 𝑚) ∈ No)
84		eleq1a 2855	. . . . . 6 ⊢ ((𝑋 +_s 𝑚) ∈ No → (𝑞 = (𝑋 +_s 𝑚) → 𝑞 ∈ No))
85	83, 84	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ (L‘𝑌)) → (𝑞 = (𝑋 +_s 𝑚) → 𝑞 ∈ No))
86	85	rexlimdva 3163	. . . 4 ⊢ (𝜑 → (∃𝑚 ∈ (L‘𝑌)𝑞 = (𝑋 +_s 𝑚) → 𝑞 ∈ No))
87	86	abssdv 3992	. . 3 ⊢ (𝜑 → {𝑞 ∣ ∃𝑚 ∈ (L‘𝑌)𝑞 = (𝑋 +_s 𝑚)} ⊆ No)
88	53, 87	unssd 4190	. 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 28270	. . . . . . . . 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 7432	. . . . . . . . . . . 12 ⊢ ((bday‘𝑟) +no (bday‘ 0_s )) = ((bday‘𝑟) +no ∅)
95		bdayon 28144	. . . . . . . . . . . . 13 ⊢ (bday‘𝑟) ∈ On
96		naddrid 8697	. . . . . . . . . . . . 13 ⊢ ((bday‘𝑟) ∈ On → ((bday‘𝑟) +no ∅) = (bday‘𝑟))
97	95, 96	ax-mp 5	. . . . . . . . . . . 12 ⊢ ((bday‘𝑟) +no ∅) = (bday‘𝑟)
98	94, 97	eqtri 2783	. . . . . . . . . . 11 ⊢ ((bday‘𝑟) +no (bday‘ 0_s )) = (bday‘𝑟)
99	98	uneq2i 4164	. . . . . . . . . 10 ⊢ (((bday‘𝑟) +no (bday‘𝑌)) ∪ ((bday‘𝑟) +no (bday‘ 0_s ))) = (((bday‘𝑟) +no (bday‘𝑌)) ∪ (bday‘𝑟))
100		naddword1 8705	. . . . . . . . . . . 12 ⊢ (((bday‘𝑟) ∈ On ∧ (bday‘𝑌) ∈ On) → (bday‘𝑟) ⊆ ((bday‘𝑟) +no (bday‘𝑌)))
101	95, 30, 100	mp2an 705	. . . . . . . . . . 11 ⊢ (bday‘𝑟) ⊆ ((bday‘𝑟) +no (bday‘𝑌))
102		ssequn2 4187	. . . . . . . . . . 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 2783	. . . . . . . . 9 ⊢ (((bday‘𝑟) +no (bday‘𝑌)) ∪ ((bday‘𝑟) +no (bday‘ 0_s ))) = ((bday‘𝑟) +no (bday‘𝑌))
105		rightold 28268	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ (R‘𝑋) → 𝑟 ∈ (O‘(bday‘𝑋)))
106		oldbday 28293	. . . . . . . . . . . . . 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 8701	. . . . . . . . . . . . 13 ⊢ (((bday‘𝑟) ∈ On ∧ (bday‘𝑋) ∈ On ∧ (bday‘𝑌) ∈ On) → ((bday‘𝑟) ∈ (bday‘𝑋) ↔ ((bday‘𝑟) +no (bday‘𝑌)) ∈ ((bday‘𝑋) +no (bday‘𝑌))))
110	95, 37, 30, 109	mp3an 1490	. . . . . . . . . . . 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 4180	. . . . . . . . . 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 2864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ (R‘𝑋)) → (((bday‘𝑟) +no (bday‘𝑌)) ∪ ((bday‘𝑟) +no (bday‘ 0_s ))) ∈ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((bday‘𝑋) +no (bday‘𝑍))))
116	89, 91, 92, 93, 115	addsproplem1 28361	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ (R‘𝑋)) → ((𝑟 +_s 𝑌) ∈ No ∧ (𝑌 <s 0_s → (𝑌 +_s 𝑟) <s ( 0_s +_s 𝑟))))
117	116	simpld 500	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ (R‘𝑋)) → (𝑟 +_s 𝑌) ∈ No)
118		eleq1a 2855	. . . . . 6 ⊢ ((𝑟 +_s 𝑌) ∈ No → (𝑤 = (𝑟 +_s 𝑌) → 𝑤 ∈ No))
119	117, 118	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ (R‘𝑋)) → (𝑤 = (𝑟 +_s 𝑌) → 𝑤 ∈ No))
120	119	rexlimdva 3163	. . . 4 ⊢ (𝜑 → (∃𝑟 ∈ (R‘𝑋)𝑤 = (𝑟 +_s 𝑌) → 𝑤 ∈ No))
121	120	abssdv 3992	. . 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 28270	. . . . . . . . 9 ⊢ (𝑠 ∈ (R‘𝑌) → 𝑠 ∈ No)
125	124	adantl 487	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (R‘𝑌)) → 𝑠 ∈ No)
126	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (R‘𝑌)) → 0_s ∈ No)
127	63	uneq2i 4164	. . . . . . . . . 10 ⊢ (((bday‘𝑋) +no (bday‘𝑠)) ∪ ((bday‘𝑋) +no (bday‘ 0_s ))) = (((bday‘𝑋) +no (bday‘𝑠)) ∪ (bday‘𝑋))
128		bdayon 28144	. . . . . . . . . . . 12 ⊢ (bday‘𝑠) ∈ On
129		naddword1 8705	. . . . . . . . . . . 12 ⊢ (((bday‘𝑋) ∈ On ∧ (bday‘𝑠) ∈ On) → (bday‘𝑋) ⊆ ((bday‘𝑋) +no (bday‘𝑠)))
130	37, 128, 129	mp2an 705	. . . . . . . . . . 11 ⊢ (bday‘𝑋) ⊆ ((bday‘𝑋) +no (bday‘𝑠))
131		ssequn2 4187	. . . . . . . . . . 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 2783	. . . . . . . . 9 ⊢ (((bday‘𝑋) +no (bday‘𝑠)) ∪ ((bday‘𝑋) +no (bday‘ 0_s ))) = ((bday‘𝑋) +no (bday‘𝑠))
134		rightold 28268	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ (R‘𝑌) → 𝑠 ∈ (O‘(bday‘𝑌)))
135		oldbday 28293	. . . . . . . . . . . . . 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 8702	. . . . . . . . . . . . 13 ⊢ (((bday‘𝑠) ∈ On ∧ (bday‘𝑌) ∈ On ∧ (bday‘𝑋) ∈ On) → ((bday‘𝑠) ∈ (bday‘𝑌) ↔ ((bday‘𝑋) +no (bday‘𝑠)) ∈ ((bday‘𝑋) +no (bday‘𝑌))))
139	128, 30, 37, 138	mp3an 1490	. . . . . . . . . . . 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 4180	. . . . . . . . . 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 2864	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ (R‘𝑌)) → (((bday‘𝑋) +no (bday‘𝑠)) ∪ ((bday‘𝑋) +no (bday‘ 0_s ))) ∈ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((bday‘𝑋) +no (bday‘𝑍))))
145	122, 123, 125, 126, 144	addsproplem1 28361	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ (R‘𝑌)) → ((𝑋 +_s 𝑠) ∈ No ∧ (𝑠 <s 0_s → (𝑠 +_s 𝑋) <s ( 0_s +_s 𝑋))))
146	145	simpld 500	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ (R‘𝑌)) → (𝑋 +_s 𝑠) ∈ No)
147		eleq1a 2855	. . . . . 6 ⊢ ((𝑋 +_s 𝑠) ∈ No → (𝑡 = (𝑋 +_s 𝑠) → 𝑡 ∈ No))
148	146, 147	syl 18	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ (R‘𝑌)) → (𝑡 = (𝑋 +_s 𝑠) → 𝑡 ∈ No))
149	148	rexlimdva 3163	. . . 4 ⊢ (𝜑 → (∃𝑠 ∈ (R‘𝑌)𝑡 = (𝑋 +_s 𝑠) → 𝑡 ∈ No))
150	149	abssdv 3992	. . 3 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ (R‘𝑌)𝑡 = (𝑋 +_s 𝑠)} ⊆ No)
151	121, 150	unssd 4190	. 2 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ (R‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ (R‘𝑌)𝑡 = (𝑋 +_s 𝑠)}) ⊆ No)
152		elun 4152	. . . . . . 7 ⊢ (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ (L‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ (L‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ↔ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ (L‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ (L‘𝑌)𝑞 = (𝑋 +_s 𝑚)}))
153		vex 3454	. . . . . . . . 9 ⊢ 𝑎 ∈ V
154		eqeq1 2764	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → (𝑝 = (𝑙 +_s 𝑌) ↔ 𝑎 = (𝑙 +_s 𝑌)))
155	154	rexbidv 3186	. . . . . . . . 9 ⊢ (𝑝 = 𝑎 → (∃𝑙 ∈ (L‘𝑋)𝑝 = (𝑙 +_s 𝑌) ↔ ∃𝑙 ∈ (L‘𝑋)𝑎 = (𝑙 +_s 𝑌)))
156	153, 155	elab 3632	. . . . . . . 8 ⊢ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ (L‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ↔ ∃𝑙 ∈ (L‘𝑋)𝑎 = (𝑙 +_s 𝑌))
157		eqeq1 2764	. . . . . . . . . 10 ⊢ (𝑞 = 𝑎 → (𝑞 = (𝑋 +_s 𝑚) ↔ 𝑎 = (𝑋 +_s 𝑚)))
158	157	rexbidv 3186	. . . . . . . . 9 ⊢ (𝑞 = 𝑎 → (∃𝑚 ∈ (L‘𝑌)𝑞 = (𝑋 +_s 𝑚) ↔ ∃𝑚 ∈ (L‘𝑌)𝑎 = (𝑋 +_s 𝑚)))
159	153, 158	elab 3632	. . . . . . . 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 4152	. . . . . . 7 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ (R‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ (R‘𝑌)𝑡 = (𝑋 +_s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ (R‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ (R‘𝑌)𝑡 = (𝑋 +_s 𝑠)}))
163		vex 3454	. . . . . . . . 9 ⊢ 𝑏 ∈ V
164		eqeq1 2764	. . . . . . . . . 10 ⊢ (𝑤 = 𝑏 → (𝑤 = (𝑟 +_s 𝑌) ↔ 𝑏 = (𝑟 +_s 𝑌)))
165	164	rexbidv 3186	. . . . . . . . 9 ⊢ (𝑤 = 𝑏 → (∃𝑟 ∈ (R‘𝑋)𝑤 = (𝑟 +_s 𝑌) ↔ ∃𝑟 ∈ (R‘𝑋)𝑏 = (𝑟 +_s 𝑌)))
166	163, 165	elab 3632	. . . . . . . 8 ⊢ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ (R‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ↔ ∃𝑟 ∈ (R‘𝑋)𝑏 = (𝑟 +_s 𝑌))
167		eqeq1 2764	. . . . . . . . . 10 ⊢ (𝑡 = 𝑏 → (𝑡 = (𝑋 +_s 𝑠) ↔ 𝑏 = (𝑋 +_s 𝑠)))
168	167	rexbidv 3186	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → (∃𝑠 ∈ (R‘𝑌)𝑡 = (𝑋 +_s 𝑠) ↔ ∃𝑠 ∈ (R‘𝑌)𝑏 = (𝑋 +_s 𝑠)))
169	163, 168	elab 3632	. . . . . . . 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 3234	. . . . . . 7 ⊢ (∃𝑙 ∈ (L‘𝑋)∃𝑟 ∈ (R‘𝑋)(𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) ↔ (∃𝑙 ∈ (L‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑟 ∈ (R‘𝑋)𝑏 = (𝑟 +_s 𝑌)))
176		lltr 28254	. . . . . . . . . . . 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 28164	. . . . . . . . . 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 8696	. . . . . . . . . . . . . . . 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 2864	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑟 ∈ (R‘𝑋))) → ((bday‘𝑌) +no (bday‘𝑙)) ∈ ((bday‘𝑋) +no (bday‘𝑌)))
189		naddcom 8696	. . . . . . . . . . . . . . . 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 2864	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑟 ∈ (R‘𝑋))) → ((bday‘𝑌) +no (bday‘𝑟)) ∈ ((bday‘𝑋) +no (bday‘𝑌)))
193		naddcl 8690	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑌) ∈ On ∧ (bday‘𝑙) ∈ On) → ((bday‘𝑌) +no (bday‘𝑙)) ∈ On)
194	30, 25, 193	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ ((bday‘𝑌) +no (bday‘𝑙)) ∈ On
195		naddcl 8690	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑌) ∈ On ∧ (bday‘𝑟) ∈ On) → ((bday‘𝑌) +no (bday‘𝑟)) ∈ On)
196	30, 95, 195	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ ((bday‘𝑌) +no (bday‘𝑟)) ∈ On
197		naddcl 8690	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑋) ∈ On ∧ (bday‘𝑌) ∈ On) → ((bday‘𝑋) +no (bday‘𝑌)) ∈ On)
198	37, 30, 197	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ ((bday‘𝑋) +no (bday‘𝑌)) ∈ On
199		onunel 6470	. . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . 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 4180	. . . . . . . . . . . . 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 28361	. . . . . . . . . . 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 5107	. . . . . . . . 9 ⊢ ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑙 +_s 𝑌) <s (𝑟 +_s 𝑌)))
208	206, 207	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑟 ∈ (R‘𝑋))) → ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
209	208	rexlimdvva 3219	. . . . . . 7 ⊢ (𝜑 → (∃𝑙 ∈ (L‘𝑋)∃𝑟 ∈ (R‘𝑋)(𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
210	175, 209	biimtrrid 246	. . . . . 6 ⊢ (𝜑 → ((∃𝑙 ∈ (L‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑟 ∈ (R‘𝑋)𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
211		reeanv 3234	. . . . . . 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 4164	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝑙) +no (bday‘𝑠)) ∪ ((bday‘𝑙) +no (bday‘ 0_s ))) = (((bday‘𝑙) +no (bday‘𝑠)) ∪ (bday‘𝑙))
218		naddword1 8705	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑙) ∈ On ∧ (bday‘𝑠) ∈ On) → (bday‘𝑙) ⊆ ((bday‘𝑙) +no (bday‘𝑠)))
219	25, 128, 218	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (bday‘𝑙) ⊆ ((bday‘𝑙) +no (bday‘𝑠))
220		ssequn2 4187	. . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . 13 ⊢ (((bday‘𝑙) +no (bday‘𝑠)) ∪ ((bday‘𝑙) +no (bday‘ 0_s ))) = ((bday‘𝑙) +no (bday‘𝑠))
223		naddel1 8701	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑙) ∈ On ∧ (bday‘𝑋) ∈ On ∧ (bday‘𝑠) ∈ On) → ((bday‘𝑙) ∈ (bday‘𝑋) ↔ ((bday‘𝑙) +no (bday‘𝑠)) ∈ ((bday‘𝑋) +no (bday‘𝑠))))
224	25, 37, 128, 223	mp3an 1490	. . . . . . . . . . . . . . . . 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 6410	. . . . . . . . . . . . . . . 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 4180	. . . . . . . . . . . . . 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 2864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑠 ∈ (R‘𝑌))) → (((bday‘𝑙) +no (bday‘𝑠)) ∪ ((bday‘𝑙) +no (bday‘ 0_s ))) ∈ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((bday‘𝑋) +no (bday‘𝑍))))
234	213, 214, 215, 216, 233	addsproplem1 28361	. . . . . . . . . . 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 28246	. . . . . . . . . . . . 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 8690	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑙) ∈ On ∧ (bday‘𝑌) ∈ On) → ((bday‘𝑙) +no (bday‘𝑌)) ∈ On)
242	25, 30, 241	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑙) +no (bday‘𝑌)) ∈ On
243		naddcl 8690	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑙) ∈ On ∧ (bday‘𝑠) ∈ On) → ((bday‘𝑙) +no (bday‘𝑠)) ∈ On)
244	25, 128, 243	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑙) +no (bday‘𝑠)) ∈ On
245		onunel 6470	. . . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . . 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 4180	. . . . . . . . . . . . . . 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 28361	. . . . . . . . . . . . 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 28359	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑠 ∈ (R‘𝑌))) → (𝑙 +_s 𝑌) = (𝑌 +_s 𝑙))
254	214, 215	addscomd 28359	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑠 ∈ (R‘𝑌))) → (𝑙 +_s 𝑠) = (𝑠 +_s 𝑙))
255	252, 253, 254	3brtr4d 5136	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑠 ∈ (R‘𝑌))) → (𝑙 +_s 𝑌) <s (𝑙 +_s 𝑠))
256		leftlt 28245	. . . . . . . . . . . 12 ⊢ (𝑙 ∈ (L‘𝑋) → 𝑙 <s 𝑋)
257	256	ad2antrl 741	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑠 ∈ (R‘𝑌))) → 𝑙 <s 𝑋)
258	55	adantr 486	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑠 ∈ (R‘𝑌))) → 𝑋 ∈ No)
259		naddcom 8696	. . . . . . . . . . . . . . . . 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 2864	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑠 ∈ (R‘𝑌))) → ((bday‘𝑠) +no (bday‘𝑙)) ∈ ((bday‘𝑋) +no (bday‘𝑌)))
262		naddcom 8696	. . . . . . . . . . . . . . . . 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 2864	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑠 ∈ (R‘𝑌))) → ((bday‘𝑠) +no (bday‘𝑋)) ∈ ((bday‘𝑋) +no (bday‘𝑌)))
265		naddcl 8690	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑠) ∈ On ∧ (bday‘𝑙) ∈ On) → ((bday‘𝑠) +no (bday‘𝑙)) ∈ On)
266	128, 25, 265	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑠) +no (bday‘𝑙)) ∈ On
267		naddcl 8690	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑠) ∈ On ∧ (bday‘𝑋) ∈ On) → ((bday‘𝑠) +no (bday‘𝑋)) ∈ On)
268	128, 37, 267	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑠) +no (bday‘𝑋)) ∈ On
269		onunel 6470	. . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . 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 4180	. . . . . . . . . . . . . 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 28361	. . . . . . . . . . . 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 28126	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑠 ∈ (R‘𝑌))) → (𝑙 +_s 𝑌) <s (𝑋 +_s 𝑠))
278		breq12 5107	. . . . . . . . 9 ⊢ ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑋 +_s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑙 +_s 𝑌) <s (𝑋 +_s 𝑠)))
279	277, 278	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ (L‘𝑋) ∧ 𝑠 ∈ (R‘𝑌))) → ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
280	279	rexlimdvva 3219	. . . . . . 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 3234	. . . . . . 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 2864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → (((bday‘𝑋) +no (bday‘𝑚)) ∪ ((bday‘𝑋) +no (bday‘ 0_s ))) ∈ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((bday‘𝑋) +no (bday‘𝑍))))
291	284, 285, 286, 287, 290	addsproplem1 28361	. . . . . . . . . . 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 4164	. . . . . . . . . . . . . 14 ⊢ (((bday‘𝑟) +no (bday‘𝑚)) ∪ ((bday‘𝑟) +no (bday‘ 0_s ))) = (((bday‘𝑟) +no (bday‘𝑚)) ∪ (bday‘𝑟))
295		naddword1 8705	. . . . . . . . . . . . . . . 16 ⊢ (((bday‘𝑟) ∈ On ∧ (bday‘𝑚) ∈ On) → (bday‘𝑟) ⊆ ((bday‘𝑟) +no (bday‘𝑚)))
296	95, 65, 295	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (bday‘𝑟) ⊆ ((bday‘𝑟) +no (bday‘𝑚))
297		ssequn2 4187	. . . . . . . . . . . . . . 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 2783	. . . . . . . . . . . . 13 ⊢ (((bday‘𝑟) +no (bday‘𝑚)) ∪ ((bday‘𝑟) +no (bday‘ 0_s ))) = ((bday‘𝑟) +no (bday‘𝑚))
300		naddel1 8701	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑟) ∈ On ∧ (bday‘𝑋) ∈ On ∧ (bday‘𝑚) ∈ On) → ((bday‘𝑟) ∈ (bday‘𝑋) ↔ ((bday‘𝑟) +no (bday‘𝑚)) ∈ ((bday‘𝑋) +no (bday‘𝑚))))
301	95, 37, 65, 300	mp3an 1490	. . . . . . . . . . . . . . . . 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 6410	. . . . . . . . . . . . . . . 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 4180	. . . . . . . . . . . . . 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 2864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → (((bday‘𝑟) +no (bday‘𝑚)) ∪ ((bday‘𝑟) +no (bday‘ 0_s ))) ∈ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((bday‘𝑋) +no (bday‘𝑍))))
310	284, 293, 286, 287, 309	addsproplem1 28361	. . . . . . . . . . 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 2864	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → (((bday‘𝑟) +no (bday‘𝑌)) ∪ ((bday‘𝑟) +no (bday‘ 0_s ))) ∈ (((bday‘𝑋) +no (bday‘𝑌)) ∪ ((bday‘𝑋) +no (bday‘𝑍))))
316	284, 293, 312, 287, 315	addsproplem1 28361	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → ((𝑟 +_s 𝑌) ∈ No ∧ (𝑌 <s 0_s → (𝑌 +_s 𝑟) <s ( 0_s +_s 𝑟))))
317	316	simpld 500	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → (𝑟 +_s 𝑌) ∈ No)
318		rightval 28242	. . . . . . . . . . . . . . . 16 ⊢ (R‘𝑋) = {𝑟 ∈ (O‘(bday‘𝑋)) ∣ 𝑋 <s 𝑟}
319	318	eleq2i 2852	. . . . . . . . . . . . . . 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 3432	. . . . . . . . . . . . 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 8696	. . . . . . . . . . . . . . . . 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 2864	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → ((bday‘𝑚) +no (bday‘𝑋)) ∈ ((bday‘𝑋) +no (bday‘𝑌)))
328		naddcom 8696	. . . . . . . . . . . . . . . . 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 2864	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → ((bday‘𝑚) +no (bday‘𝑟)) ∈ ((bday‘𝑋) +no (bday‘𝑌)))
331		naddcl 8690	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑚) ∈ On ∧ (bday‘𝑋) ∈ On) → ((bday‘𝑚) +no (bday‘𝑋)) ∈ On)
332	65, 37, 331	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑚) +no (bday‘𝑋)) ∈ On
333		naddcl 8690	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑚) ∈ On ∧ (bday‘𝑟) ∈ On) → ((bday‘𝑚) +no (bday‘𝑟)) ∈ On)
334	65, 95, 333	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑚) +no (bday‘𝑟)) ∈ On
335		onunel 6470	. . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . 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 4180	. . . . . . . . . . . . . 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 28361	. . . . . . . . . . . 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 28241	. . . . . . . . . . . . . . . . 17 ⊢ (L‘𝑌) = {𝑚 ∈ (O‘(bday‘𝑌)) ∣ 𝑚 <s 𝑌}
344	343	eleq2i 2852	. . . . . . . . . . . . . . . 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 3432	. . . . . . . . . . . . . 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 8690	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑟) ∈ On ∧ (bday‘𝑚) ∈ On) → ((bday‘𝑟) +no (bday‘𝑚)) ∈ On)
351	95, 65, 350	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑟) +no (bday‘𝑚)) ∈ On
352		naddcl 8690	. . . . . . . . . . . . . . . . . 18 ⊢ (((bday‘𝑟) ∈ On ∧ (bday‘𝑌) ∈ On) → ((bday‘𝑟) +no (bday‘𝑌)) ∈ On)
353	95, 30, 352	mp2an 705	. . . . . . . . . . . . . . . . 17 ⊢ ((bday‘𝑟) +no (bday‘𝑌)) ∈ On
354		onunel 6470	. . . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . . 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 4180	. . . . . . . . . . . . . . 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 28361	. . . . . . . . . . . . 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 28359	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → (𝑟 +_s 𝑚) = (𝑚 +_s 𝑟))
363	293, 312	addscomd 28359	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → (𝑟 +_s 𝑌) = (𝑌 +_s 𝑟))
364	361, 362, 363	3brtr4d 5136	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → (𝑟 +_s 𝑚) <s (𝑟 +_s 𝑌))
365	292, 311, 317, 342, 364	ltstrd 28126	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → (𝑋 +_s 𝑚) <s (𝑟 +_s 𝑌))
366		breq12 5107	. . . . . . . . 9 ⊢ ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑟 +_s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑋 +_s 𝑚) <s (𝑟 +_s 𝑌)))
367	365, 366	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑟 ∈ (R‘𝑋))) → ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
368	367	rexlimdvva 3219	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ (L‘𝑌)∃𝑟 ∈ (R‘𝑋)(𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
369	283, 368	biimtrrid 246	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ (L‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑟 ∈ (R‘𝑋)𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
370		reeanv 3234	. . . . . . 7 ⊢ (∃𝑚 ∈ (L‘𝑌)∃𝑠 ∈ (R‘𝑌)(𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑋 +_s 𝑠)) ↔ (∃𝑚 ∈ (L‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑠 ∈ (R‘𝑌)𝑏 = (𝑋 +_s 𝑠)))
371		lltr 28254	. . . . . . . . . . . . 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 28164	. . . . . . . . . . 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 8690	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑋) ∈ On ∧ (bday‘𝑚) ∈ On) → ((bday‘𝑋) +no (bday‘𝑚)) ∈ On)
383	37, 65, 382	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑋) +no (bday‘𝑚)) ∈ On
384		naddcl 8690	. . . . . . . . . . . . . . . . 17 ⊢ (((bday‘𝑋) ∈ On ∧ (bday‘𝑠) ∈ On) → ((bday‘𝑋) +no (bday‘𝑠)) ∈ On)
385	37, 128, 384	mp2an 705	. . . . . . . . . . . . . . . 16 ⊢ ((bday‘𝑋) +no (bday‘𝑠)) ∈ On
386		onunel 6470	. . . . . . . . . . . . . . . 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 1490	. . . . . . . . . . . . . . 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 4180	. . . . . . . . . . . . . 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 28361	. . . . . . . . . . . 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 28359	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑠 ∈ (R‘𝑌))) → (𝑋 +_s 𝑚) = (𝑚 +_s 𝑋))
395	377, 379	addscomd 28359	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑠 ∈ (R‘𝑌))) → (𝑋 +_s 𝑠) = (𝑠 +_s 𝑋))
396	393, 394, 395	3brtr4d 5136	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑠 ∈ (R‘𝑌))) → (𝑋 +_s 𝑚) <s (𝑋 +_s 𝑠))
397		breq12 5107	. . . . . . . . 9 ⊢ ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑋 +_s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑋 +_s 𝑚) <s (𝑋 +_s 𝑠)))
398	396, 397	syl5ibrcom 250	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ (L‘𝑌) ∧ 𝑠 ∈ (R‘𝑌))) → ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
399	398	rexlimdvva 3219	. . . . . . 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 28160	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 1569 ∈ wcel 2144 {cab 2738 ∀wral 3076 ∃wrex 3086 {crab 3412 Vcvv 3450 ⊆ wss 3895 ∪ cun 4149 ∅c0 4278 class class class wbr 5102 Oncon0 6362 ‘cfv 6539 (class class class)co 7421 +no cnadd 8678 Nocsur 28003 <s clts 28004 bdaycbday 28005 <<s cslts 28149 0_s c0s 28197 Ocold 28215 Lcleft 28217 Rcright 28218 +_s cadds 28351

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1827 ax-4 1841 ax-5 1942 ax-6 1999 ax-7 2040 ax-8 2146 ax-9 2154 ax-10 2177 ax-11 2193 ax-12 2212 ax-ext 2732 ax-rep 5231 ax-sep 5248 ax-nul 5259 ax-pow 5326 ax-pr 5390 ax-un 7752

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1572 df-fal 1582 df-ex 1812 df-nf 1816 df-sb 2099 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3739 df-csb 3847 df-ss 3896 df-pss 4014 df-dif 4047 df-in 4091 df-un 4151 df-nul 4279 df-if 4482 df-pw 4558 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4835 df-uni 4867 df-int 4907 df-iun 4952 df-br 5103 df-opab 5167 df-mpt 5186 df-tr 5212 df-id 5545 df-eprel 5550 df-po 5558 df-so 5559 df-fr 5603 df-se 5604 df-we 5605 df-xp 5656 df-rel 5657 df-cnv 5658 df-co 5659 df-dm 5660 df-rn 5661 df-res 5662 df-ima 5663 df-pred 6304 df-ord 6365 df-on 6366 df-suc 6368 df-iota 6494 df-fun 6541 df-fn 6542 df-f 6543 df-f1 6544 df-fo 6545 df-f1o 6546 df-fv 6547 df-riota 7378 df-ov 7424 df-oprab 7425 df-mpo 7426 df-1st 8002 df-2nd 8003 df-frecs 8303 df-wrecs 8334 df-recs 8383 df-1o 8480 df-2o 8481 df-nadd 8679 df-no 28006 df-lts 28007 df-bday 28008 df-slts 28150 df-cuts 28152 df-0s 28199 df-made 28219 df-old 28220 df-left 28222 df-right 28223 df-norec2 28341 df-adds 28352

This theorem is used by: addsproplem3 28363

W3C validator