| Step | Hyp | Ref
| Expression |
| 1 | | fvex 6919 |
. . . . 5
⊢ ( L
‘𝑋) ∈
V |
| 2 | 1 | abrexex 7987 |
. . . 4
⊢ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V |
| 3 | 2 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∈ V) |
| 4 | | fvex 6919 |
. . . . 5
⊢ ( L
‘𝑌) ∈
V |
| 5 | 4 | abrexex 7987 |
. . . 4
⊢ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V |
| 6 | 5 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ∈ V) |
| 7 | 3, 6 | unexd 7774 |
. 2
⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∈ V) |
| 8 | | fvex 6919 |
. . . . 5
⊢ ( R
‘𝑋) ∈
V |
| 9 | 8 | abrexex 7987 |
. . . 4
⊢ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V |
| 10 | 9 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∈ V) |
| 11 | | fvex 6919 |
. . . . 5
⊢ ( R
‘𝑌) ∈
V |
| 12 | 11 | abrexex 7987 |
. . . 4
⊢ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V |
| 13 | 12 | a1i 11 |
. . 3
⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ∈ V) |
| 14 | 10, 13 | unexd 7774 |
. 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 480 |
. . . . . . . 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 27919 |
. . . . . . . . . 10
⊢ ( L
‘𝑋) ⊆ No |
| 18 | 17 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ No
) |
| 19 | 18 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 𝑙 ∈ No
) |
| 20 | | addsproplem2.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ No
) |
| 21 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 𝑌 ∈ No
) |
| 22 | | 0sno 27871 |
. . . . . . . . 9
⊢
0s ∈ No |
| 23 | 22 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → 0s ∈ No ) |
| 24 | | bday0s 27873 |
. . . . . . . . . . . . 13
⊢ ( bday ‘ 0s ) = ∅ |
| 25 | 24 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑙) +no ( bday
‘ 0s )) = (( bday
‘𝑙) +no
∅) |
| 26 | | bdayelon 27821 |
. . . . . . . . . . . . 13
⊢ ( bday ‘𝑙) ∈ On |
| 27 | | naddrid 8721 |
. . . . . . . . . . . . 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 4165 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑙) +no ( bday
‘ 0s ))) = ((( bday
‘𝑙) +no ( bday ‘𝑌)) ∪ ( bday
‘𝑙)) |
| 31 | | bdayelon 27821 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝑌) ∈ On |
| 32 | | naddword1 8729 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑌)
∈ On) → ( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑌))) |
| 33 | 26, 31, 32 | mp2an 692 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑌)) |
| 34 | | ssequn2 4189 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑌)) ↔ ((( bday
‘𝑙) +no ( bday ‘𝑌)) ∪ ( bday
‘𝑙)) = (( bday ‘𝑙) +no ( bday
‘𝑌))) |
| 35 | 33, 34 | mpbi 230 |
. . . . . . . . . 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 27917 |
. . . . . . . . . . . . . 14
⊢ ( L
‘𝑋) ⊆ ( O
‘( bday ‘𝑋)) |
| 38 | 37 | sseli 3979 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 ∈ ( O ‘(
bday ‘𝑋))) |
| 39 | | bdayelon 27821 |
. . . . . . . . . . . . . 14
⊢ ( bday ‘𝑋) ∈ On |
| 40 | | oldbday 27939 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑙 ∈ No )
→ (𝑙 ∈ ( O
‘( bday ‘𝑋)) ↔ ( bday
‘𝑙) ∈
( bday ‘𝑋))) |
| 41 | 39, 18, 40 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ( L ‘𝑋) → (𝑙 ∈ ( O ‘(
bday ‘𝑋))
↔ ( bday ‘𝑙) ∈ ( bday
‘𝑋))) |
| 42 | 38, 41 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ ( L ‘𝑋) → (
bday ‘𝑙)
∈ ( bday ‘𝑋)) |
| 43 | | naddel1 8725 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑋)
∈ On ∧ ( bday ‘𝑌) ∈ On) → ((
bday ‘𝑙)
∈ ( bday ‘𝑋) ↔ (( bday
‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌)))) |
| 44 | 26, 39, 31, 43 | mp3an 1463 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑙) ∈ ( bday
‘𝑋) ↔
(( bday ‘𝑙) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
| 45 | 42, 44 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝑙 ∈ ( L ‘𝑋) → (( bday ‘𝑙) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
| 46 | 45 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (( bday
‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 47 | | elun1 4182 |
. . . . . . . . . 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 2845 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → ((( bday
‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 50 | 16, 19, 21, 23, 49 | addsproplem1 28002 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → ((𝑙 +s 𝑌) ∈ No
∧ (𝑌 <s
0s → (𝑌
+s 𝑙) <s (
0s +s 𝑙)))) |
| 51 | 50 | simpld 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (𝑙 +s 𝑌) ∈ No
) |
| 52 | | eleq1a 2836 |
. . . . . 6
⊢ ((𝑙 +s 𝑌) ∈ No
→ (𝑝 = (𝑙 +s 𝑌) → 𝑝 ∈ No
)) |
| 53 | 51, 52 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑙 ∈ ( L ‘𝑋)) → (𝑝 = (𝑙 +s 𝑌) → 𝑝 ∈ No
)) |
| 54 | 53 | rexlimdva 3155 |
. . . 4
⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) → 𝑝 ∈ No
)) |
| 55 | 54 | abssdv 4068 |
. . 3
⊢ (𝜑 → {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ⊆ No
) |
| 56 | 15 | adantr 480 |
. . . . . . . 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 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 𝑋 ∈ No
) |
| 59 | | leftssno 27919 |
. . . . . . . . . 10
⊢ ( L
‘𝑌) ⊆ No |
| 60 | 59 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ No
) |
| 61 | 60 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 𝑚 ∈ No
) |
| 62 | 22 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → 0s ∈ No ) |
| 63 | 24 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑋) +no ( bday
‘ 0s )) = (( bday
‘𝑋) +no
∅) |
| 64 | | naddrid 8721 |
. . . . . . . . . . . . 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 4165 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘ 0s ))) = ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ ( bday
‘𝑋)) |
| 68 | | bdayelon 27821 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝑚) ∈ On |
| 69 | | naddword1 8729 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑚)
∈ On) → ( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑚))) |
| 70 | 39, 68, 69 | mp2an 692 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑚)) |
| 71 | | ssequn2 4189 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑚)) ↔ ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ ( bday
‘𝑋)) = (( bday ‘𝑋) +no ( bday
‘𝑚))) |
| 72 | 70, 71 | mpbi 230 |
. . . . . . . . . 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 27917 |
. . . . . . . . . . . . . 14
⊢ ( L
‘𝑌) ⊆ ( O
‘( bday ‘𝑌)) |
| 75 | 74 | sseli 3979 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ ( O ‘(
bday ‘𝑌))) |
| 76 | | oldbday 27939 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑌) ∈ On ∧ 𝑚 ∈ No )
→ (𝑚 ∈ ( O
‘( bday ‘𝑌)) ↔ ( bday
‘𝑚) ∈
( bday ‘𝑌))) |
| 77 | 31, 60, 76 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ ( L ‘𝑌) → (𝑚 ∈ ( O ‘(
bday ‘𝑌))
↔ ( bday ‘𝑚) ∈ ( bday
‘𝑌))) |
| 78 | 75, 77 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈ ( L ‘𝑌) → (
bday ‘𝑚)
∈ ( bday ‘𝑌)) |
| 79 | | naddel2 8726 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑌)
∈ On ∧ ( bday ‘𝑋) ∈ On) → ((
bday ‘𝑚)
∈ ( bday ‘𝑌) ↔ (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌)))) |
| 80 | 68, 31, 39, 79 | mp3an 1463 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ↔
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
| 81 | 78, 80 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ( L ‘𝑌) → (( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
| 82 | 81 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 83 | | elun1 4182 |
. . . . . . . . . 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 2845 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 86 | 56, 58, 61, 62, 85 | addsproplem1 28002 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → ((𝑋 +s 𝑚) ∈ No
∧ (𝑚 <s
0s → (𝑚
+s 𝑋) <s (
0s +s 𝑋)))) |
| 87 | 86 | simpld 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (𝑋 +s 𝑚) ∈ No
) |
| 88 | | eleq1a 2836 |
. . . . . 6
⊢ ((𝑋 +s 𝑚) ∈
No → (𝑞 =
(𝑋 +s 𝑚) → 𝑞 ∈ No
)) |
| 89 | 87, 88 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ( L ‘𝑌)) → (𝑞 = (𝑋 +s 𝑚) → 𝑞 ∈ No
)) |
| 90 | 89 | rexlimdva 3155 |
. . . 4
⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) → 𝑞 ∈ No
)) |
| 91 | 90 | abssdv 4068 |
. . 3
⊢ (𝜑 → {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ⊆ No
) |
| 92 | 55, 91 | unssd 4192 |
. 2
⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ⊆ No
) |
| 93 | 15 | adantr 480 |
. . . . . . . 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 27920 |
. . . . . . . . . 10
⊢ ( R
‘𝑋) ⊆ No |
| 95 | 94 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ No
) |
| 96 | 95 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 𝑟 ∈ No
) |
| 97 | 20 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 𝑌 ∈ No
) |
| 98 | 22 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → 0s ∈ No ) |
| 99 | 24 | oveq2i 7442 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑟) +no ( bday
‘ 0s )) = (( bday
‘𝑟) +no
∅) |
| 100 | | bdayelon 27821 |
. . . . . . . . . . . . 13
⊢ ( bday ‘𝑟) ∈ On |
| 101 | | naddrid 8721 |
. . . . . . . . . . . . 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 4165 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑟) +no ( bday
‘ 0s ))) = ((( bday
‘𝑟) +no ( bday ‘𝑌)) ∪ ( bday
‘𝑟)) |
| 105 | | naddword1 8729 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑌)
∈ On) → ( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑌))) |
| 106 | 100, 31, 105 | mp2an 692 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑌)) |
| 107 | | ssequn2 4189 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑌)) ↔ ((( bday
‘𝑟) +no ( bday ‘𝑌)) ∪ ( bday
‘𝑟)) = (( bday ‘𝑟) +no ( bday
‘𝑌))) |
| 108 | 106, 107 | mpbi 230 |
. . . . . . . . . 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 27918 |
. . . . . . . . . . . . . 14
⊢ ( R
‘𝑋) ⊆ ( O
‘( bday ‘𝑋)) |
| 111 | 110 | sseli 3979 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ ( O ‘(
bday ‘𝑋))) |
| 112 | | oldbday 27939 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑋) ∈ On ∧ 𝑟 ∈ No )
→ (𝑟 ∈ ( O
‘( bday ‘𝑋)) ↔ ( bday
‘𝑟) ∈
( bday ‘𝑋))) |
| 113 | 39, 95, 112 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ ( R ‘𝑋) → (𝑟 ∈ ( O ‘(
bday ‘𝑋))
↔ ( bday ‘𝑟) ∈ ( bday
‘𝑋))) |
| 114 | 111, 113 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝑟 ∈ ( R ‘𝑋) → (
bday ‘𝑟)
∈ ( bday ‘𝑋)) |
| 115 | | naddel1 8725 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑋)
∈ On ∧ ( bday ‘𝑌) ∈ On) → ((
bday ‘𝑟)
∈ ( bday ‘𝑋) ↔ (( bday
‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌)))) |
| 116 | 100, 39, 31, 115 | mp3an 1463 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑟) ∈ ( bday
‘𝑋) ↔
(( bday ‘𝑟) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
| 117 | 114, 116 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝑟 ∈ ( R ‘𝑋) → (( bday ‘𝑟) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
| 118 | 117 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (( bday
‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 119 | | elun1 4182 |
. . . . . . . . . 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 2845 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → ((( bday
‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 122 | 93, 96, 97, 98, 121 | addsproplem1 28002 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → ((𝑟 +s 𝑌) ∈ No
∧ (𝑌 <s
0s → (𝑌
+s 𝑟) <s (
0s +s 𝑟)))) |
| 123 | 122 | simpld 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (𝑟 +s 𝑌) ∈ No
) |
| 124 | | eleq1a 2836 |
. . . . . 6
⊢ ((𝑟 +s 𝑌) ∈ No
→ (𝑤 = (𝑟 +s 𝑌) → 𝑤 ∈ No
)) |
| 125 | 123, 124 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑟 ∈ ( R ‘𝑋)) → (𝑤 = (𝑟 +s 𝑌) → 𝑤 ∈ No
)) |
| 126 | 125 | rexlimdva 3155 |
. . . 4
⊢ (𝜑 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) → 𝑤 ∈ No
)) |
| 127 | 126 | abssdv 4068 |
. . 3
⊢ (𝜑 → {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ⊆ No
) |
| 128 | 15 | adantr 480 |
. . . . . . . 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 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 𝑋 ∈ No
) |
| 130 | | rightssno 27920 |
. . . . . . . . . 10
⊢ ( R
‘𝑌) ⊆ No |
| 131 | 130 | sseli 3979 |
. . . . . . . . 9
⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ No
) |
| 132 | 131 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 𝑠 ∈ No
) |
| 133 | 22 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → 0s ∈ No ) |
| 134 | 66 | uneq2i 4165 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑠)) ∪
(( bday ‘𝑋) +no ( bday
‘ 0s ))) = ((( bday
‘𝑋) +no ( bday ‘𝑠)) ∪ ( bday
‘𝑋)) |
| 135 | | bdayelon 27821 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝑠) ∈ On |
| 136 | | naddword1 8729 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑠)
∈ On) → ( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑠))) |
| 137 | 39, 135, 136 | mp2an 692 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑠)) |
| 138 | | ssequn2 4189 |
. . . . . . . . . . 11
⊢ (( bday ‘𝑋) ⊆ (( bday
‘𝑋) +no ( bday ‘𝑠)) ↔ ((( bday
‘𝑋) +no ( bday ‘𝑠)) ∪ ( bday
‘𝑋)) = (( bday ‘𝑋) +no ( bday
‘𝑠))) |
| 139 | 137, 138 | mpbi 230 |
. . . . . . . . . 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 27918 |
. . . . . . . . . . . . . 14
⊢ ( R
‘𝑌) ⊆ ( O
‘( bday ‘𝑌)) |
| 142 | 141 | sseli 3979 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑠 ∈ ( O ‘(
bday ‘𝑌))) |
| 143 | | oldbday 27939 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑌) ∈ On ∧ 𝑠 ∈ No )
→ (𝑠 ∈ ( O
‘( bday ‘𝑌)) ↔ ( bday
‘𝑠) ∈
( bday ‘𝑌))) |
| 144 | 31, 131, 143 | sylancr 587 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ( R ‘𝑌) → (𝑠 ∈ ( O ‘(
bday ‘𝑌))
↔ ( bday ‘𝑠) ∈ ( bday
‘𝑌))) |
| 145 | 142, 144 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (𝑠 ∈ ( R ‘𝑌) → (
bday ‘𝑠)
∈ ( bday ‘𝑌)) |
| 146 | | naddel2 8726 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑠) ∈ On ∧ (
bday ‘𝑌)
∈ On ∧ ( bday ‘𝑋) ∈ On) → ((
bday ‘𝑠)
∈ ( bday ‘𝑌) ↔ (( bday
‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌)))) |
| 147 | 135, 31, 39, 146 | mp3an 1463 |
. . . . . . . . . . . 12
⊢ (( bday ‘𝑠) ∈ ( bday
‘𝑌) ↔
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
| 148 | 145, 147 | sylib 218 |
. . . . . . . . . . 11
⊢ (𝑠 ∈ ( R ‘𝑌) → (( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
| 149 | 148 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (( bday
‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 150 | | elun1 4182 |
. . . . . . . . . 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 2845 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ((( bday
‘𝑋) +no ( bday ‘𝑠)) ∪ (( bday
‘𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 153 | 128, 129,
132, 133, 152 | addsproplem1 28002 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → ((𝑋 +s 𝑠) ∈ No
∧ (𝑠 <s
0s → (𝑠
+s 𝑋) <s (
0s +s 𝑋)))) |
| 154 | 153 | simpld 494 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (𝑋 +s 𝑠) ∈ No
) |
| 155 | | eleq1a 2836 |
. . . . . 6
⊢ ((𝑋 +s 𝑠) ∈
No → (𝑡 =
(𝑋 +s 𝑠) → 𝑡 ∈ No
)) |
| 156 | 154, 155 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑠 ∈ ( R ‘𝑌)) → (𝑡 = (𝑋 +s 𝑠) → 𝑡 ∈ No
)) |
| 157 | 156 | rexlimdva 3155 |
. . . 4
⊢ (𝜑 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) → 𝑡 ∈ No
)) |
| 158 | 157 | abssdv 4068 |
. . 3
⊢ (𝜑 → {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ⊆ No
) |
| 159 | 127, 158 | unssd 4192 |
. 2
⊢ (𝜑 → ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ⊆ No
) |
| 160 | | elun 4153 |
. . . . . . 7
⊢ (𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ↔ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∨ 𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)})) |
| 161 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑎 ∈ V |
| 162 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑎 → (𝑝 = (𝑙 +s 𝑌) ↔ 𝑎 = (𝑙 +s 𝑌))) |
| 163 | 162 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑝 = 𝑎 → (∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌) ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌))) |
| 164 | 161, 163 | elab 3679 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ↔ ∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌)) |
| 165 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑎 → (𝑞 = (𝑋 +s 𝑚) ↔ 𝑎 = (𝑋 +s 𝑚))) |
| 166 | 165 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑞 = 𝑎 → (∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚) ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚))) |
| 167 | 161, 166 | elab 3679 |
. . . . . . . 8
⊢ (𝑎 ∈ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)} ↔ ∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚)) |
| 168 | 164, 167 | orbi12i 915 |
. . . . . . 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 4153 |
. . . . . . 7
⊢ (𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)}) ↔ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∨ 𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) |
| 171 | | vex 3484 |
. . . . . . . . 9
⊢ 𝑏 ∈ V |
| 172 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑤 = 𝑏 → (𝑤 = (𝑟 +s 𝑌) ↔ 𝑏 = (𝑟 +s 𝑌))) |
| 173 | 172 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑤 = 𝑏 → (∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌) ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌))) |
| 174 | 171, 173 | elab 3679 |
. . . . . . . 8
⊢ (𝑏 ∈ {𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ↔ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) |
| 175 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑡 = 𝑏 → (𝑡 = (𝑋 +s 𝑠) ↔ 𝑏 = (𝑋 +s 𝑠))) |
| 176 | 175 | rexbidv 3179 |
. . . . . . . . 9
⊢ (𝑡 = 𝑏 → (∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠) ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) |
| 177 | 171, 176 | elab 3679 |
. . . . . . . 8
⊢ (𝑏 ∈ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)} ↔ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) |
| 178 | 174, 177 | orbi12i 915 |
. . . . . . 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 1013 |
. . . . 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 3229 |
. . . . . . 7
⊢
(∃𝑙 ∈ ( L
‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌))) |
| 184 | | lltropt 27911 |
. . . . . . . . . . . 12
⊢ ( L
‘𝑋) <<s ( R
‘𝑋) |
| 185 | 184 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ( L ‘𝑋) <<s ( R ‘𝑋)) |
| 186 | | simprl 771 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ ( L ‘𝑋)) |
| 187 | | simprr 773 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ ( R ‘𝑋)) |
| 188 | 185, 186,
187 | ssltsepcd 27839 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 <s 𝑟) |
| 189 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
| 190 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 ∈ No
) |
| 191 | 18 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑙 ∈ No
) |
| 192 | 95 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ No
) |
| 193 | | naddcom 8720 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑌) ∈ On ∧ (
bday ‘𝑙)
∈ On) → (( bday ‘𝑌) +no ( bday
‘𝑙)) = (( bday ‘𝑙) +no ( bday
‘𝑌))) |
| 194 | 31, 26, 193 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑌) +no ( bday
‘𝑙)) = (( bday ‘𝑙) +no ( bday
‘𝑌)) |
| 195 | 45 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 196 | 194, 195 | eqeltrid 2845 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑌) +no ( bday ‘𝑙)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 197 | | naddcom 8720 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑌) ∈ On ∧ (
bday ‘𝑟)
∈ On) → (( bday ‘𝑌) +no ( bday
‘𝑟)) = (( bday ‘𝑟) +no ( bday
‘𝑌))) |
| 198 | 31, 100, 197 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑌) +no ( bday
‘𝑟)) = (( bday ‘𝑟) +no ( bday
‘𝑌)) |
| 199 | 117 | ad2antll 729 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 200 | 198, 199 | eqeltrid 2845 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑌) +no ( bday ‘𝑟)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 201 | | naddcl 8715 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑌) ∈ On ∧ (
bday ‘𝑙)
∈ On) → (( bday ‘𝑌) +no ( bday
‘𝑙)) ∈
On) |
| 202 | 31, 26, 201 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑌) +no ( bday
‘𝑙)) ∈
On |
| 203 | | naddcl 8715 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑌) ∈ On ∧ (
bday ‘𝑟)
∈ On) → (( bday ‘𝑌) +no ( bday
‘𝑟)) ∈
On) |
| 204 | 31, 100, 203 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑌) +no ( bday
‘𝑟)) ∈
On |
| 205 | | naddcl 8715 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑌)
∈ On) → (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On) |
| 206 | 39, 31, 205 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On |
| 207 | | onunel 6489 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑌) +no ( bday
‘𝑙)) ∈ On
∧ (( bday ‘𝑌) +no ( bday
‘𝑟)) ∈ On
∧ (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On) → (((( bday ‘𝑌) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑌) +no ( bday
‘𝑟))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑌) +no ( bday
‘𝑙)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑌) +no ( bday
‘𝑟)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))))) |
| 208 | 202, 204,
206, 207 | mp3an 1463 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑌) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑌) +no ( bday
‘𝑟))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑌) +no ( bday
‘𝑙)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑌) +no ( bday
‘𝑟)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
| 209 | 196, 200,
208 | sylanbrc 583 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday
‘𝑌) +no ( bday ‘𝑟))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 210 | | elun1 4182 |
. . . . . . . . . . . . 13
⊢ (((( bday ‘𝑌) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑌) +no ( bday
‘𝑟))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑌) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑌) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 211 | 209, 210 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑌) +no ( bday ‘𝑙)) ∪ (( bday
‘𝑌) +no ( bday ‘𝑟))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
| 212 | 189, 190,
191, 192, 211 | addsproplem1 28002 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑌 +s 𝑙) ∈ No
∧ (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)))) |
| 213 | 212 | simprd 495 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 <s 𝑟 → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))) |
| 214 | 188, 213 | mpd 15 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑙 +s 𝑌) <s (𝑟 +s 𝑌)) |
| 215 | | breq12 5148 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑟 +s 𝑌))) |
| 216 | 214, 215 | syl5ibrcom 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
| 217 | 216 | rexlimdvva 3213 |
. . . . . . 7
⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
| 218 | 183, 217 | biimtrrid 243 |
. . . . . 6
⊢ (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
| 219 | | reeanv 3229 |
. . . . . . 7
⊢
(∃𝑙 ∈ ( L
‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) |
| 220 | 51 | adantrr 717 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) ∈ No
) |
| 221 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
| 222 | 18 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 ∈ No
) |
| 223 | 131 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ No
) |
| 224 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 0s ∈ No ) |
| 225 | 29 | uneq2i 4165 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑠)) ∪
(( bday ‘𝑙) +no ( bday
‘ 0s ))) = ((( bday
‘𝑙) +no ( bday ‘𝑠)) ∪ ( bday
‘𝑙)) |
| 226 | | naddword1 8729 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑠)
∈ On) → ( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑠))) |
| 227 | 26, 135, 226 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ ( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑠)) |
| 228 | | ssequn2 4189 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑙) ⊆ (( bday
‘𝑙) +no ( bday ‘𝑠)) ↔ ((( bday
‘𝑙) +no ( bday ‘𝑠)) ∪ ( bday
‘𝑙)) = (( bday ‘𝑙) +no ( bday
‘𝑠))) |
| 229 | 227, 228 | mpbi 230 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑠)) ∪
( bday ‘𝑙)) = (( bday
‘𝑙) +no ( bday ‘𝑠)) |
| 230 | 225, 229 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑠)) ∪
(( bday ‘𝑙) +no ( bday
‘ 0s ))) = (( bday
‘𝑙) +no ( bday ‘𝑠)) |
| 231 | | naddel1 8725 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑋)
∈ On ∧ ( bday ‘𝑠) ∈ On) → ((
bday ‘𝑙)
∈ ( bday ‘𝑋) ↔ (( bday
‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑠)))) |
| 232 | 26, 39, 135, 231 | mp3an 1463 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑙) ∈ ( bday
‘𝑋) ↔
(( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑠))) |
| 233 | 42, 232 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝑙 ∈ ( L ‘𝑋) → (( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑠))) |
| 234 | 233 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑠))) |
| 235 | 148 | ad2antll 729 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 236 | | ontr1 6430 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∈ On
→ (((( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∧
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
(( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
| 237 | 206, 236 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∧
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
(( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
| 238 | 234, 235,
237 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑙) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 239 | | elun1 4182 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
(( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 240 | 238, 239 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑙) +no ( bday ‘𝑠)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
| 241 | 230, 240 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑙) +no ( bday ‘𝑠)) ∪ (( bday
‘𝑙) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 242 | 221, 222,
223, 224, 241 | addsproplem1 28002 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑠) ∈ No
∧ (𝑠 <s
0s → (𝑠
+s 𝑙) <s (
0s +s 𝑙)))) |
| 243 | 242 | simpld 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) ∈ No
) |
| 244 | 154 | adantrl 716 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) ∈ No
) |
| 245 | | rightval 27903 |
. . . . . . . . . . . . . . 15
⊢ ( R
‘𝑌) = {𝑠 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑌 <s 𝑠} |
| 246 | 245 | reqabi 3460 |
. . . . . . . . . . . . . 14
⊢ (𝑠 ∈ ( R ‘𝑌) ↔ (𝑠 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑌 <s 𝑠)) |
| 247 | 246 | simprbi 496 |
. . . . . . . . . . . . 13
⊢ (𝑠 ∈ ( R ‘𝑌) → 𝑌 <s 𝑠) |
| 248 | 247 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 <s 𝑠) |
| 249 | 20 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑌 ∈ No
) |
| 250 | 45 | ad2antrl 728 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑙) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 251 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑌)
∈ On) → (( bday ‘𝑙) +no (
bday ‘𝑌))
∈ On) |
| 252 | 26, 31, 251 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑙) +no ( bday
‘𝑌)) ∈
On |
| 253 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑙) ∈ On ∧ (
bday ‘𝑠)
∈ On) → (( bday ‘𝑙) +no (
bday ‘𝑠))
∈ On) |
| 254 | 26, 135, 253 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
On |
| 255 | | onunel 6489 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑙) +no ( bday
‘𝑌)) ∈ On
∧ (( bday ‘𝑙) +no ( bday
‘𝑠)) ∈ On
∧ (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On) → (((( bday ‘𝑙) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑙) +no ( bday
‘𝑠))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑙) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))))) |
| 256 | 252, 254,
206, 255 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑙) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑙) +no ( bday
‘𝑠))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑙) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑙) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
| 257 | 250, 238,
256 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑙) +no ( bday ‘𝑠))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 258 | | elun1 4182 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑙) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑙) +no ( bday
‘𝑠))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑙) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑙) +no ( bday
‘𝑠))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 259 | 257, 258 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑙) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑙) +no ( bday ‘𝑠))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
| 260 | 221, 222,
249, 223, 259 | addsproplem1 28002 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑙 +s 𝑌) ∈ No
∧ (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙)))) |
| 261 | 260 | simprd 495 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 <s 𝑠 → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙))) |
| 262 | 248, 261 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑌 +s 𝑙) <s (𝑠 +s 𝑙)) |
| 263 | 222, 249 | addscomd 28000 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) = (𝑌 +s 𝑙)) |
| 264 | 222, 223 | addscomd 28000 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) = (𝑠 +s 𝑙)) |
| 265 | 262, 263,
264 | 3brtr4d 5175 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑙 +s 𝑠)) |
| 266 | | leftval 27902 |
. . . . . . . . . . . . . 14
⊢ ( L
‘𝑋) = {𝑙 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑙 <s 𝑋} |
| 267 | 266 | reqabi 3460 |
. . . . . . . . . . . . 13
⊢ (𝑙 ∈ ( L ‘𝑋) ↔ (𝑙 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑙 <s 𝑋)) |
| 268 | 267 | simprbi 496 |
. . . . . . . . . . . 12
⊢ (𝑙 ∈ ( L ‘𝑋) → 𝑙 <s 𝑋) |
| 269 | 268 | ad2antrl 728 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑙 <s 𝑋) |
| 270 | 57 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 ∈ No
) |
| 271 | | naddcom 8720 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑠) ∈ On ∧ (
bday ‘𝑙)
∈ On) → (( bday ‘𝑠) +no (
bday ‘𝑙)) =
(( bday ‘𝑙) +no ( bday
‘𝑠))) |
| 272 | 135, 26, 271 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑠) +no ( bday
‘𝑙)) = (( bday ‘𝑙) +no ( bday
‘𝑠)) |
| 273 | 272, 238 | eqeltrid 2845 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑠) +no ( bday ‘𝑙)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 274 | | naddcom 8720 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑠) ∈ On ∧ (
bday ‘𝑋)
∈ On) → (( bday ‘𝑠) +no (
bday ‘𝑋)) =
(( bday ‘𝑋) +no ( bday
‘𝑠))) |
| 275 | 135, 39, 274 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑠) +no ( bday
‘𝑋)) = (( bday ‘𝑋) +no ( bday
‘𝑠)) |
| 276 | 275, 235 | eqeltrid 2845 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑠) +no ( bday ‘𝑋)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 277 | | naddcl 8715 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑠) ∈ On ∧ (
bday ‘𝑙)
∈ On) → (( bday ‘𝑠) +no (
bday ‘𝑙))
∈ On) |
| 278 | 135, 26, 277 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑠) +no ( bday
‘𝑙)) ∈
On |
| 279 | | naddcl 8715 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑠) ∈ On ∧ (
bday ‘𝑋)
∈ On) → (( bday ‘𝑠) +no (
bday ‘𝑋))
∈ On) |
| 280 | 135, 39, 279 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑠) +no ( bday
‘𝑋)) ∈
On |
| 281 | | onunel 6489 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑠) +no ( bday
‘𝑙)) ∈ On
∧ (( bday ‘𝑠) +no ( bday
‘𝑋)) ∈ On
∧ (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On) → (((( bday ‘𝑠) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑠) +no ( bday
‘𝑋))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑠) +no ( bday
‘𝑙)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑠) +no ( bday
‘𝑋)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))))) |
| 282 | 278, 280,
206, 281 | mp3an 1463 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑠) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑠) +no ( bday
‘𝑋))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑠) +no ( bday
‘𝑙)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑠) +no ( bday
‘𝑋)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
| 283 | 273, 276,
282 | sylanbrc 583 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday
‘𝑠) +no ( bday ‘𝑋))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 284 | | elun1 4182 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑠) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑠) +no ( bday
‘𝑋))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑠) +no ( bday
‘𝑙)) ∪
(( bday ‘𝑠) +no ( bday
‘𝑋))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 285 | 283, 284 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑠) +no ( bday ‘𝑙)) ∪ (( bday
‘𝑠) +no ( bday ‘𝑋))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
| 286 | 221, 223,
222, 270, 285 | addsproplem1 28002 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑠 +s 𝑙) ∈ No
∧ (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠)))) |
| 287 | 286 | simprd 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 <s 𝑋 → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠))) |
| 288 | 269, 287 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑠) <s (𝑋 +s 𝑠)) |
| 289 | 220, 243,
244, 265, 288 | slttrd 27804 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑙 +s 𝑌) <s (𝑋 +s 𝑠)) |
| 290 | | breq12 5148 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑙 +s 𝑌) <s (𝑋 +s 𝑠))) |
| 291 | 289, 290 | syl5ibrcom 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑙 ∈ ( L ‘𝑋) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
| 292 | 291 | rexlimdvva 3213 |
. . . . . . 7
⊢ (𝜑 → (∃𝑙 ∈ ( L ‘𝑋)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑙 +s 𝑌) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
| 293 | 219, 292 | biimtrrid 243 |
. . . . . 6
⊢ (𝜑 → ((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
| 294 | 218, 293 | jaod 860 |
. . . . 5
⊢ (𝜑 → (((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏)) |
| 295 | | reeanv 3229 |
. . . . . . 7
⊢
(∃𝑚 ∈ ( L
‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌))) |
| 296 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
| 297 | 57 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 ∈ No
) |
| 298 | 60 | ad2antrl 728 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ No
) |
| 299 | 22 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 0s ∈ No ) |
| 300 | 81 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 301 | 300, 83 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
| 302 | 73, 301 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑋) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 303 | 296, 297,
298, 299, 302 | addsproplem1 28002 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑋 +s 𝑚) ∈ No
∧ (𝑚 <s
0s → (𝑚
+s 𝑋) <s (
0s +s 𝑋)))) |
| 304 | 303 | simpld 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) ∈ No
) |
| 305 | 95 | ad2antll 729 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ No
) |
| 306 | 103 | uneq2i 4165 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑟) +no ( bday
‘ 0s ))) = ((( bday
‘𝑟) +no ( bday ‘𝑚)) ∪ ( bday
‘𝑟)) |
| 307 | | naddword1 8729 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑚)
∈ On) → ( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑚))) |
| 308 | 100, 68, 307 | mp2an 692 |
. . . . . . . . . . . . . . 15
⊢ ( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑚)) |
| 309 | | ssequn2 4189 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑟) ⊆ (( bday
‘𝑟) +no ( bday ‘𝑚)) ↔ ((( bday
‘𝑟) +no ( bday ‘𝑚)) ∪ ( bday
‘𝑟)) = (( bday ‘𝑟) +no ( bday
‘𝑚))) |
| 310 | 308, 309 | mpbi 230 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
( bday ‘𝑟)) = (( bday
‘𝑟) +no ( bday ‘𝑚)) |
| 311 | 306, 310 | eqtri 2765 |
. . . . . . . . . . . . 13
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑟) +no ( bday
‘ 0s ))) = (( bday
‘𝑟) +no ( bday ‘𝑚)) |
| 312 | | naddel1 8725 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑋)
∈ On ∧ ( bday ‘𝑚) ∈ On) → ((
bday ‘𝑟)
∈ ( bday ‘𝑋) ↔ (( bday
‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑚)))) |
| 313 | 100, 39, 68, 312 | mp3an 1463 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑟) ∈ ( bday
‘𝑋) ↔
(( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑚))) |
| 314 | 114, 313 | sylib 218 |
. . . . . . . . . . . . . . . 16
⊢ (𝑟 ∈ ( R ‘𝑋) → (( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑚))) |
| 315 | 314 | ad2antll 729 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑚))) |
| 316 | | ontr1 6430 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∈ On
→ (((( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∧
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
(( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
| 317 | 206, 316 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∧
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
(( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
| 318 | 315, 300,
317 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 319 | | elun1 4182 |
. . . . . . . . . . . . . 14
⊢ ((( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
(( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 320 | 318, 319 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑚)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
| 321 | 311, 320 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 322 | 296, 305,
298, 299, 321 | addsproplem1 28002 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No
∧ (𝑚 <s
0s → (𝑚
+s 𝑟) <s (
0s +s 𝑟)))) |
| 323 | 322 | simpld 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) ∈ No
) |
| 324 | 20 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑌 ∈ No
) |
| 325 | 117 | ad2antll 729 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑌)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 326 | 325, 119 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑟) +no ( bday ‘𝑌)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
| 327 | 109, 326 | eqeltrid 2845 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑟) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑟) +no ( bday ‘ 0s ))) ∈ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 328 | 296, 305,
324, 299, 327 | addsproplem1 28002 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑌) ∈ No
∧ (𝑌 <s
0s → (𝑌
+s 𝑟) <s (
0s +s 𝑟)))) |
| 329 | 328 | simpld 494 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) ∈ No
) |
| 330 | | rightval 27903 |
. . . . . . . . . . . . . . . 16
⊢ ( R
‘𝑋) = {𝑟 ∈ ( O ‘( bday ‘𝑋)) ∣ 𝑋 <s 𝑟} |
| 331 | 330 | eleq2i 2833 |
. . . . . . . . . . . . . . 15
⊢ (𝑟 ∈ ( R ‘𝑋) ↔ 𝑟 ∈ {𝑟 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑟}) |
| 332 | 331 | biimpi 216 |
. . . . . . . . . . . . . 14
⊢ (𝑟 ∈ ( R ‘𝑋) → 𝑟 ∈ {𝑟 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑟}) |
| 333 | 332 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑟 ∈ {𝑟 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑟}) |
| 334 | | rabid 3458 |
. . . . . . . . . . . . 13
⊢ (𝑟 ∈ {𝑟 ∈ ( O ‘(
bday ‘𝑋))
∣ 𝑋 <s 𝑟} ↔ (𝑟 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑋 <s 𝑟)) |
| 335 | 333, 334 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 ∈ ( O ‘(
bday ‘𝑋))
∧ 𝑋 <s 𝑟)) |
| 336 | 335 | simprd 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑋 <s 𝑟) |
| 337 | | naddcom 8720 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑋)
∈ On) → (( bday ‘𝑚) +no (
bday ‘𝑋)) =
(( bday ‘𝑋) +no ( bday
‘𝑚))) |
| 338 | 68, 39, 337 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑚) +no ( bday
‘𝑋)) = (( bday ‘𝑋) +no ( bday
‘𝑚)) |
| 339 | 338, 300 | eqeltrid 2845 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑚) +no ( bday ‘𝑋)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 340 | | naddcom 8720 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑟)
∈ On) → (( bday ‘𝑚) +no (
bday ‘𝑟)) =
(( bday ‘𝑟) +no ( bday
‘𝑚))) |
| 341 | 68, 100, 340 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑚) +no ( bday
‘𝑟)) = (( bday ‘𝑟) +no ( bday
‘𝑚)) |
| 342 | 341, 318 | eqeltrid 2845 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (( bday
‘𝑚) +no ( bday ‘𝑟)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 343 | | naddcl 8715 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑋)
∈ On) → (( bday ‘𝑚) +no (
bday ‘𝑋))
∈ On) |
| 344 | 68, 39, 343 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑚) +no ( bday
‘𝑋)) ∈
On |
| 345 | | naddcl 8715 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑟)
∈ On) → (( bday ‘𝑚) +no (
bday ‘𝑟))
∈ On) |
| 346 | 68, 100, 345 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑚) +no ( bday
‘𝑟)) ∈
On |
| 347 | | onunel 6489 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑚) +no ( bday
‘𝑋)) ∈ On
∧ (( bday ‘𝑚) +no ( bday
‘𝑟)) ∈ On
∧ (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On) → (((( bday ‘𝑚) +no ( bday
‘𝑋)) ∪
(( bday ‘𝑚) +no ( bday
‘𝑟))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑚) +no ( bday
‘𝑋)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑚) +no ( bday
‘𝑟)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))))) |
| 348 | 344, 346,
206, 347 | mp3an 1463 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑚) +no ( bday
‘𝑋)) ∪
(( bday ‘𝑚) +no ( bday
‘𝑟))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑚) +no ( bday
‘𝑋)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑚) +no ( bday
‘𝑟)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
| 349 | 339, 342,
348 | sylanbrc 583 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday
‘𝑚) +no ( bday ‘𝑟))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 350 | | elun1 4182 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑚) +no ( bday
‘𝑋)) ∪
(( bday ‘𝑚) +no ( bday
‘𝑟))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑚) +no ( bday
‘𝑋)) ∪
(( bday ‘𝑚) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 351 | 349, 350 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑚) +no ( bday ‘𝑋)) ∪ (( bday
‘𝑚) +no ( bday ‘𝑟))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
| 352 | 296, 298,
297, 305, 351 | addsproplem1 28002 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑚 +s 𝑋) ∈ No
∧ (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚)))) |
| 353 | 352 | simprd 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 <s 𝑟 → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚))) |
| 354 | 336, 353 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑚)) |
| 355 | | leftval 27902 |
. . . . . . . . . . . . . . . . 17
⊢ ( L
‘𝑌) = {𝑚 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑚 <s 𝑌} |
| 356 | 355 | eleq2i 2833 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈ ( L ‘𝑌) ↔ 𝑚 ∈ {𝑚 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑚 <s 𝑌}) |
| 357 | 356 | biimpi 216 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ( L ‘𝑌) → 𝑚 ∈ {𝑚 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑚 <s 𝑌}) |
| 358 | 357 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 ∈ {𝑚 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑚 <s 𝑌}) |
| 359 | | rabid 3458 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ {𝑚 ∈ ( O ‘(
bday ‘𝑌))
∣ 𝑚 <s 𝑌} ↔ (𝑚 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑚 <s 𝑌)) |
| 360 | 358, 359 | sylib 218 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑚 <s 𝑌)) |
| 361 | 360 | simprd 495 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → 𝑚 <s 𝑌) |
| 362 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑚)
∈ On) → (( bday ‘𝑟) +no (
bday ‘𝑚))
∈ On) |
| 363 | 100, 68, 362 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
On |
| 364 | | naddcl 8715 |
. . . . . . . . . . . . . . . . . 18
⊢ ((( bday ‘𝑟) ∈ On ∧ (
bday ‘𝑌)
∈ On) → (( bday ‘𝑟) +no (
bday ‘𝑌))
∈ On) |
| 365 | 100, 31, 364 | mp2an 692 |
. . . . . . . . . . . . . . . . 17
⊢ (( bday ‘𝑟) +no ( bday
‘𝑌)) ∈
On |
| 366 | | onunel 6489 |
. . . . . . . . . . . . . . . . 17
⊢ (((( bday ‘𝑟) +no ( bday
‘𝑚)) ∈ On
∧ (( bday ‘𝑟) +no ( bday
‘𝑌)) ∈ On
∧ (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On) → (((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑟) +no ( bday
‘𝑌))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑟) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))))) |
| 367 | 363, 365,
206, 366 | mp3an 1463 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑟) +no ( bday
‘𝑌))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑟) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑟) +no ( bday
‘𝑌)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
| 368 | 318, 325,
367 | sylanbrc 583 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑟) +no ( bday ‘𝑌))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 369 | | elun1 4182 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑟) +no ( bday
‘𝑌))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑟) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑟) +no ( bday
‘𝑌))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 370 | 368, 369 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((( bday
‘𝑟) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑟) +no ( bday ‘𝑌))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
| 371 | 296, 305,
298, 324, 370 | addsproplem1 28002 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑟 +s 𝑚) ∈ No
∧ (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟)))) |
| 372 | 371 | simprd 495 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 <s 𝑌 → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟))) |
| 373 | 361, 372 | mpd 15 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑚 +s 𝑟) <s (𝑌 +s 𝑟)) |
| 374 | 305, 298 | addscomd 28000 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) = (𝑚 +s 𝑟)) |
| 375 | 305, 324 | addscomd 28000 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑌) = (𝑌 +s 𝑟)) |
| 376 | 373, 374,
375 | 3brtr4d 5175 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑟 +s 𝑚) <s (𝑟 +s 𝑌)) |
| 377 | 304, 323,
329, 354, 376 | slttrd 27804 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → (𝑋 +s 𝑚) <s (𝑟 +s 𝑌)) |
| 378 | | breq12 5148 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑟 +s 𝑌))) |
| 379 | 377, 378 | syl5ibrcom 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑟 ∈ ( R ‘𝑋))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
| 380 | 379 | rexlimdvva 3213 |
. . . . . . 7
⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑟 ∈ ( R ‘𝑋)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
| 381 | 295, 380 | biimtrrid 243 |
. . . . . 6
⊢ (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) → 𝑎 <s 𝑏)) |
| 382 | | reeanv 3229 |
. . . . . . 7
⊢
(∃𝑚 ∈ ( L
‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) ↔ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) |
| 383 | | lltropt 27911 |
. . . . . . . . . . . . 13
⊢ ( L
‘𝑌) <<s ( R
‘𝑌) |
| 384 | 383 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ( L ‘𝑌) <<s ( R ‘𝑌)) |
| 385 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ ( L ‘𝑌)) |
| 386 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ ( R ‘𝑌)) |
| 387 | 384, 385,
386 | ssltsepcd 27839 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 <s 𝑠) |
| 388 | 15 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
| 389 | 57 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑋 ∈ No
) |
| 390 | 60 | ad2antrl 728 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑚 ∈ No
) |
| 391 | 131 | ad2antll 729 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → 𝑠 ∈ No
) |
| 392 | 81 | ad2antrl 728 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 393 | 148 | ad2antll 729 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (( bday
‘𝑋) +no ( bday ‘𝑠)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 394 | | naddcl 8715 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑚)
∈ On) → (( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
On) |
| 395 | 39, 68, 394 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
On |
| 396 | | naddcl 8715 |
. . . . . . . . . . . . . . . . 17
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑠)
∈ On) → (( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
On) |
| 397 | 39, 135, 396 | mp2an 692 |
. . . . . . . . . . . . . . . 16
⊢ (( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
On |
| 398 | | onunel 6489 |
. . . . . . . . . . . . . . . 16
⊢ (((( bday ‘𝑋) +no ( bday
‘𝑚)) ∈ On
∧ (( bday ‘𝑋) +no ( bday
‘𝑠)) ∈ On
∧ (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On) → (((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑠))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))))) |
| 399 | 395, 397,
206, 398 | mp3an 1463 |
. . . . . . . . . . . . . . 15
⊢ (((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑠))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ↔
((( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) ∧
(( bday ‘𝑋) +no ( bday
‘𝑠)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
| 400 | 392, 393,
399 | sylanbrc 583 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑠))) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
| 401 | | elun1 4182 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑠))) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑠))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
| 402 | 400, 401 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑠))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
| 403 | 388, 389,
390, 391, 402 | addsproplem1 28002 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑋 +s 𝑚) ∈ No
∧ (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋)))) |
| 404 | 403 | simprd 495 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 <s 𝑠 → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋))) |
| 405 | 387, 404 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑚 +s 𝑋) <s (𝑠 +s 𝑋)) |
| 406 | 389, 390 | addscomd 28000 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) = (𝑚 +s 𝑋)) |
| 407 | 389, 391 | addscomd 28000 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑠) = (𝑠 +s 𝑋)) |
| 408 | 405, 406,
407 | 3brtr4d 5175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → (𝑋 +s 𝑚) <s (𝑋 +s 𝑠)) |
| 409 | | breq12 5148 |
. . . . . . . . 9
⊢ ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → (𝑎 <s 𝑏 ↔ (𝑋 +s 𝑚) <s (𝑋 +s 𝑠))) |
| 410 | 408, 409 | syl5ibrcom 247 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ ( L ‘𝑌) ∧ 𝑠 ∈ ( R ‘𝑌))) → ((𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
| 411 | 410 | rexlimdvva 3213 |
. . . . . . 7
⊢ (𝜑 → (∃𝑚 ∈ ( L ‘𝑌)∃𝑠 ∈ ( R ‘𝑌)(𝑎 = (𝑋 +s 𝑚) ∧ 𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
| 412 | 382, 411 | biimtrrid 243 |
. . . . . 6
⊢ (𝜑 → ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)) → 𝑎 <s 𝑏)) |
| 413 | 381, 412 | jaod 860 |
. . . . 5
⊢ (𝜑 → (((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) → 𝑎 <s 𝑏)) |
| 414 | 294, 413 | jaod 860 |
. . . 4
⊢ (𝜑 → ((((∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑙 ∈ ( L ‘𝑋)𝑎 = (𝑙 +s 𝑌) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠))) ∨ ((∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑟 ∈ ( R ‘𝑋)𝑏 = (𝑟 +s 𝑌)) ∨ (∃𝑚 ∈ ( L ‘𝑌)𝑎 = (𝑋 +s 𝑚) ∧ ∃𝑠 ∈ ( R ‘𝑌)𝑏 = (𝑋 +s 𝑠)))) → 𝑎 <s 𝑏)) |
| 415 | 182, 414 | biimtrid 242 |
. . 3
⊢ (𝜑 → ((𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) → 𝑎 <s 𝑏)) |
| 416 | 415 | 3impib 1117 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) ∧ 𝑏 ∈ ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) → 𝑎 <s 𝑏) |
| 417 | 7, 14, 92, 159, 416 | ssltd 27836 |
1
⊢ (𝜑 → ({𝑝 ∣ ∃𝑙 ∈ ( L ‘𝑋)𝑝 = (𝑙 +s 𝑌)} ∪ {𝑞 ∣ ∃𝑚 ∈ ( L ‘𝑌)𝑞 = (𝑋 +s 𝑚)}) <<s ({𝑤 ∣ ∃𝑟 ∈ ( R ‘𝑋)𝑤 = (𝑟 +s 𝑌)} ∪ {𝑡 ∣ ∃𝑠 ∈ ( R ‘𝑌)𝑡 = (𝑋 +s 𝑠)})) |