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 27987

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 6847	. . . . 5 ⊢ ( L ‘𝑋) ∈ V
2	1	abrexex 7911	. . . 4 ⊢ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∈ V
3	2	a1i 11	. . 3 ⊢ (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∈ V)
4		fvex 6847	. . . . 5 ⊢ ( L ‘𝑌) ∈ V
5	4	abrexex 7911	. . . 4 ⊢ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)} ∈ V
6	5	a1i 11	. . 3 ⊢ (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)} ∈ V)
7	3, 6	unexd 7704	. 2 ⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ∈ V)
8		fvex 6847	. . . . 5 ⊢ ( R ‘𝑋) ∈ V
9	8	abrexex 7911	. . . 4 ⊢ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∈ V
10	9	a1i 11	. . 3 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∈ V)
11		fvex 6847	. . . . 5 ⊢ ( R ‘𝑌) ∈ V
12	11	abrexex 7911	. . . 4 ⊢ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)} ∈ V
13	12	a1i 11	. . 3 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)} ∈ V)
14	10, 13	unexd 7704	. 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 481	. . . . . . . 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 27894	. . . . . . . . 9 ⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ No )
18	17	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 𝑙 ∈ No )
19		addsproplem2.3	. . . . . . . . 9 ⊢ (𝜑 → 𝑌 ∈ No )
20	19	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 𝑌 ∈ No )
21		0no 27826	. . . . . . . . 9 ⊢ 0_s ∈ No
22	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 0_s ∈ No )
23		bday0 27828	. . . . . . . . . . . . 13 ⊢ ( bday ‘ 0_s ) = ∅
24	23	oveq2i 7374	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑙) +no ( bday ‘ 0_s )) = (( bday ‘𝑙) +no ∅)
25		bdayon 27769	. . . . . . . . . . . . 13 ⊢ ( bday ‘𝑙) ∈ On
26		naddrid 8616	. . . . . . . . . . . . 13 ⊢ (( bday ‘𝑙) ∈ On → (( bday ‘𝑙) +no ∅) = ( bday ‘𝑙))
27	25, 26	ax-mp 5	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑙) +no ∅) = ( bday ‘𝑙)
28	24, 27	eqtri 2763	. . . . . . . . . . 11 ⊢ (( bday ‘𝑙) +no ( bday ‘ 0_s )) = ( bday ‘𝑙)
29	28	uneq2i 4102	. . . . . . . . . 10 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑙))
30		bdayon 27769	. . . . . . . . . . . 12 ⊢ ( bday ‘𝑌) ∈ On
31		naddword1 8624	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑌) ∈ On) → ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑌)))
32	25, 30, 31	mp2an 698	. . . . . . . . . . 11 ⊢ ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑌))
33		ssequn2 4125	. . . . . . . . . . 11 ⊢ (( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑌)))
34	32, 33	mpbi 231	. . . . . . . . . 10 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑌))
35	29, 34	eqtri 2763	. . . . . . . . 9 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) = (( bday ‘𝑙) +no ( bday ‘𝑌))
36		leftold 27892	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ ( O ‘( bday ‘𝑋)))
37		bdayon 27769	. . . . . . . . . . . . . 14 ⊢ ( bday ‘𝑋) ∈ On
38		oldbday 27918	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑙 ∈ No ) → (𝑙 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑙) ∈ ( bday ‘𝑋)))
39	37, 17, 38	sylancr 593	. . . . . . . . . . . . 13 ⊢ (𝑙 ∈ ( L ‘𝑋) → (𝑙 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑙) ∈ ( bday ‘𝑋)))
40	36, 39	mpbid 233	. . . . . . . . . . . 12 ⊢ (𝑙 ∈ ( L ‘𝑋) → ( bday ‘𝑙) ∈ ( bday ‘𝑋))
41		naddel1 8620	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑙) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
42	25, 37, 30, 41	mp3an 1469	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑙) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
43	40, 42	sylib 219	. . . . . . . . . . 11 ⊢ (𝑙 ∈ ( L ‘𝑋) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
44	43	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
45		elun1 4118	. . . . . . . . . 10 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
46	44, 45	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
47	35, 46	eqeltrid 2844	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
48	16, 18, 20, 22, 47	addsproplem1 27986	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → ((𝑙 +_s 𝑌) ∈ No ∧ (𝑌 <s 0_s → (𝑌 +_s 𝑙) <s ( 0_s +_s 𝑙))))
49	48	simpld 495	. . . . . 6 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (𝑙 +_s 𝑌) ∈ No )
50		eleq1a 2835	. . . . . 6 ⊢ ((𝑙 +_s 𝑌) ∈ No → (𝑝 = (𝑙 +_s 𝑌) → 𝑝 ∈ No ))
51	49, 50	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (𝑝 = (𝑙 +_s 𝑌) → 𝑝 ∈ No ))
52	51	rexlimdva 3141	. . . 4 ⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌) → 𝑝 ∈ No ))
53	52	abssdv 4005	. . 3 ⊢ (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ⊆ No )
54	15	adantr 481	. . . . . . . 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 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 𝑋 ∈ No )
57		leftno 27894	. . . . . . . . 9 ⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ No )
58	57	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 𝑚 ∈ No )
59	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 0_s ∈ No )
60	23	oveq2i 7374	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑋) +no ( bday ‘ 0_s )) = (( bday ‘𝑋) +no ∅)
61		naddrid 8616	. . . . . . . . . . . . 13 ⊢ (( bday ‘𝑋) ∈ On → (( bday ‘𝑋) +no ∅) = ( bday ‘𝑋))
62	37, 61	ax-mp 5	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑋) +no ∅) = ( bday ‘𝑋)
63	60, 62	eqtri 2763	. . . . . . . . . . 11 ⊢ (( bday ‘𝑋) +no ( bday ‘ 0_s )) = ( bday ‘𝑋)
64	63	uneq2i 4102	. . . . . . . . . 10 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑋))
65		bdayon 27769	. . . . . . . . . . . 12 ⊢ ( bday ‘𝑚) ∈ On
66		naddword1 8624	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑚) ∈ On) → ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑚)))
67	37, 65, 66	mp2an 698	. . . . . . . . . . 11 ⊢ ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑚))
68		ssequn2 4125	. . . . . . . . . . 11 ⊢ (( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑚)) ↔ ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑚)))
69	67, 68	mpbi 231	. . . . . . . . . 10 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑚))
70	64, 69	eqtri 2763	. . . . . . . . 9 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) = (( bday ‘𝑋) +no ( bday ‘𝑚))
71		leftold 27892	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ ( O ‘( bday ‘𝑌)))
72		oldbday 27918	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑌) ∈ On ∧ 𝑚 ∈ No ) → (𝑚 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑚) ∈ ( bday ‘𝑌)))
73	30, 57, 72	sylancr 593	. . . . . . . . . . . . 13 ⊢ (𝑚 ∈ ( L ‘𝑌) → (𝑚 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑚) ∈ ( bday ‘𝑌)))
74	71, 73	mpbid 233	. . . . . . . . . . . 12 ⊢ (𝑚 ∈ ( L ‘𝑌) → ( bday ‘𝑚) ∈ ( bday ‘𝑌))
75		naddel2 8621	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑚) ∈ ( bday ‘𝑌) ↔ (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
76	65, 30, 37, 75	mp3an 1469	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑚) ∈ ( bday ‘𝑌) ↔ (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
77	74, 76	sylib 219	. . . . . . . . . . 11 ⊢ (𝑚 ∈ ( L ‘𝑌) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
78	77	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
79		elun1 4118	. . . . . . . . . 10 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
80	78, 79	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
81	70, 80	eqeltrid 2844	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
82	54, 56, 58, 59, 81	addsproplem1 27986	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → ((𝑋 +_s 𝑚) ∈ No ∧ (𝑚 <s 0_s → (𝑚 +_s 𝑋) <s ( 0_s +_s 𝑋))))
83	82	simpld 495	. . . . . 6 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (𝑋 +_s 𝑚) ∈ No )
84		eleq1a 2835	. . . . . 6 ⊢ ((𝑋 +_s 𝑚) ∈ No → (𝑞 = (𝑋 +_s 𝑚) → 𝑞 ∈ No ))
85	83, 84	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (𝑞 = (𝑋 +_s 𝑚) → 𝑞 ∈ No ))
86	85	rexlimdva 3141	. . . 4 ⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚) → 𝑞 ∈ No ))
87	86	abssdv 4005	. . 3 ⊢ (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)} ⊆ No )
88	53, 87	unssd 4128	. 2 ⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ⊆ No )
89	15	adantr 481	. . . . . . . 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 27895	. . . . . . . . 9 ⊢ (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ No )
91	90	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 𝑟 ∈ No )
92	19	adantr 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 𝑌 ∈ No )
93	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 0_s ∈ No )
94	23	oveq2i 7374	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑟) +no ( bday ‘ 0_s )) = (( bday ‘𝑟) +no ∅)
95		bdayon 27769	. . . . . . . . . . . . 13 ⊢ ( bday ‘𝑟) ∈ On
96		naddrid 8616	. . . . . . . . . . . . 13 ⊢ (( bday ‘𝑟) ∈ On → (( bday ‘𝑟) +no ∅) = ( bday ‘𝑟))
97	95, 96	ax-mp 5	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑟) +no ∅) = ( bday ‘𝑟)
98	94, 97	eqtri 2763	. . . . . . . . . . 11 ⊢ (( bday ‘𝑟) +no ( bday ‘ 0_s )) = ( bday ‘𝑟)
99	98	uneq2i 4102	. . . . . . . . . 10 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑟))
100		naddword1 8624	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑌) ∈ On) → ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑌)))
101	95, 30, 100	mp2an 698	. . . . . . . . . . 11 ⊢ ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑌))
102		ssequn2 4125	. . . . . . . . . . 11 ⊢ (( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑌)) ↔ ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑌)))
103	101, 102	mpbi 231	. . . . . . . . . 10 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑌))
104	99, 103	eqtri 2763	. . . . . . . . 9 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) = (( bday ‘𝑟) +no ( bday ‘𝑌))
105		rightold 27893	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ ( O ‘( bday ‘𝑋)))
106		oldbday 27918	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑟 ∈ No ) → (𝑟 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑟) ∈ ( bday ‘𝑋)))
107	37, 90, 106	sylancr 593	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ ( R ‘𝑋) → (𝑟 ∈ ( O ‘( bday ‘𝑋)) ↔ ( bday ‘𝑟) ∈ ( bday ‘𝑋)))
108	105, 107	mpbid 233	. . . . . . . . . . . 12 ⊢ (𝑟 ∈ ( R ‘𝑋) → ( bday ‘𝑟) ∈ ( bday ‘𝑋))
109		naddel1 8620	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑟) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
110	95, 37, 30, 109	mp3an 1469	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑟) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
111	108, 110	sylib 219	. . . . . . . . . . 11 ⊢ (𝑟 ∈ ( R ‘𝑋) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
112	111	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
113		elun1 4118	. . . . . . . . . 10 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
114	112, 113	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
115	104, 114	eqeltrid 2844	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
116	89, 91, 92, 93, 115	addsproplem1 27986	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → ((𝑟 +_s 𝑌) ∈ No ∧ (𝑌 <s 0_s → (𝑌 +_s 𝑟) <s ( 0_s +_s 𝑟))))
117	116	simpld 495	. . . . . 6 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (𝑟 +_s 𝑌) ∈ No )
118		eleq1a 2835	. . . . . 6 ⊢ ((𝑟 +_s 𝑌) ∈ No → (𝑤 = (𝑟 +_s 𝑌) → 𝑤 ∈ No ))
119	117, 118	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (𝑤 = (𝑟 +_s 𝑌) → 𝑤 ∈ No ))
120	119	rexlimdva 3141	. . . 4 ⊢ (𝜑 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌) → 𝑤 ∈ No ))
121	120	abssdv 4005	. . 3 ⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ⊆ No )
122	15	adantr 481	. . . . . . . 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 481	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 𝑋 ∈ No )
124		rightno 27895	. . . . . . . . 9 ⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ No )
125	124	adantl 482	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 𝑠 ∈ No )
126	21	a1i 11	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 0_s ∈ No )
127	63	uneq2i 4102	. . . . . . . . . 10 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑋))
128		bdayon 27769	. . . . . . . . . . . 12 ⊢ ( bday ‘𝑠) ∈ On
129		naddword1 8624	. . . . . . . . . . . 12 ⊢ ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑠) ∈ On) → ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑠)))
130	37, 128, 129	mp2an 698	. . . . . . . . . . 11 ⊢ ( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑠))
131		ssequn2 4125	. . . . . . . . . . 11 ⊢ (( bday ‘𝑋) ⊆ (( bday ‘𝑋) +no ( bday ‘𝑠)) ↔ ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑠)))
132	130, 131	mpbi 231	. . . . . . . . . 10 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑠))
133	127, 132	eqtri 2763	. . . . . . . . 9 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) = (( bday ‘𝑋) +no ( bday ‘𝑠))
134		rightold 27893	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ ( O ‘( bday ‘𝑌)))
135		oldbday 27918	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑌) ∈ On ∧ 𝑠 ∈ No ) → (𝑠 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑠) ∈ ( bday ‘𝑌)))
136	30, 124, 135	sylancr 593	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ( R ‘𝑌) → (𝑠 ∈ ( O ‘( bday ‘𝑌)) ↔ ( bday ‘𝑠) ∈ ( bday ‘𝑌)))
137	134, 136	mpbid 233	. . . . . . . . . . . 12 ⊢ (𝑠 ∈ ( R ‘𝑌) → ( bday ‘𝑠) ∈ ( bday ‘𝑌))
138		naddel2 8621	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑠) ∈ ( bday ‘𝑌) ↔ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌))))
139	128, 30, 37, 138	mp3an 1469	. . . . . . . . . . . 12 ⊢ (( bday ‘𝑠) ∈ ( bday ‘𝑌) ↔ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
140	137, 139	sylib 219	. . . . . . . . . . 11 ⊢ (𝑠 ∈ ( R ‘𝑌) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
141	140	adantl 482	. . . . . . . . . 10 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
142		elun1 4118	. . . . . . . . . 10 ⊢ ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
143	141, 142	syl 17	. . . . . . . . 9 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
144	133, 143	eqeltrid 2844	. . . . . . . 8 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ((( bday ‘𝑋) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
145	122, 123, 125, 126, 144	addsproplem1 27986	. . . . . . 7 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ((𝑋 +_s 𝑠) ∈ No ∧ (𝑠 <s 0_s → (𝑠 +_s 𝑋) <s ( 0_s +_s 𝑋))))
146	145	simpld 495	. . . . . 6 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (𝑋 +_s 𝑠) ∈ No )
147		eleq1a 2835	. . . . . 6 ⊢ ((𝑋 +_s 𝑠) ∈ No → (𝑡 = (𝑋 +_s 𝑠) → 𝑡 ∈ No ))
148	146, 147	syl 17	. . . . 5 ⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (𝑡 = (𝑋 +_s 𝑠) → 𝑡 ∈ No ))
149	148	rexlimdva 3141	. . . 4 ⊢ (𝜑 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠) → 𝑡 ∈ No ))
150	149	abssdv 4005	. . 3 ⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)} ⊆ No )
151	121, 150	unssd 4128	. 2 ⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)}) ⊆ No )
152		elun 4090	. . . . . . 7 ⊢ (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ↔ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}))
153		vex 3436	. . . . . . . . 9 ⊢ 𝑎 ∈ V
154		eqeq1 2744	. . . . . . . . . 10 ⊢ (𝑝 = 𝑎 → (𝑝 = (𝑙 +_s 𝑌) ↔ 𝑎 = (𝑙 +_s 𝑌)))
155	154	rexbidv 3164	. . . . . . . . 9 ⊢ (𝑝 = 𝑎 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌) ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌)))
156	153, 155	elab 3624	. . . . . . . 8 ⊢ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌))
157		eqeq1 2744	. . . . . . . . . 10 ⊢ (𝑞 = 𝑎 → (𝑞 = (𝑋 +_s 𝑚) ↔ 𝑎 = (𝑋 +_s 𝑚)))
158	157	rexbidv 3164	. . . . . . . . 9 ⊢ (𝑞 = 𝑎 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚) ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚)))
159	153, 158	elab 3624	. . . . . . . 8 ⊢ (𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)} ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚))
160	156, 159	orbi12i 920	. . . . . . 7 ⊢ ((𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚)))
161	152, 160	bitri 276	. . . . . 6 ⊢ (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚)))
162		elun 4090	. . . . . . 7 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)}))
163		vex 3436	. . . . . . . . 9 ⊢ 𝑏 ∈ V
164		eqeq1 2744	. . . . . . . . . 10 ⊢ (𝑤 = 𝑏 → (𝑤 = (𝑟 +_s 𝑌) ↔ 𝑏 = (𝑟 +_s 𝑌)))
165	164	rexbidv 3164	. . . . . . . . 9 ⊢ (𝑤 = 𝑏 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌) ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)))
166	163, 165	elab 3624	. . . . . . . 8 ⊢ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌))
167		eqeq1 2744	. . . . . . . . . 10 ⊢ (𝑡 = 𝑏 → (𝑡 = (𝑋 +_s 𝑠) ↔ 𝑏 = (𝑋 +_s 𝑠)))
168	167	rexbidv 3164	. . . . . . . . 9 ⊢ (𝑡 = 𝑏 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠) ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)))
169	163, 168	elab 3624	. . . . . . . 8 ⊢ (𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)} ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠))
170	166, 169	orbi12i 920	. . . . . . 7 ⊢ ((𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)}) ↔ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)))
171	162, 170	bitri 276	. . . . . 6 ⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)}) ↔ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)))
172	161, 171	anbi12i 634	. . . . 5 ⊢ ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)})) ↔ ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚)) ∧ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠))))
173		anddi 1018	. . . . 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 276	. . . 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 3212	. . . . . . 7 ⊢ (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)))
176		lltr 27879	. . . . . . . . . . . 12 ⊢ ( L ‘𝑋) <<s ( R ‘𝑋)
177	176	a1i 11	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ( L ‘𝑋) <<s ( R ‘𝑋))
178		simprl 776	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ ( L ‘𝑋))
179		simprr 778	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ ( R ‘𝑋))
180	177, 178, 179	sltssepcd 27789	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 <s 𝑟)
181	15	adantr 481	. . . . . . . . . . . 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 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 ∈ No )
183	17	ad2antrl 734	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ No )
184	90	ad2antll 735	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ No )
185		naddcom 8615	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑌)))
186	30, 25, 185	mp2an 698	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑌) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑌))
187	43	ad2antrl 734	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
188	186, 187	eqeltrid 2844	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
189		naddcom 8615	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑌)))
190	30, 95, 189	mp2an 698	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑌) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑌))
191	111	ad2antll 735	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
192	190, 191	eqeltrid 2844	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
193		naddcl 8610	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ On)
194	30, 25, 193	mp2an 698	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑌) +no ( bday ‘𝑙)) ∈ On
195		naddcl 8610	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑌) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ On)
196	30, 95, 195	mp2an 698	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑌) +no ( bday ‘𝑟)) ∈ On
197		naddcl 8610	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On)
198	37, 30, 197	mp2an 698	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑋) +no ( bday ‘𝑌)) ∈ On
199		onunel 6424	. . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . 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 589	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑌) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
202		elun1 4118	. . . . . . . . . . . . 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 17	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑌) +no ( bday ‘𝑟))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
204	181, 182, 183, 184, 203	addsproplem1 27986	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑌 +_s 𝑙) ∈ No ∧ (𝑙 <s 𝑟 → (𝑙 +_s 𝑌) <s (𝑟 +_s 𝑌))))
205	204	simprd 496	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 <s 𝑟 → (𝑙 +_s 𝑌) <s (𝑟 +_s 𝑌)))
206	180, 205	mpd 15	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 +_s 𝑌) <s (𝑟 +_s 𝑌))
207		breq12 5084	. . . . . . . . 9 ⊢ ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑙 +_s 𝑌) <s (𝑟 +_s 𝑌)))
208	206, 207	syl5ibrcom 248	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
209	208	rexlimdvva 3197	. . . . . . 7 ⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
210	175, 209	biimtrrid 244	. . . . . 6 ⊢ (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
211		reeanv 3212	. . . . . . 7 ⊢ (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑋 +_s 𝑠)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)))
212	49	adantrr 723	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +_s 𝑌) ∈ No )
213	15	adantr 481	. . . . . . . . . . . 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 734	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 ∈ No )
215	124	ad2antll 735	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ No )
216	21	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 0_s ∈ No )
217	28	uneq2i 4102	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑙))
218		naddword1 8624	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑠) ∈ On) → ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑠)))
219	25, 128, 218	mp2an 698	. . . . . . . . . . . . . . 15 ⊢ ( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑠))
220		ssequn2 4125	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑙) ⊆ (( bday ‘𝑙) +no ( bday ‘𝑠)) ↔ ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑠)))
221	219, 220	mpbi 231	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑠))
222	217, 221	eqtri 2763	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) = (( bday ‘𝑙) +no ( bday ‘𝑠))
223		naddel1 8620	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑠) ∈ On) → (( bday ‘𝑙) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠))))
224	25, 37, 128, 223	mp3an 1469	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑙) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠)))
225	40, 224	sylib 219	. . . . . . . . . . . . . . . 16 ⊢ (𝑙 ∈ ( L ‘𝑋) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠)))
226	225	ad2antrl 734	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑠)))
227	140	ad2antll 735	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
228		ontr1 6364	. . . . . . . . . . . . . . . 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 590	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
231		elun1 4118	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
232	230, 231	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
233	222, 232	eqeltrid 2844	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑙) +no ( bday ‘𝑠)) ∪ (( bday ‘𝑙) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
234	213, 214, 215, 216, 233	addsproplem1 27986	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +_s 𝑠) ∈ No ∧ (𝑠 <s 0_s → (𝑠 +_s 𝑙) <s ( 0_s +_s 𝑙))))
235	234	simpld 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +_s 𝑠) ∈ No )
236	146	adantrl 722	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +_s 𝑠) ∈ No )
237		rightgt 27871	. . . . . . . . . . . . 13 ⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑌 <s 𝑠)
238	237	ad2antll 735	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 <s 𝑠)
239	19	adantr 481	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 ∈ No )
240	43	ad2antrl 734	. . . . . . . . . . . . . . . 16 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
241		naddcl 8610	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ On)
242	25, 30, 241	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑙) +no ( bday ‘𝑌)) ∈ On
243		naddcl 8610	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑙) ∈ On ∧ ( bday ‘𝑠) ∈ On) → (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ On)
244	25, 128, 243	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑙) +no ( bday ‘𝑠)) ∈ On
245		onunel 6424	. . . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
248		elun1 4118	. . . . . . . . . . . . . . 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 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑙) +no ( bday ‘𝑠))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
250	213, 214, 239, 215, 249	addsproplem1 27986	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +_s 𝑌) ∈ No ∧ (𝑌 <s 𝑠 → (𝑌 +_s 𝑙) <s (𝑠 +_s 𝑙))))
251	250	simprd 496	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 <s 𝑠 → (𝑌 +_s 𝑙) <s (𝑠 +_s 𝑙)))
252	238, 251	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 +_s 𝑙) <s (𝑠 +_s 𝑙))
253	214, 239	addscomd 27984	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +_s 𝑌) = (𝑌 +_s 𝑙))
254	214, 215	addscomd 27984	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +_s 𝑠) = (𝑠 +_s 𝑙))
255	252, 253, 254	3brtr4d 5111	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +_s 𝑌) <s (𝑙 +_s 𝑠))
256		leftlt 27870	. . . . . . . . . . . 12 ⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 <s 𝑋)
257	256	ad2antrl 734	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 <s 𝑋)
258	55	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 ∈ No )
259		naddcom 8615	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑠)))
260	128, 25, 259	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑠) +no ( bday ‘𝑙)) = (( bday ‘𝑙) +no ( bday ‘𝑠))
261	260, 230	eqeltrid 2844	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
262		naddcom 8615	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑠)))
263	128, 37, 262	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑠) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑠))
264	263, 227	eqeltrid 2844	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
265		naddcl 8610	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑙) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ On)
266	128, 25, 265	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑠) +no ( bday ‘𝑙)) ∈ On
267		naddcl 8610	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑠) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ On)
268	128, 37, 267	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑠) +no ( bday ‘𝑋)) ∈ On
269		onunel 6424	. . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑠) +no ( bday ‘𝑋))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
272		elun1 4118	. . . . . . . . . . . . . 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 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday ‘𝑠) +no ( bday ‘𝑋))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
274	213, 215, 214, 258, 273	addsproplem1 27986	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑠 +_s 𝑙) ∈ No ∧ (𝑙 <s 𝑋 → (𝑙 +_s 𝑠) <s (𝑋 +_s 𝑠))))
275	274	simprd 496	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 <s 𝑋 → (𝑙 +_s 𝑠) <s (𝑋 +_s 𝑠)))
276	257, 275	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +_s 𝑠) <s (𝑋 +_s 𝑠))
277	212, 235, 236, 255, 276	ltstrd 27752	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +_s 𝑌) <s (𝑋 +_s 𝑠))
278		breq12 5084	. . . . . . . . 9 ⊢ ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑋 +_s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑙 +_s 𝑌) <s (𝑋 +_s 𝑠)))
279	277, 278	syl5ibrcom 248	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
280	279	rexlimdvva 3197	. . . . . . 7 ⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +_s 𝑌) ∧ 𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
281	211, 280	biimtrrid 244	. . . . . 6 ⊢ (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
282	210, 281	jaod 865	. . . . 5 ⊢ (𝜑 → (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠))) → 𝑎 <s 𝑏))
283		reeanv 3212	. . . . . . 7 ⊢ (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑟 +_s 𝑌)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)))
284	15	adantr 481	. . . . . . . . . . . 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 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 ∈ No )
286	57	ad2antrl 734	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ No )
287	21	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 0_s ∈ No )
288	77	ad2antrl 734	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
289	288, 79	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
290	70, 289	eqeltrid 2844	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
291	284, 285, 286, 287, 290	addsproplem1 27986	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑋 +_s 𝑚) ∈ No ∧ (𝑚 <s 0_s → (𝑚 +_s 𝑋) <s ( 0_s +_s 𝑋))))
292	291	simpld 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +_s 𝑚) ∈ No )
293	90	ad2antll 735	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ No )
294	98	uneq2i 4102	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) = ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑟))
295		naddword1 8624	. . . . . . . . . . . . . . . 16 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑚) ∈ On) → ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑚)))
296	95, 65, 295	mp2an 698	. . . . . . . . . . . . . . 15 ⊢ ( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑚))
297		ssequn2 4125	. . . . . . . . . . . . . . 15 ⊢ (( bday ‘𝑟) ⊆ (( bday ‘𝑟) +no ( bday ‘𝑚)) ↔ ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑚)))
298	296, 297	mpbi 231	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑚))
299	294, 298	eqtri 2763	. . . . . . . . . . . . 13 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) = (( bday ‘𝑟) +no ( bday ‘𝑚))
300		naddel1 8620	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑚) ∈ On) → (( bday ‘𝑟) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚))))
301	95, 37, 65, 300	mp3an 1469	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑟) ∈ ( bday ‘𝑋) ↔ (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚)))
302	108, 301	sylib 219	. . . . . . . . . . . . . . . 16 ⊢ (𝑟 ∈ ( R ‘𝑋) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚)))
303	302	ad2antll 735	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑚)))
304		ontr1 6364	. . . . . . . . . . . . . . . 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 590	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
307		elun1 4118	. . . . . . . . . . . . . 14 ⊢ ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
308	306, 307	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
309	299, 308	eqeltrid 2844	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
310	284, 293, 286, 287, 309	addsproplem1 27986	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +_s 𝑚) ∈ No ∧ (𝑚 <s 0_s → (𝑚 +_s 𝑟) <s ( 0_s +_s 𝑟))))
311	310	simpld 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +_s 𝑚) ∈ No )
312	19	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 ∈ No )
313	111	ad2antll 735	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
314	313, 113	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
315	104, 314	eqeltrid 2844	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑟) +no ( bday ‘ 0_s ))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
316	284, 293, 312, 287, 315	addsproplem1 27986	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +_s 𝑌) ∈ No ∧ (𝑌 <s 0_s → (𝑌 +_s 𝑟) <s ( 0_s +_s 𝑟))))
317	316	simpld 495	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +_s 𝑌) ∈ No )
318		rightval 27867	. . . . . . . . . . . . . . . 16 ⊢ ( R ‘𝑋) = {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟}
319	318	eleq2i 2832	. . . . . . . . . . . . . . 15 ⊢ (𝑟 ∈ ( R ‘𝑋) ↔ 𝑟 ∈ {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟})
320	319	biimpi 217	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟})
321	320	ad2antll 735	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟})
322		rabid 3413	. . . . . . . . . . . . 13 ⊢ (𝑟 ∈ {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟} ↔ (𝑟 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑟))
323	321, 322	sylib 219	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 ∈ ( O ‘( bday ‘𝑋)) ∧ 𝑋 <s 𝑟))
324	323	simprd 496	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 <s 𝑟)
325		naddcom 8615	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑚)))
326	65, 37, 325	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑚) +no ( bday ‘𝑋)) = (( bday ‘𝑋) +no ( bday ‘𝑚))
327	326, 288	eqeltrid 2844	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
328		naddcom 8615	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑚)))
329	65, 95, 328	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑚) +no ( bday ‘𝑟)) = (( bday ‘𝑟) +no ( bday ‘𝑚))
330	329, 306	eqeltrid 2844	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
331		naddcl 8610	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑋) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ On)
332	65, 37, 331	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑚) +no ( bday ‘𝑋)) ∈ On
333		naddcl 8610	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑚) ∈ On ∧ ( bday ‘𝑟) ∈ On) → (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ On)
334	65, 95, 333	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑚) +no ( bday ‘𝑟)) ∈ On
335		onunel 6424	. . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday ‘𝑚) +no ( bday ‘𝑟))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
338		elun1 4118	. . . . . . . . . . . . . 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 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday ‘𝑚) +no ( bday ‘𝑟))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
340	284, 286, 285, 293, 339	addsproplem1 27986	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑚 +_s 𝑋) ∈ No ∧ (𝑋 <s 𝑟 → (𝑋 +_s 𝑚) <s (𝑟 +_s 𝑚))))
341	340	simprd 496	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 <s 𝑟 → (𝑋 +_s 𝑚) <s (𝑟 +_s 𝑚)))
342	324, 341	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +_s 𝑚) <s (𝑟 +_s 𝑚))
343		leftval 27866	. . . . . . . . . . . . . . . . 17 ⊢ ( L ‘𝑌) = {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌}
344	343	eleq2i 2832	. . . . . . . . . . . . . . . 16 ⊢ (𝑚 ∈ ( L ‘𝑌) ↔ 𝑚 ∈ {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌})
345	344	biimpi 217	. . . . . . . . . . . . . . 15 ⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌})
346	345	ad2antrl 734	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌})
347		rabid 3413	. . . . . . . . . . . . . 14 ⊢ (𝑚 ∈ {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌} ↔ (𝑚 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑚 <s 𝑌))
348	346, 347	sylib 219	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 ∈ ( O ‘( bday ‘𝑌)) ∧ 𝑚 <s 𝑌))
349	348	simprd 496	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 <s 𝑌)
350		naddcl 8610	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑚) ∈ On) → (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ On)
351	95, 65, 350	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑟) +no ( bday ‘𝑚)) ∈ On
352		naddcl 8610	. . . . . . . . . . . . . . . . . 18 ⊢ ((( bday ‘𝑟) ∈ On ∧ ( bday ‘𝑌) ∈ On) → (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ On)
353	95, 30, 352	mp2an 698	. . . . . . . . . . . . . . . . 17 ⊢ (( bday ‘𝑟) +no ( bday ‘𝑌)) ∈ On
354		onunel 6424	. . . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘𝑌))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
357		elun1 4118	. . . . . . . . . . . . . . 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 17	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday ‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑟) +no ( bday ‘𝑌))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
359	284, 293, 286, 312, 358	addsproplem1 27986	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +_s 𝑚) ∈ No ∧ (𝑚 <s 𝑌 → (𝑚 +_s 𝑟) <s (𝑌 +_s 𝑟))))
360	359	simprd 496	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 <s 𝑌 → (𝑚 +_s 𝑟) <s (𝑌 +_s 𝑟)))
361	349, 360	mpd 15	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 +_s 𝑟) <s (𝑌 +_s 𝑟))
362	293, 286	addscomd 27984	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +_s 𝑚) = (𝑚 +_s 𝑟))
363	293, 312	addscomd 27984	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +_s 𝑌) = (𝑌 +_s 𝑟))
364	361, 362, 363	3brtr4d 5111	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +_s 𝑚) <s (𝑟 +_s 𝑌))
365	292, 311, 317, 342, 364	ltstrd 27752	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +_s 𝑚) <s (𝑟 +_s 𝑌))
366		breq12 5084	. . . . . . . . 9 ⊢ ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑟 +_s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑋 +_s 𝑚) <s (𝑟 +_s 𝑌)))
367	365, 366	syl5ibrcom 248	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
368	367	rexlimdvva 3197	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
369	283, 368	biimtrrid 244	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)) → 𝑎 <s 𝑏))
370		reeanv 3212	. . . . . . 7 ⊢ (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑋 +_s 𝑠)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)))
371		lltr 27879	. . . . . . . . . . . . 13 ⊢ ( L ‘𝑌) <<s ( R ‘𝑌)
372	371	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ( L ‘𝑌) <<s ( R ‘𝑌))
373		simprl 776	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ ( L ‘𝑌))
374		simprr 778	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ ( R ‘𝑌))
375	372, 373, 374	sltssepcd 27789	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 <s 𝑠)
376	15	adantr 481	. . . . . . . . . . . . 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 481	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 ∈ No )
378	57	ad2antrl 734	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ No )
379	124	ad2antll 735	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ No )
380	77	ad2antrl 734	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
381	140	ad2antll 735	. . . . . . . . . . . . . . 15 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
382		naddcl 8610	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑚) ∈ On) → (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ On)
383	37, 65, 382	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑋) +no ( bday ‘𝑚)) ∈ On
384		naddcl 8610	. . . . . . . . . . . . . . . . 17 ⊢ ((( bday ‘𝑋) ∈ On ∧ ( bday ‘𝑠) ∈ On) → (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ On)
385	37, 128, 384	mp2an 698	. . . . . . . . . . . . . . . 16 ⊢ (( bday ‘𝑋) +no ( bday ‘𝑠)) ∈ On
386		onunel 6424	. . . . . . . . . . . . . . . 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 1469	. . . . . . . . . . . . . . 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 589	. . . . . . . . . . . . . 14 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑠))) ∈ (( bday ‘𝑋) +no ( bday ‘𝑌)))
389		elun1 4118	. . . . . . . . . . . . . 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 17	. . . . . . . . . . . . 13 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday ‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑠))) ∈ ((( bday ‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday ‘𝑋) +no ( bday ‘𝑍))))
391	376, 377, 378, 379, 390	addsproplem1 27986	. . . . . . . . . . . 12 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑋 +_s 𝑚) ∈ No ∧ (𝑚 <s 𝑠 → (𝑚 +_s 𝑋) <s (𝑠 +_s 𝑋))))
392	391	simprd 496	. . . . . . . . . . 11 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 <s 𝑠 → (𝑚 +_s 𝑋) <s (𝑠 +_s 𝑋)))
393	375, 392	mpd 15	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 +_s 𝑋) <s (𝑠 +_s 𝑋))
394	377, 378	addscomd 27984	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +_s 𝑚) = (𝑚 +_s 𝑋))
395	377, 379	addscomd 27984	. . . . . . . . . 10 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +_s 𝑠) = (𝑠 +_s 𝑋))
396	393, 394, 395	3brtr4d 5111	. . . . . . . . 9 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +_s 𝑚) <s (𝑋 +_s 𝑠))
397		breq12 5084	. . . . . . . . 9 ⊢ ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑋 +_s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑋 +_s 𝑚) <s (𝑋 +_s 𝑠)))
398	396, 397	syl5ibrcom 248	. . . . . . . 8 ⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
399	398	rexlimdvva 3197	. . . . . . 7 ⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +_s 𝑚) ∧ 𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
400	370, 399	biimtrrid 244	. . . . . 6 ⊢ (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)) → 𝑎 <s 𝑏))
401	369, 400	jaod 865	. . . . 5 ⊢ (𝜑 → (((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠))) → 𝑎 <s 𝑏))
402	282, 401	jaod 865	. . . 4 ⊢ (𝜑 → ((((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +_s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠))) ∨ ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +_s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +_s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +_s 𝑠)))) → 𝑎 <s 𝑏))
403	174, 402	biimtrid 243	. . 3 ⊢ (𝜑 → ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)})) → 𝑎 <s 𝑏))
404	403	3impib 1122	. 2 ⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)})) → 𝑎 <s 𝑏)
405	7, 14, 88, 151, 404	sltsd 27785	1 ⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +_s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +_s 𝑚)}) <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +_s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +_s 𝑠)}))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 207 ∧ wa 396 ∨ wo 853 = wceq 1547 ∈ wcel 2119 {cab 2718 ∀wral 3054 ∃wrex 3064 {crab 3392 Vcvv 3432 ∪ cun 3888 ⊆ wss 3890 ∅c0 4268 class class class wbr 5079 Oncon0 6317 ‘cfv 6492 (class class class)co 7363 +no cnadd 8598 No csur 27628 <s clts 27629 bday cbday 27630 <<s cslts 27774 0_s c0s 27822 O cold 27840 L cleft 27842 R cright 27843 +_s cadds 27976

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2712 ax-rep 5206 ax-sep 5225 ax-nul 5235 ax-pow 5301 ax-pr 5369 ax-un 7685

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2719 df-cleq 2732 df-clel 2815 df-nfc 2889 df-ne 2936 df-ral 3055 df-rex 3065 df-rmo 3345 df-reu 3346 df-rab 3393 df-v 3434 df-sbc 3731 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-pss 3910 df-nul 4269 df-if 4462 df-pw 4538 df-sn 4563 df-pr 4565 df-tp 4567 df-op 4569 df-uni 4846 df-int 4885 df-iun 4930 df-br 5080 df-opab 5142 df-mpt 5161 df-tr 5187 df-id 5520 df-eprel 5525 df-po 5533 df-so 5534 df-fr 5578 df-se 5579 df-we 5580 df-xp 5631 df-rel 5632 df-cnv 5633 df-co 5634 df-dm 5635 df-rn 5636 df-res 5637 df-ima 5638 df-pred 6259 df-ord 6320 df-on 6321 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7320 df-ov 7366 df-oprab 7367 df-mpo 7368 df-1st 7938 df-2nd 7939 df-frecs 8228 df-wrecs 8259 df-recs 8308 df-1o 8402 df-2o 8403 df-nadd 8599 df-no 27631 df-lts 27632 df-bday 27633 df-slts 27775 df-cuts 27777 df-0s 27824 df-made 27844 df-old 27845 df-left 27847 df-right 27848 df-norec2 27966 df-adds 27977

This theorem is referenced by: addsproplem3 27988

W3C validator