Step | Hyp | Ref
| Expression |
1 | | fvex 6856 |
. . . . 5
⊢ ( L
‘𝑋) ∈
V |
2 | 1 | abrexex 7896 |
. . . 4
⊢ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V |
3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V) |
4 | | fvex 6856 |
. . . . 5
⊢ ( L
‘𝑌) ∈
V |
5 | 4 | abrexex 7896 |
. . . 4
⊢ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V |
6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V) |
7 | 3, 6 | unexd 7689 |
. 2
⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∈ V) |
8 | | fvex 6856 |
. . . . 5
⊢ ( R
‘𝑋) ∈
V |
9 | 8 | abrexex 7896 |
. . . 4
⊢ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V |
10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V) |
11 | | fvex 6856 |
. . . . 5
⊢ ( R
‘𝑌) ∈
V |
12 | 11 | abrexex 7896 |
. . . 4
⊢ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V |
13 | 12 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V) |
14 | 10, 13 | unexd 7689 |
. 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 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
17 | | leftssno 27213 |
. . . . . . . . . 10
⊢ ( L
‘𝑋) ⊆ No |
18 | 17 | sseli 3941 |
. . . . . . . . 9
⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ No
) |
19 | 18 | adantl 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 𝑙 ∈ No
) |
20 | | addsproplem2.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ No
) |
21 | 20 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 𝑌 ∈ No
) |
22 | | 0sno 27168 |
. . . . . . . . 9
⊢
0s ∈ No |
23 | 22 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 0s ∈ No ) |
24 | | bday0s 27170 |
. . . . . . . . . . . . 13
⊢ ( bday ‘ 0s ) = ∅ |
25 | 24 | oveq2i 7369 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑙) +no ( bday
‘ 0s )) = (( bday
‘𝑙) +no
∅) |
26 | | bdayelon 27119 |
. . . . . . . . . . . . 13
⊢ ( bday ‘𝑙) ∈ On |
27 | | naddid1 8630 |
. . . . . . . . . . . . 13
⊢ (( bday ‘𝑙) ∈ On → ((
bday ‘𝑙) +no
∅) = ( bday ‘𝑙)) |
28 | 26, 27 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑙) +no ∅) = ( bday
‘𝑙) |
29 | 25, 28 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑙) +no ( bday
‘ 0s )) = ( bday
‘𝑙) |
30 | 29 | uneq2i 4121 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑙) +no ( bday
‘ 0s ))) = ((( bday
‘𝑙) +no ( bday ‘𝑌)) ∪ ( bday
‘𝑙)) |
31 | | bdayelon 27119 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝑌) ∈ On |
32 | | naddword1 8637 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑌)
∈ On) → ( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑌))) |
33 | 26, 31, 32 | mp2an 691 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑌)) |
34 | | ssequn2 4144 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑌)) ↔ ((( bday
‘𝑙) +no ( bday ‘𝑌)) ∪ ( bday
‘𝑙)) = (( bday ‘𝑙) +no ( bday
‘𝑌))) |
35 | 33, 34 | mpbi 229 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑌)) ∪
( bday ‘𝑙)) = (( bday
‘𝑙) +no ( bday ‘𝑌)) |
36 | 30, 35 | eqtri 2765 |
. . . . . . . . 9
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑙) +no ( bday
‘ 0s ))) = (( bday
‘𝑙) +no ( bday ‘𝑌)) |
37 | | leftssold 27211 |
. . . . . . . . . . . . . 14
⊢ ( L
‘𝑋) ⊆ ( O
‘( bday ‘𝑋)) |
38 | 37 | sseli 3941 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ ( O ‘(
bday ‘𝑋))) |
39 | | bdayelon 27119 |
. . . . . . . . . . . . . 14
⊢ ( bday ‘𝑋) ∈ On |
40 | | oldbday 27233 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑙 ∈ No )
→ (𝑙 ∈ ( O
‘( bday ‘𝑋)) ↔ ( bday
‘𝑙) ∈
( bday ‘𝑋))) |
41 | 39, 18, 40 | sylancr 588 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ( L ‘𝑋) → (𝑙 ∈ ( O ‘(
bday ‘𝑋))
↔ ( bday ‘𝑙) ∈ ( bday
‘𝑋))) |
42 | 38, 41 | mpbid 231 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ ( L ‘𝑋) → (
bday ‘𝑙)
∈ ( bday ‘𝑋)) |
43 | | naddel1 8633 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑋)
∈ On ∧ ( bday ‘𝑌) ∈ On) → ((
bday ‘𝑙)
∈ ( bday ‘𝑋) ↔ (( bday
‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌)))) |
44 | 26, 39, 31, 43 | mp3an 1462 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑙) ∈ ( bday
‘𝑋) ↔
(( bday ‘𝑙) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
45 | 42, 44 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ ( L ‘𝑋) → (( bday ‘𝑙) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
46 | 45 | adantl 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (( bday
‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
47 | | elun1 4137 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
(( bday ‘𝑙) +no ( bday
‘𝑌)) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
48 | 46, 47 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (( bday
‘𝑙) +no ( bday ‘𝑌)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
49 | 36, 48 | eqeltrid 2842 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → ((( bday
‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
50 | 16, 19, 21, 23, 49 | addsproplem1 27284 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → ((𝑙 +s 𝑌) ∈ No
∧ (𝑌 <s
0s → (𝑌
+s 𝑙) <s (
0s +s 𝑙)))) |
51 | 50 | simpld 496 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (𝑙 +s 𝑌) ∈ No
) |
52 | | eleq1a 2833 |
. . . . . 6
⊢ ((𝑙 +s 𝑌) ∈ No
→ (𝑝 = (𝑙 +s 𝑌) → 𝑝 ∈ No
)) |
53 | 51, 52 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (𝑝 = (𝑙 +s 𝑌) → 𝑝 ∈ No
)) |
54 | 53 | rexlimdva 3153 |
. . . 4
⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) → 𝑝 ∈ No
)) |
55 | 54 | abssdv 4026 |
. . 3
⊢ (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ⊆ No
) |
56 | 15 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
57 | | addsproplem2.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝑋 ∈ No
) |
58 | 57 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 𝑋 ∈ No
) |
59 | | leftssno 27213 |
. . . . . . . . . 10
⊢ ( L
‘𝑌) ⊆ No |
60 | 59 | sseli 3941 |
. . . . . . . . 9
⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ No
) |
61 | 60 | adantl 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 𝑚 ∈ No
) |
62 | 22 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 0s ∈ No ) |
63 | 24 | oveq2i 7369 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑋) +no ( bday
‘ 0s )) = (( bday
‘𝑋) +no
∅) |
64 | | naddid1 8630 |
. . . . . . . . . . . . 13
⊢ (( bday ‘𝑋) ∈ On → ((
bday ‘𝑋) +no
∅) = ( bday ‘𝑋)) |
65 | 39, 64 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑋) +no ∅) = (
bday ‘𝑋) |
66 | 63, 65 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑋) +no ( bday
‘ 0s )) = ( bday
‘𝑋) |
67 | 66 | uneq2i 4121 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘ 0s ))) = ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ ( bday
‘𝑋)) |
68 | | bdayelon 27119 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝑚) ∈ On |
69 | | naddword1 8637 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑚)
∈ On) → ( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑚))) |
70 | 39, 68, 69 | mp2an 691 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑚)) |
71 | | ssequn2 4144 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑚)) ↔ ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ ( bday
‘𝑋)) = (( bday ‘𝑋) +no ( bday
‘𝑚))) |
72 | 70, 71 | mpbi 229 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
( bday ‘𝑋)) = (( bday
‘𝑋) +no ( bday ‘𝑚)) |
73 | 67, 72 | eqtri 2765 |
. . . . . . . . 9
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘ 0s ))) = (( bday
‘𝑋) +no ( bday ‘𝑚)) |
74 | | leftssold 27211 |
. . . . . . . . . . . . . 14
⊢ ( L
‘𝑌) ⊆ ( O
‘( bday ‘𝑌)) |
75 | 74 | sseli 3941 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ ( O ‘(
bday ‘𝑌))) |
76 | | oldbday 27233 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑌) ∈ On ∧ 𝑚 ∈ No )
→ (𝑚 ∈ ( O
‘( bday ‘𝑌)) ↔ ( bday
‘𝑚) ∈
( bday ‘𝑌))) |
77 | 31, 60, 76 | sylancr 588 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ( L ‘𝑌) → (𝑚 ∈ ( O ‘(
bday ‘𝑌))
↔ ( bday ‘𝑚) ∈ ( bday
‘𝑌))) |
78 | 75, 77 | mpbid 231 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ( L ‘𝑌) → (
bday ‘𝑚)
∈ ( bday ‘𝑌)) |
79 | | naddel2 8634 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑌)
∈ On ∧ ( bday ‘𝑋) ∈ On) → ((
bday ‘𝑚)
∈ ( bday ‘𝑌) ↔ (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌)))) |
80 | 68, 31, 39, 79 | mp3an 1462 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ↔
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
81 | 78, 80 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ( L ‘𝑌) → (( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
82 | 81 | adantl 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
83 | | elun1 4137 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
84 | 82, 83 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
85 | 73, 84 | eqeltrid 2842 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
86 | 56, 58, 61, 62, 85 | addsproplem1 27284 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → ((𝑋 +s 𝑚) ∈ No
∧ (𝑚 <s
0s → (𝑚
+s 𝑋) <s (
0s +s 𝑋)))) |
87 | 86 | simpld 496 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (𝑋 +s 𝑚) ∈ No
) |
88 | | eleq1a 2833 |
. . . . . 6
⊢ ((𝑋 +s 𝑚) ∈
No → (𝑞 =
(𝑋 +s 𝑚) → 𝑞 ∈ No
)) |
89 | 87, 88 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (𝑞 = (𝑋 +s 𝑚) → 𝑞 ∈ No
)) |
90 | 89 | rexlimdva 3153 |
. . . 4
⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) → 𝑞 ∈ No
)) |
91 | 90 | abssdv 4026 |
. . 3
⊢ (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ⊆ No
) |
92 | 55, 91 | unssd 4147 |
. 2
⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ⊆ No
) |
93 | 15 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
94 | | rightssno 27214 |
. . . . . . . . . 10
⊢ ( R
‘𝑋) ⊆ No |
95 | 94 | sseli 3941 |
. . . . . . . . 9
⊢ (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ No
) |
96 | 95 | adantl 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 𝑟 ∈ No
) |
97 | 20 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 𝑌 ∈ No
) |
98 | 22 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 0s ∈ No ) |
99 | 24 | oveq2i 7369 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑟) +no ( bday
‘ 0s )) = (( bday
‘𝑟) +no
∅) |
100 | | bdayelon 27119 |
. . . . . . . . . . . . 13
⊢ ( bday ‘𝑟) ∈ On |
101 | | naddid1 8630 |
. . . . . . . . . . . . 13
⊢ (( bday ‘𝑟) ∈ On → ((
bday ‘𝑟) +no
∅) = ( bday ‘𝑟)) |
102 | 100, 101 | ax-mp 5 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑟) +no ∅) = ( bday
‘𝑟) |
103 | 99, 102 | eqtri 2765 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑟) +no ( bday
‘ 0s )) = ( bday
‘𝑟) |
104 | 103 | uneq2i 4121 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑟) +no ( bday
‘ 0s ))) = ((( bday
‘𝑟) +no ( bday ‘𝑌)) ∪ ( bday
‘𝑟)) |
105 | | naddword1 8637 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑌)
∈ On) → ( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑌))) |
106 | 100, 31, 105 | mp2an 691 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑌)) |
107 | | ssequn2 4144 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑌)) ↔ ((( bday
‘𝑟) +no ( bday ‘𝑌)) ∪ ( bday
‘𝑟)) = (( bday ‘𝑟) +no ( bday
‘𝑌))) |
108 | 106, 107 | mpbi 229 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑌)) ∪
( bday ‘𝑟)) = (( bday
‘𝑟) +no ( bday ‘𝑌)) |
109 | 104, 108 | eqtri 2765 |
. . . . . . . . 9
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑟) +no ( bday
‘ 0s ))) = (( bday
‘𝑟) +no ( bday ‘𝑌)) |
110 | | rightssold 27212 |
. . . . . . . . . . . . . 14
⊢ ( R
‘𝑋) ⊆ ( O
‘( bday ‘𝑋)) |
111 | 110 | sseli 3941 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ ( O ‘(
bday ‘𝑋))) |
112 | | oldbday 27233 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑟 ∈ No )
→ (𝑟 ∈ ( O
‘( bday ‘𝑋)) ↔ ( bday
‘𝑟) ∈
( bday ‘𝑋))) |
113 | 39, 95, 112 | sylancr 588 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ( R ‘𝑋) → (𝑟 ∈ ( O ‘(
bday ‘𝑋))
↔ ( bday ‘𝑟) ∈ ( bday
‘𝑋))) |
114 | 111, 113 | mpbid 231 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ( R ‘𝑋) → (
bday ‘𝑟)
∈ ( bday ‘𝑋)) |
115 | | naddel1 8633 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑋)
∈ On ∧ ( bday ‘𝑌) ∈ On) → ((
bday ‘𝑟)
∈ ( bday ‘𝑋) ↔ (( bday
‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌)))) |
116 | 100, 39, 31, 115 | mp3an 1462 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑟) ∈ ( bday
‘𝑋) ↔
(( bday ‘𝑟) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
117 | 114, 116 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ( R ‘𝑋) → (( bday ‘𝑟) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
118 | 117 | adantl 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (( bday
‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
119 | | elun1 4137 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
(( bday ‘𝑟) +no ( bday
‘𝑌)) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
120 | 118, 119 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (( bday
‘𝑟) +no ( bday ‘𝑌)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
121 | 109, 120 | eqeltrid 2842 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → ((( bday
‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
122 | 93, 96, 97, 98, 121 | addsproplem1 27284 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → ((𝑟 +s 𝑌) ∈ No
∧ (𝑌 <s
0s → (𝑌
+s 𝑟) <s (
0s +s 𝑟)))) |
123 | 122 | simpld 496 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (𝑟 +s 𝑌) ∈ No
) |
124 | | eleq1a 2833 |
. . . . . 6
⊢ ((𝑟 +s 𝑌) ∈ No
→ (𝑤 = (𝑟 +s 𝑌) → 𝑤 ∈ No
)) |
125 | 123, 124 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (𝑤 = (𝑟 +s 𝑌) → 𝑤 ∈ No
)) |
126 | 125 | rexlimdva 3153 |
. . . 4
⊢ (𝜑 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) → 𝑤 ∈ No
)) |
127 | 126 | abssdv 4026 |
. . 3
⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ⊆ No
) |
128 | 15 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
129 | 57 | adantr 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 𝑋 ∈ No
) |
130 | | rightssno 27214 |
. . . . . . . . . 10
⊢ ( R
‘𝑌) ⊆ No |
131 | 130 | sseli 3941 |
. . . . . . . . 9
⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ No
) |
132 | 131 | adantl 483 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 𝑠 ∈ No
) |
133 | 22 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 0s ∈ No ) |
134 | 66 | uneq2i 4121 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑠)) ∪
(( bday ‘𝑋) +no ( bday
‘ 0s ))) = ((( bday
‘𝑋) +no ( bday ‘𝑠)) ∪ ( bday
‘𝑋)) |
135 | | bdayelon 27119 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝑠) ∈ On |
136 | | naddword1 8637 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑠)
∈ On) → ( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑠))) |
137 | 39, 135, 136 | mp2an 691 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑠)) |
138 | | ssequn2 4144 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑠)) ↔ ((( bday
‘𝑋) +no ( bday ‘𝑠)) ∪ ( bday
‘𝑋)) = (( bday ‘𝑋) +no ( bday
‘𝑠))) |
139 | 137, 138 | mpbi 229 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑠)) ∪
( bday ‘𝑋)) = (( bday
‘𝑋) +no ( bday ‘𝑠)) |
140 | 134, 139 | eqtri 2765 |
. . . . . . . . 9
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑠)) ∪
(( bday ‘𝑋) +no ( bday
‘ 0s ))) = (( bday
‘𝑋) +no ( bday ‘𝑠)) |
141 | | rightssold 27212 |
. . . . . . . . . . . . . 14
⊢ ( R
‘𝑌) ⊆ ( O
‘( bday ‘𝑌)) |
142 | 141 | sseli 3941 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ ( O ‘(
bday ‘𝑌))) |
143 | | oldbday 27233 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑌) ∈ On ∧ 𝑠 ∈ No )
→ (𝑠 ∈ ( O
‘( bday ‘𝑌)) ↔ ( bday
‘𝑠) ∈
( bday ‘𝑌))) |
144 | 31, 131, 143 | sylancr 588 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ( R ‘𝑌) → (𝑠 ∈ ( O ‘(
bday ‘𝑌))
↔ ( bday ‘𝑠) ∈ ( bday
‘𝑌))) |
145 | 142, 144 | mpbid 231 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ( R ‘𝑌) → (
bday ‘𝑠)
∈ ( bday ‘𝑌)) |
146 | | naddel2 8634 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑠) ∈ On ∧ (
bday ‘𝑌)
∈ On ∧ ( bday ‘𝑋) ∈ On) → ((
bday ‘𝑠)
∈ ( bday ‘𝑌) ↔ (( bday
‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌)))) |
147 | 135, 31, 39, 146 | mp3an 1462 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑠) ∈ ( bday
‘𝑌) ↔
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
148 | 145, 147 | sylib 217 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ ( R ‘𝑌) → (( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
149 | 148 | adantl 483 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (( bday
‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
150 | | elun1 4137 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
151 | 149, 150 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (( bday
‘𝑋) +no ( bday ‘𝑠)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
152 | 140, 151 | eqeltrid 2842 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ((( bday
‘𝑋) +no ( bday ‘𝑠)) ∪ (( bday
‘𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
153 | 128, 129,
132, 133, 152 | addsproplem1 27284 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ((𝑋 +s 𝑠) ∈ No
∧ (𝑠 <s
0s → (𝑠
+s 𝑋) <s (
0s +s 𝑋)))) |
154 | 153 | simpld 496 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (𝑋 +s 𝑠) ∈ No
) |
155 | | eleq1a 2833 |
. . . . . 6
⊢ ((𝑋 +s 𝑠) ∈
No → (𝑡 =
(𝑋 +s 𝑠) → 𝑡 ∈ No
)) |
156 | 154, 155 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (𝑡 = (𝑋 +s 𝑠) → 𝑡 ∈ No
)) |
157 | 156 | rexlimdva 3153 |
. . . 4
⊢ (𝜑 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) → 𝑡 ∈ No
)) |
158 | 157 | abssdv 4026 |
. . 3
⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ⊆ No
) |
159 | 127, 158 | unssd 4147 |
. 2
⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ⊆ No
) |
160 | | elun 4109 |
. . . . . . 7
⊢ (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)})) |
161 | | vex 3450 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
162 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑎 → (𝑝 = (𝑙 +s 𝑌) ↔ 𝑎 = (𝑙 +s 𝑌))) |
163 | 162 | rexbidv 3176 |
. . . . . . . . 9
⊢ (𝑝 = 𝑎 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌))) |
164 | 161, 163 | elab 3631 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌)) |
165 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑎 → (𝑞 = (𝑋 +s 𝑚) ↔ 𝑎 = (𝑋 +s 𝑚))) |
166 | 165 | rexbidv 3176 |
. . . . . . . . 9
⊢ (𝑞 = 𝑎 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚))) |
167 | 161, 166 | elab 3631 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)) |
168 | 164, 167 | orbi12i 914 |
. . . . . . 7
⊢ ((𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚))) |
169 | 160, 168 | bitri 275 |
. . . . . 6
⊢ (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚))) |
170 | | elun 4109 |
. . . . . . 7
⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) |
171 | | vex 3450 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
172 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝑌) ↔ 𝑏 = (𝑟 +s 𝑌))) |
173 | 172 | rexbidv 3176 |
. . . . . . . . 9
⊢ (𝑤 = 𝑏 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌))) |
174 | 171, 173 | elab 3631 |
. . . . . . . 8
⊢ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) |
175 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑏 → (𝑡 = (𝑋 +s 𝑠) ↔ 𝑏 = (𝑋 +s 𝑠))) |
176 | 175 | rexbidv 3176 |
. . . . . . . . 9
⊢ (𝑡 = 𝑏 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) |
177 | 171, 176 | elab 3631 |
. . . . . . . 8
⊢ (𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) |
178 | 174, 177 | orbi12i 914 |
. . . . . . 7
⊢ ((𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) |
179 | 170, 178 | bitri 275 |
. . . . . 6
⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) |
180 | 169, 179 | anbi12i 628 |
. . . . 5
⊢ ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) ↔ ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)) ∧ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))) |
181 | | anddi 1010 |
. . . . 5
⊢
(((∃𝑙 ∈ (
L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∨ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)) ∧ (∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌) ∨ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) ↔ (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) ∨ ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))))) |
182 | 180, 181 | bitri 275 |
. . . 4
⊢ ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) ↔ (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) ∨ ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))))) |
183 | | reeanv 3218 |
. . . . . . 7
⊢
(∃𝑙 ∈ ( L
‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌))) |
184 | | lltropt 27205 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈
No → ( L ‘𝑋) <<s ( R ‘𝑋)) |
185 | 57, 184 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ( L ‘𝑋) <<s ( R ‘𝑋)) |
186 | 185 | adantr 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ( L ‘𝑋) <<s ( R ‘𝑋)) |
187 | | simprl 770 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ ( L ‘𝑋)) |
188 | | simprr 772 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ ( R ‘𝑋)) |
189 | 186, 187,
188 | ssltsepcd 27136 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 <s 𝑟) |
190 | 15 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
191 | 20 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 ∈ No
) |
192 | 18 | ad2antrl 727 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ No
) |
193 | 95 | ad2antll 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ No
) |
194 | | naddcom 8629 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑌) ∈ On ∧ (
bday ‘𝑙)
∈ On) → (( bday ‘𝑌) +no ( bday
‘𝑙)) = (( bday ‘𝑙) +no ( bday
‘𝑌))) |
195 | 31, 26, 194 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑌) +no ( bday
‘𝑙)) = (( bday ‘𝑙) +no ( bday
‘𝑌)) |
196 | 45 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
197 | 195, 196 | eqeltrid 2842 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑌) +no ( bday ‘𝑙)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
198 | | naddcom 8629 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑌) ∈ On ∧ (
bday ‘𝑟)
∈ On) → (( bday ‘𝑌) +no ( bday
‘𝑟)) = (( bday ‘𝑟) +no ( bday
‘𝑌))) |
199 | 31, 100, 198 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑌) +no ( bday
‘𝑟)) = (( bday ‘𝑟) +no ( bday
‘𝑌)) |
200 | 117 | ad2antll 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
201 | 199, 200 | eqeltrid 2842 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑌) +no ( bday ‘𝑟)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
202 | | naddcl 8624 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑌) ∈ On ∧ (
bday ‘𝑙)
∈ On) → (( bday ‘𝑌) +no ( bday
‘𝑙)) ∈
On) |
203 | 31, 26, 202 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑌) +no ( bday
‘𝑙)) ∈
On |
204 | | naddcl 8624 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑌) ∈ On ∧ (
bday ‘𝑟)
∈ On) → (( bday ‘𝑌) +no ( bday
‘𝑟)) ∈
On) |
205 | 31, 100, 204 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑌) +no ( bday
‘𝑟)) ∈
On |
206 | | naddcl 8624 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑌)
∈ On) → (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On) |
207 | 39, 31, 206 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On |
208 | | onunel 6423 |
. . . . . . . . . . . . . . 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
‘𝑌))))) |
209 | 203, 205,
207, 208 | mp3an 1462 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑌) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑌) +no ( bday
‘𝑟))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑌) +no ( bday
‘𝑙)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑌) +no ( bday
‘𝑟)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
210 | 197, 201,
209 | sylanbrc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday
‘𝑌) +no ( bday ‘𝑟))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
211 | | elun1 4137 |
. . . . . . . . . . . . 13
⊢ (((( bday ‘𝑌) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑌) +no ( bday
‘𝑟))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑌) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑌) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
212 | 210, 211 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday
‘𝑌) +no ( bday ‘𝑟))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
213 | 190, 191,
192, 193, 212 | addsproplem1 27284 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑌 +s 𝑙) ∈ No
∧ (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)))) |
214 | 213 | simprd 497 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))) |
215 | 189, 214 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)) |
216 | | breq12 5111 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))) |
217 | 215, 216 | syl5ibrcom 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
218 | 217 | rexlimdvva 3206 |
. . . . . . 7
⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
219 | 183, 218 | biimtrrid 242 |
. . . . . 6
⊢ (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
220 | | reeanv 3218 |
. . . . . . 7
⊢
(∃𝑙 ∈ ( L
‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) |
221 | 51 | adantrr 716 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) ∈ No
) |
222 | 15 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
223 | 18 | ad2antrl 727 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 ∈ No
) |
224 | 131 | ad2antll 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ No
) |
225 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 0s ∈ No ) |
226 | 29 | uneq2i 4121 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑠)) ∪
(( bday ‘𝑙) +no ( bday
‘ 0s ))) = ((( bday
‘𝑙) +no ( bday ‘𝑠)) ∪ ( bday
‘𝑙)) |
227 | | naddword1 8637 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑠)
∈ On) → ( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑠))) |
228 | 26, 135, 227 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢ ( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑠)) |
229 | | ssequn2 4144 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑠)) ↔ ((( bday
‘𝑙) +no ( bday ‘𝑠)) ∪ ( bday
‘𝑙)) = (( bday ‘𝑙) +no ( bday
‘𝑠))) |
230 | 228, 229 | mpbi 229 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑠)) ∪
( bday ‘𝑙)) = (( bday
‘𝑙) +no ( bday ‘𝑠)) |
231 | 226, 230 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑠)) ∪
(( bday ‘𝑙) +no ( bday
‘ 0s ))) = (( bday
‘𝑙) +no ( bday ‘𝑠)) |
232 | | naddel1 8633 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑋)
∈ On ∧ ( bday ‘𝑠) ∈ On) → ((
bday ‘𝑙)
∈ ( bday ‘𝑋) ↔ (( bday
‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑠)))) |
233 | 26, 39, 135, 232 | mp3an 1462 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑙) ∈ ( bday
‘𝑋) ↔
(( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑠))) |
234 | 42, 233 | sylib 217 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ ( L ‘𝑋) → (( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑠))) |
235 | 234 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑠))) |
236 | 148 | ad2antll 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
237 | | 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
‘𝑌)))) |
238 | 207, 237 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∧
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
(( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
239 | 235, 236,
238 | syl2anc 585 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
240 | | elun1 4137 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
(( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
241 | 239, 240 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑙) +no ( bday ‘𝑠)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
242 | 231, 241 | eqeltrid 2842 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑙) +no ( bday ‘𝑠)) ∪ (( bday
‘𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
243 | 222, 223,
224, 225, 242 | addsproplem1 27284 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑠) ∈ No
∧ (𝑠 <s
0s → (𝑠
+s 𝑙) <s (
0s +s 𝑙)))) |
244 | 243 | simpld 496 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) ∈ No
) |
245 | 154 | adantrl 715 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) ∈ No
) |
246 | | rightval 27197 |
. . . . . . . . . . . . . . 15
⊢ ( R
‘𝑌) = {𝑠 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑌 <s 𝑠} |
247 | 246 | reqabi 3430 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ( R ‘𝑌) ↔ (𝑠 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑌 <s 𝑠)) |
248 | 247 | simprbi 498 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑌 <s 𝑠) |
249 | 248 | ad2antll 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 <s 𝑠) |
250 | 20 | adantr 482 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 ∈ No
) |
251 | 45 | ad2antrl 727 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
252 | | naddcl 8624 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑌)
∈ On) → (( bday ‘𝑙) +no (
bday ‘𝑌))
∈ On) |
253 | 26, 31, 252 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑙) +no ( bday
‘𝑌)) ∈
On |
254 | | naddcl 8624 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑠)
∈ On) → (( bday ‘𝑙) +no (
bday ‘𝑠))
∈ On) |
255 | 26, 135, 254 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
On |
256 | | onunel 6423 |
. . . . . . . . . . . . . . . . 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
‘𝑌))))) |
257 | 253, 255,
207, 256 | mp3an 1462 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑙) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑙) +no ( bday
‘𝑠))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑙) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
258 | 251, 239,
257 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑙) +no ( bday ‘𝑠))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
259 | | elun1 4137 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑙) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑙) +no ( bday
‘𝑠))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑙) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑙) +no ( bday
‘𝑠))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
260 | 258, 259 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑙) +no ( bday ‘𝑠))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
261 | 222, 223,
250, 224, 260 | addsproplem1 27284 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑌) ∈ No
∧ (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙)))) |
262 | 261 | simprd 497 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙))) |
263 | 249, 262 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙)) |
264 | 223, 250 | addscomd 27282 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) = (𝑌 +s 𝑙)) |
265 | 223, 224 | addscomd 27282 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) = (𝑠 +s 𝑙)) |
266 | 263, 264,
265 | 3brtr4d 5138 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑙 +s 𝑠)) |
267 | | leftval 27196 |
. . . . . . . . . . . . . 14
⊢ ( L
‘𝑋) = {𝑙 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑙 <s 𝑋} |
268 | 267 | reqabi 3430 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ( L ‘𝑋) ↔ (𝑙 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑙 <s 𝑋)) |
269 | 268 | simprbi 498 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 <s 𝑋) |
270 | 269 | ad2antrl 727 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 <s 𝑋) |
271 | 57 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 ∈ No
) |
272 | | naddcom 8629 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑠) ∈ On ∧ (
bday ‘𝑙)
∈ On) → (( bday ‘𝑠) +no (
bday ‘𝑙)) =
(( bday ‘𝑙) +no ( bday
‘𝑠))) |
273 | 135, 26, 272 | mp2an 691 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑠) +no ( bday
‘𝑙)) = (( bday ‘𝑙) +no ( bday
‘𝑠)) |
274 | 273, 239 | eqeltrid 2842 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑠) +no ( bday ‘𝑙)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
275 | | naddcom 8629 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑠) ∈ On ∧ (
bday ‘𝑋)
∈ On) → (( bday ‘𝑠) +no (
bday ‘𝑋)) =
(( bday ‘𝑋) +no ( bday
‘𝑠))) |
276 | 135, 39, 275 | mp2an 691 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑠) +no ( bday
‘𝑋)) = (( bday ‘𝑋) +no ( bday
‘𝑠)) |
277 | 276, 236 | eqeltrid 2842 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑠) +no ( bday ‘𝑋)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
278 | | naddcl 8624 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑠) ∈ On ∧ (
bday ‘𝑙)
∈ On) → (( bday ‘𝑠) +no (
bday ‘𝑙))
∈ On) |
279 | 135, 26, 278 | mp2an 691 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑠) +no ( bday
‘𝑙)) ∈
On |
280 | | naddcl 8624 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑠) ∈ On ∧ (
bday ‘𝑋)
∈ On) → (( bday ‘𝑠) +no (
bday ‘𝑋))
∈ On) |
281 | 135, 39, 280 | mp2an 691 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑠) +no ( bday
‘𝑋)) ∈
On |
282 | | onunel 6423 |
. . . . . . . . . . . . . . . 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
‘𝑌))))) |
283 | 279, 281,
207, 282 | mp3an 1462 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑠) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑠) +no ( bday
‘𝑋))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑠) +no ( bday
‘𝑙)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑠) +no ( bday
‘𝑋)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
284 | 274, 277,
283 | sylanbrc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday
‘𝑠) +no ( bday ‘𝑋))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
285 | | elun1 4137 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑠) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑠) +no ( bday
‘𝑋))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑠) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑠) +no ( bday
‘𝑋))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
286 | 284, 285 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday
‘𝑠) +no ( bday ‘𝑋))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
287 | 222, 224,
223, 271, 286 | addsproplem1 27284 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑠 +s 𝑙) ∈ No
∧ (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠)))) |
288 | 287 | simprd 497 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠))) |
289 | 270, 288 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠)) |
290 | 221, 244,
245, 266, 289 | slttrd 27110 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑋 +s 𝑠)) |
291 | | breq12 5111 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑋 +s 𝑠))) |
292 | 290, 291 | syl5ibrcom 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
293 | 292 | rexlimdvva 3206 |
. . . . . . 7
⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
294 | 220, 293 | biimtrrid 242 |
. . . . . 6
⊢ (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
295 | 219, 294 | jaod 858 |
. . . . 5
⊢ (𝜑 → (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏)) |
296 | | reeanv 3218 |
. . . . . . 7
⊢
(∃𝑚 ∈ ( L
‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌))) |
297 | 15 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
298 | 57 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 ∈ No
) |
299 | 60 | ad2antrl 727 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ No
) |
300 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 0s ∈ No ) |
301 | 81 | ad2antrl 727 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
302 | 301, 83 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
303 | 73, 302 | eqeltrid 2842 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
304 | 297, 298,
299, 300, 303 | addsproplem1 27284 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑋 +s 𝑚) ∈ No
∧ (𝑚 <s
0s → (𝑚
+s 𝑋) <s (
0s +s 𝑋)))) |
305 | 304 | simpld 496 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) ∈ No
) |
306 | 95 | ad2antll 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ No
) |
307 | 103 | uneq2i 4121 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑟) +no ( bday
‘ 0s ))) = ((( bday
‘𝑟) +no ( bday ‘𝑚)) ∪ ( bday
‘𝑟)) |
308 | | naddword1 8637 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑚)
∈ On) → ( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑚))) |
309 | 100, 68, 308 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢ ( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑚)) |
310 | | ssequn2 4144 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑚)) ↔ ((( bday
‘𝑟) +no ( bday ‘𝑚)) ∪ ( bday
‘𝑟)) = (( bday ‘𝑟) +no ( bday
‘𝑚))) |
311 | 309, 310 | mpbi 229 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
( bday ‘𝑟)) = (( bday
‘𝑟) +no ( bday ‘𝑚)) |
312 | 307, 311 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑟) +no ( bday
‘ 0s ))) = (( bday
‘𝑟) +no ( bday ‘𝑚)) |
313 | | naddel1 8633 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑋)
∈ On ∧ ( bday ‘𝑚) ∈ On) → ((
bday ‘𝑟)
∈ ( bday ‘𝑋) ↔ (( bday
‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑚)))) |
314 | 100, 39, 68, 313 | mp3an 1462 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑟) ∈ ( bday
‘𝑋) ↔
(( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑚))) |
315 | 114, 314 | sylib 217 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ ( R ‘𝑋) → (( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑚))) |
316 | 315 | ad2antll 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑚))) |
317 | | 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
‘𝑌)))) |
318 | 207, 317 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∧
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
(( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
319 | 316, 301,
318 | syl2anc 585 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
320 | | elun1 4137 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
(( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
321 | 319, 320 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑚)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
322 | 312, 321 | eqeltrid 2842 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
323 | 297, 306,
299, 300, 322 | addsproplem1 27284 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No
∧ (𝑚 <s
0s → (𝑚
+s 𝑟) <s (
0s +s 𝑟)))) |
324 | 323 | simpld 496 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) ∈ No
) |
325 | 20 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 ∈ No
) |
326 | 117 | ad2antll 728 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
327 | 326, 119 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑌)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
328 | 109, 327 | eqeltrid 2842 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
329 | 297, 306,
325, 300, 328 | addsproplem1 27284 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑌) ∈ No
∧ (𝑌 <s
0s → (𝑌
+s 𝑟) <s (
0s +s 𝑟)))) |
330 | 329 | simpld 496 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) ∈ No
) |
331 | | rightval 27197 |
. . . . . . . . . . . . . . . 16
⊢ ( R
‘𝑋) = {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟} |
332 | 331 | eleq2i 2830 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ ( R ‘𝑋) ↔ 𝑟 ∈ {𝑟 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑟}) |
333 | 332 | biimpi 215 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ {𝑟 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑟}) |
334 | 333 | ad2antll 728 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ {𝑟 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑟}) |
335 | | rabid 3428 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ {𝑟 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑟} ↔ (𝑟 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑋 <s 𝑟)) |
336 | 334, 335 | sylib 217 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑋 <s 𝑟)) |
337 | 336 | simprd 497 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 <s 𝑟) |
338 | | naddcom 8629 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑋)
∈ On) → (( bday ‘𝑚) +no (
bday ‘𝑋)) =
(( bday ‘𝑋) +no ( bday
‘𝑚))) |
339 | 68, 39, 338 | mp2an 691 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑚) +no ( bday
‘𝑋)) = (( bday ‘𝑋) +no ( bday
‘𝑚)) |
340 | 339, 301 | eqeltrid 2842 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑚) +no ( bday ‘𝑋)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
341 | | naddcom 8629 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑟)
∈ On) → (( bday ‘𝑚) +no (
bday ‘𝑟)) =
(( bday ‘𝑟) +no ( bday
‘𝑚))) |
342 | 68, 100, 341 | mp2an 691 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑚) +no ( bday
‘𝑟)) = (( bday ‘𝑟) +no ( bday
‘𝑚)) |
343 | 342, 319 | eqeltrid 2842 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑚) +no ( bday ‘𝑟)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
344 | | naddcl 8624 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑋)
∈ On) → (( bday ‘𝑚) +no (
bday ‘𝑋))
∈ On) |
345 | 68, 39, 344 | mp2an 691 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑚) +no ( bday
‘𝑋)) ∈
On |
346 | | naddcl 8624 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑟)
∈ On) → (( bday ‘𝑚) +no (
bday ‘𝑟))
∈ On) |
347 | 68, 100, 346 | mp2an 691 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑚) +no ( bday
‘𝑟)) ∈
On |
348 | | onunel 6423 |
. . . . . . . . . . . . . . . 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
‘𝑌))))) |
349 | 345, 347,
207, 348 | mp3an 1462 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑚) +no ( bday
‘𝑋)) ∪
(( bday ‘𝑚) +no ( bday
‘𝑟))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑚) +no ( bday
‘𝑋)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑚) +no ( bday
‘𝑟)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
350 | 340, 343,
349 | sylanbrc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday
‘𝑚) +no ( bday ‘𝑟))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
351 | | elun1 4137 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑚) +no ( bday
‘𝑋)) ∪
(( bday ‘𝑚) +no ( bday
‘𝑟))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑚) +no ( bday
‘𝑋)) ∪
(( bday ‘𝑚) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
352 | 350, 351 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday
‘𝑚) +no ( bday ‘𝑟))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
353 | 297, 299,
298, 306, 352 | addsproplem1 27284 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑚 +s 𝑋) ∈ No
∧ (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚)))) |
354 | 353 | simprd 497 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚))) |
355 | 337, 354 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚)) |
356 | | leftval 27196 |
. . . . . . . . . . . . . . . . 17
⊢ ( L
‘𝑌) = {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌} |
357 | 356 | eleq2i 2830 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ( L ‘𝑌) ↔ 𝑚 ∈ {𝑚 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑚 <s 𝑌}) |
358 | 357 | biimpi 215 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ {𝑚 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑚 <s 𝑌}) |
359 | 358 | ad2antrl 727 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ {𝑚 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑚 <s 𝑌}) |
360 | | rabid 3428 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ {𝑚 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑚 <s 𝑌} ↔ (𝑚 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑚 <s 𝑌)) |
361 | 359, 360 | sylib 217 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑚 <s 𝑌)) |
362 | 361 | simprd 497 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 <s 𝑌) |
363 | | naddcl 8624 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑚)
∈ On) → (( bday ‘𝑟) +no (
bday ‘𝑚))
∈ On) |
364 | 100, 68, 363 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
On |
365 | | naddcl 8624 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑌)
∈ On) → (( bday ‘𝑟) +no (
bday ‘𝑌))
∈ On) |
366 | 100, 31, 365 | mp2an 691 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑟) +no ( bday
‘𝑌)) ∈
On |
367 | | onunel 6423 |
. . . . . . . . . . . . . . . . 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
‘𝑌))))) |
368 | 364, 366,
207, 367 | mp3an 1462 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑟) +no ( bday
‘𝑌))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑟) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
369 | 319, 326,
368 | sylanbrc 584 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑟) +no ( bday ‘𝑌))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
370 | | elun1 4137 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑟) +no ( bday
‘𝑌))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑟) +no ( bday
‘𝑌))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
371 | 369, 370 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑟) +no ( bday ‘𝑌))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
372 | 297, 306,
299, 325, 371 | addsproplem1 27284 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No
∧ (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟)))) |
373 | 372 | simprd 497 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟))) |
374 | 362, 373 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟)) |
375 | 306, 299 | addscomd 27282 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) = (𝑚 +s 𝑟)) |
376 | 306, 325 | addscomd 27282 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) = (𝑌 +s 𝑟)) |
377 | 374, 375,
376 | 3brtr4d 5138 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) <s (𝑟 +s 𝑌)) |
378 | 305, 324,
330, 355, 377 | slttrd 27110 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑌)) |
379 | | breq12 5111 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑟 +s 𝑌))) |
380 | 378, 379 | syl5ibrcom 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
381 | 380 | rexlimdvva 3206 |
. . . . . . 7
⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
382 | 296, 381 | biimtrrid 242 |
. . . . . 6
⊢ (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
383 | | reeanv 3218 |
. . . . . . 7
⊢
(∃𝑚 ∈ ( L
‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) |
384 | | lltropt 27205 |
. . . . . . . . . . . . . 14
⊢ (𝑌 ∈
No → ( L ‘𝑌) <<s ( R ‘𝑌)) |
385 | 20, 384 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → ( L ‘𝑌) <<s ( R ‘𝑌)) |
386 | 385 | adantr 482 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ( L ‘𝑌) <<s ( R ‘𝑌)) |
387 | | simprl 770 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ ( L ‘𝑌)) |
388 | | simprr 772 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ ( R ‘𝑌)) |
389 | 386, 387,
388 | ssltsepcd 27136 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 <s 𝑠) |
390 | 15 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
391 | 57 | adantr 482 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 ∈ No
) |
392 | 60 | ad2antrl 727 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ No
) |
393 | 131 | ad2antll 728 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ No
) |
394 | 81 | ad2antrl 727 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
395 | 148 | ad2antll 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
396 | | naddcl 8624 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑚)
∈ On) → (( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
On) |
397 | 39, 68, 396 | mp2an 691 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
On |
398 | | naddcl 8624 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑠)
∈ On) → (( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
On) |
399 | 39, 135, 398 | mp2an 691 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
On |
400 | | onunel 6423 |
. . . . . . . . . . . . . . . 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
‘𝑌))))) |
401 | 397, 399,
207, 400 | mp3an 1462 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑠))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
402 | 394, 395,
401 | sylanbrc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑠))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
403 | | elun1 4137 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑠))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑠))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
404 | 402, 403 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑠))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
405 | 390, 391,
392, 393, 404 | addsproplem1 27284 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑋 +s 𝑚) ∈ No
∧ (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋)))) |
406 | 405 | simprd 497 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋))) |
407 | 389, 406 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋)) |
408 | 391, 392 | addscomd 27282 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) = (𝑚 +s 𝑋)) |
409 | 391, 393 | addscomd 27282 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) = (𝑠 +s 𝑋)) |
410 | 407, 408,
409 | 3brtr4d 5138 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) <s (𝑋 +s 𝑠)) |
411 | | breq12 5111 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑋 +s 𝑠))) |
412 | 410, 411 | syl5ibrcom 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
413 | 412 | rexlimdvva 3206 |
. . . . . . 7
⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
414 | 383, 413 | biimtrrid 242 |
. . . . . 6
⊢ (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
415 | 382, 414 | jaod 858 |
. . . . 5
⊢ (𝜑 → (((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏)) |
416 | 295, 415 | jaod 858 |
. . . 4
⊢ (𝜑 → ((((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) ∨ ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))) → 𝑎 <s 𝑏)) |
417 | 182, 416 | biimtrid 241 |
. . 3
⊢ (𝜑 → ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) → 𝑎 <s 𝑏)) |
418 | 417 | 3impib 1117 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) → 𝑎 <s 𝑏) |
419 | 7, 14, 92, 159, 418 | ssltd 27134 |
1
⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) |