Step | Hyp | Ref
| Expression |
1 | | addspropord.3 |
. . . 4
⊢ (𝜑 → 𝑌 ∈ No
) |
2 | | addspropord.4 |
. . . 4
⊢ (𝜑 → 𝑍 ∈ No
) |
3 | | addsproplem6.6 |
. . . 4
⊢ (𝜑 → (
bday ‘𝑌) =
( bday ‘𝑍)) |
4 | | addspropord.5 |
. . . 4
⊢ (𝜑 → 𝑌 <s 𝑍) |
5 | | nodense 27043 |
. . . 4
⊢ (((𝑌 ∈
No ∧ 𝑍 ∈
No ) ∧ (( bday
‘𝑌) = ( bday ‘𝑍) ∧ 𝑌 <s 𝑍)) → ∃𝑚 ∈ No
(( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍)) |
6 | 1, 2, 3, 4, 5 | syl22anc 838 |
. . 3
⊢ (𝜑 → ∃𝑚 ∈ No
(( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍)) |
7 | | addsproplem.1 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
8 | | addspropord.2 |
. . . . . . 7
⊢ (𝜑 → 𝑋 ∈ No
) |
9 | 7, 8, 1 | addsproplem3 27286 |
. . . . . 6
⊢ (𝜑 → ((𝑋 +s 𝑌) ∈ No
∧ ({𝑎 ∣
∃𝑏 ∈ ( L
‘𝑋)𝑎 = (𝑏 +s 𝑌)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑌)𝑐 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑌)} ∧ {(𝑋 +s 𝑌)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)}))) |
10 | 9 | simp1d 1143 |
. . . . 5
⊢ (𝜑 → (𝑋 +s 𝑌) ∈ No
) |
11 | 10 | adantr 482 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑌) ∈ No
) |
12 | 7 | adantr 482 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
13 | 8 | adantr 482 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑋 ∈ No
) |
14 | | simprl 770 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 ∈ No
) |
15 | | unidm 4113 |
. . . . . . 7
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑚)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑚))) =
(( bday ‘𝑋) +no ( bday
‘𝑚)) |
16 | | simprr1 1222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ( bday
‘𝑚) ∈
( bday ‘𝑌)) |
17 | | bdayelon 27119 |
. . . . . . . . . 10
⊢ ( bday ‘𝑚) ∈ On |
18 | | bdayelon 27119 |
. . . . . . . . . 10
⊢ ( bday ‘𝑌) ∈ On |
19 | | bdayelon 27119 |
. . . . . . . . . 10
⊢ ( bday ‘𝑋) ∈ On |
20 | | naddel2 8634 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑚) ∈ On ∧ (
bday ‘𝑌)
∈ On ∧ ( bday ‘𝑋) ∈ On) → ((
bday ‘𝑚)
∈ ( bday ‘𝑌) ↔ (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌)))) |
21 | 17, 18, 19, 20 | mp3an 1462 |
. . . . . . . . 9
⊢ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ↔
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
22 | 16, 21 | sylib 217 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ (( bday
‘𝑋) +no ( bday ‘𝑌))) |
23 | | elun1 4137 |
. . . . . . . 8
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
(( bday ‘𝑋) +no ( bday
‘𝑌)) →
(( bday ‘𝑋) +no ( bday
‘𝑚)) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
24 | 22, 23 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (( bday
‘𝑋) +no ( bday ‘𝑚)) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
25 | 15, 24 | eqeltrid 2842 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ((( bday
‘𝑋) +no ( bday ‘𝑚)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑚))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
26 | 12, 13, 14, 14, 25 | addsproplem1 27284 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ((𝑋 +s 𝑚) ∈ No
∧ (𝑚 <s 𝑚 → (𝑚 +s 𝑋) <s (𝑚 +s 𝑋)))) |
27 | 26 | simpld 496 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) ∈ No
) |
28 | | uncom 4114 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) =
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
29 | 28 | eleq2i 2830 |
. . . . . . . . . . 11
⊢ (((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) ↔
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
30 | 29 | imbi1i 350 |
. . . . . . . . . 10
⊢
((((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ (((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑍)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑌))) → ((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
31 | 30 | ralbii 3097 |
. . . . . . . . 9
⊢
(∀𝑧 ∈
No (((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) ∈ ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) → ((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
32 | 31 | 2ralbii 3128 |
. . . . . . . 8
⊢
(∀𝑥 ∈
No ∀𝑦 ∈ No
∀𝑧 ∈ No (((( bday ‘𝑥) +no (
bday ‘𝑦))
∪ (( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
33 | 7, 32 | sylib 217 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
34 | 33, 8, 2 | addsproplem3 27286 |
. . . . . 6
⊢ (𝜑 → ((𝑋 +s 𝑍) ∈ No
∧ ({𝑎 ∣
∃𝑏 ∈ ( L
‘𝑋)𝑎 = (𝑏 +s 𝑍)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑍)} ∧ {(𝑋 +s 𝑍)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑍)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑍)𝑔 = (𝑋 +s ℎ)}))) |
35 | 34 | simp1d 1143 |
. . . . 5
⊢ (𝜑 → (𝑋 +s 𝑍) ∈ No
) |
36 | 35 | adantr 482 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑍) ∈ No
) |
37 | 9 | simp3d 1145 |
. . . . . 6
⊢ (𝜑 → {(𝑋 +s 𝑌)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)})) |
38 | 37 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → {(𝑋 +s 𝑌)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)})) |
39 | | ovex 7391 |
. . . . . . 7
⊢ (𝑋 +s 𝑌) ∈ V |
40 | 39 | snid 4623 |
. . . . . 6
⊢ (𝑋 +s 𝑌) ∈ {(𝑋 +s 𝑌)} |
41 | 40 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑌) ∈ {(𝑋 +s 𝑌)}) |
42 | | oldbday 27233 |
. . . . . . . . . . 11
⊢ ((( bday ‘𝑌) ∈ On ∧ 𝑚 ∈ No )
→ (𝑚 ∈ ( O
‘( bday ‘𝑌)) ↔ ( bday
‘𝑚) ∈
( bday ‘𝑌))) |
43 | 18, 14, 42 | sylancr 588 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑚 ∈ ( O ‘(
bday ‘𝑌))
↔ ( bday ‘𝑚) ∈ ( bday
‘𝑌))) |
44 | 16, 43 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 ∈ ( O ‘(
bday ‘𝑌))) |
45 | | simprr2 1223 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑌 <s 𝑚) |
46 | | breq2 5110 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑚 → (𝑌 <s 𝑎 ↔ 𝑌 <s 𝑚)) |
47 | | rightval 27197 |
. . . . . . . . . 10
⊢ ( R
‘𝑌) = {𝑎 ∈ ( O ‘( bday ‘𝑌)) ∣ 𝑌 <s 𝑎} |
48 | 46, 47 | elrab2 3649 |
. . . . . . . . 9
⊢ (𝑚 ∈ ( R ‘𝑌) ↔ (𝑚 ∈ ( O ‘(
bday ‘𝑌))
∧ 𝑌 <s 𝑚)) |
49 | 44, 45, 48 | sylanbrc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 ∈ ( R ‘𝑌)) |
50 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑋 +s 𝑚) = (𝑋 +s 𝑚) |
51 | | oveq2 7366 |
. . . . . . . . 9
⊢ (ℎ = 𝑚 → (𝑋 +s ℎ) = (𝑋 +s 𝑚)) |
52 | 51 | rspceeqv 3596 |
. . . . . . . 8
⊢ ((𝑚 ∈ ( R ‘𝑌) ∧ (𝑋 +s 𝑚) = (𝑋 +s 𝑚)) → ∃ℎ ∈ ( R ‘𝑌)(𝑋 +s 𝑚) = (𝑋 +s ℎ)) |
53 | 49, 50, 52 | sylancl 587 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ∃ℎ ∈ ( R ‘𝑌)(𝑋 +s 𝑚) = (𝑋 +s ℎ)) |
54 | | ovex 7391 |
. . . . . . . 8
⊢ (𝑋 +s 𝑚) ∈ V |
55 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑔 = (𝑋 +s 𝑚) → (𝑔 = (𝑋 +s ℎ) ↔ (𝑋 +s 𝑚) = (𝑋 +s ℎ))) |
56 | 55 | rexbidv 3176 |
. . . . . . . 8
⊢ (𝑔 = (𝑋 +s 𝑚) → (∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ) ↔ ∃ℎ ∈ ( R ‘𝑌)(𝑋 +s 𝑚) = (𝑋 +s ℎ))) |
57 | 54, 56 | elab 3631 |
. . . . . . 7
⊢ ((𝑋 +s 𝑚) ∈ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)} ↔ ∃ℎ ∈ ( R ‘𝑌)(𝑋 +s 𝑚) = (𝑋 +s ℎ)) |
58 | 53, 57 | sylibr 233 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) ∈ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)}) |
59 | | elun2 4138 |
. . . . . 6
⊢ ((𝑋 +s 𝑚) ∈ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)} → (𝑋 +s 𝑚) ∈ ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)})) |
60 | 58, 59 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) ∈ ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑌)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑌)𝑔 = (𝑋 +s ℎ)})) |
61 | 38, 41, 60 | ssltsepcd 27136 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑌) <s (𝑋 +s 𝑚)) |
62 | 33 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
63 | 2 | adantr 482 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑍 ∈ No
) |
64 | 62, 13, 63 | addsproplem3 27286 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ((𝑋 +s 𝑍) ∈ No
∧ ({𝑎 ∣
∃𝑏 ∈ ( L
‘𝑋)𝑎 = (𝑏 +s 𝑍)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑍)} ∧ {(𝑋 +s 𝑍)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑋)𝑒 = (𝑓 +s 𝑍)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑍)𝑔 = (𝑋 +s ℎ)}))) |
65 | 64 | simp2d 1144 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑍)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑍)}) |
66 | 3 | adantr 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ( bday
‘𝑌) = ( bday ‘𝑍)) |
67 | 16, 66 | eleqtrd 2840 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ( bday
‘𝑚) ∈
( bday ‘𝑍)) |
68 | | bdayelon 27119 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑍) ∈ On |
69 | | oldbday 27233 |
. . . . . . . . . . 11
⊢ ((( bday ‘𝑍) ∈ On ∧ 𝑚 ∈ No )
→ (𝑚 ∈ ( O
‘( bday ‘𝑍)) ↔ ( bday
‘𝑚) ∈
( bday ‘𝑍))) |
70 | 68, 14, 69 | sylancr 588 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑚 ∈ ( O ‘(
bday ‘𝑍))
↔ ( bday ‘𝑚) ∈ ( bday
‘𝑍))) |
71 | 67, 70 | mpbird 257 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 ∈ ( O ‘(
bday ‘𝑍))) |
72 | | simprr3 1224 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 <s 𝑍) |
73 | | breq1 5109 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑚 → (𝑎 <s 𝑍 ↔ 𝑚 <s 𝑍)) |
74 | | leftval 27196 |
. . . . . . . . . 10
⊢ ( L
‘𝑍) = {𝑎 ∈ ( O ‘( bday ‘𝑍)) ∣ 𝑎 <s 𝑍} |
75 | 73, 74 | elrab2 3649 |
. . . . . . . . 9
⊢ (𝑚 ∈ ( L ‘𝑍) ↔ (𝑚 ∈ ( O ‘(
bday ‘𝑍))
∧ 𝑚 <s 𝑍)) |
76 | 71, 72, 75 | sylanbrc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → 𝑚 ∈ ( L ‘𝑍)) |
77 | | oveq2 7366 |
. . . . . . . . 9
⊢ (𝑑 = 𝑚 → (𝑋 +s 𝑑) = (𝑋 +s 𝑚)) |
78 | 77 | rspceeqv 3596 |
. . . . . . . 8
⊢ ((𝑚 ∈ ( L ‘𝑍) ∧ (𝑋 +s 𝑚) = (𝑋 +s 𝑚)) → ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑚) = (𝑋 +s 𝑑)) |
79 | 76, 50, 78 | sylancl 587 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑚) = (𝑋 +s 𝑑)) |
80 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑐 = (𝑋 +s 𝑚) → (𝑐 = (𝑋 +s 𝑑) ↔ (𝑋 +s 𝑚) = (𝑋 +s 𝑑))) |
81 | 80 | rexbidv 3176 |
. . . . . . . 8
⊢ (𝑐 = (𝑋 +s 𝑚) → (∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑) ↔ ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑚) = (𝑋 +s 𝑑))) |
82 | 54, 81 | elab 3631 |
. . . . . . 7
⊢ ((𝑋 +s 𝑚) ∈ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)} ↔ ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑚) = (𝑋 +s 𝑑)) |
83 | 79, 82 | sylibr 233 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) ∈ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)}) |
84 | | elun2 4138 |
. . . . . 6
⊢ ((𝑋 +s 𝑚) ∈ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)} → (𝑋 +s 𝑚) ∈ ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑍)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)})) |
85 | 83, 84 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) ∈ ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑋)𝑎 = (𝑏 +s 𝑍)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑐 = (𝑋 +s 𝑑)})) |
86 | | ovex 7391 |
. . . . . . 7
⊢ (𝑋 +s 𝑍) ∈ V |
87 | 86 | snid 4623 |
. . . . . 6
⊢ (𝑋 +s 𝑍) ∈ {(𝑋 +s 𝑍)} |
88 | 87 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑍) ∈ {(𝑋 +s 𝑍)}) |
89 | 65, 85, 88 | ssltsepcd 27136 |
. . . 4
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑚) <s (𝑋 +s 𝑍)) |
90 | 11, 27, 36, 61, 89 | slttrd 27110 |
. . 3
⊢ ((𝜑 ∧ (𝑚 ∈ No
∧ (( bday ‘𝑚) ∈ ( bday
‘𝑌) ∧
𝑌 <s 𝑚 ∧ 𝑚 <s 𝑍))) → (𝑋 +s 𝑌) <s (𝑋 +s 𝑍)) |
91 | 6, 90 | rexlimddv 3159 |
. 2
⊢ (𝜑 → (𝑋 +s 𝑌) <s (𝑋 +s 𝑍)) |
92 | 1, 8 | addscomd 27282 |
. 2
⊢ (𝜑 → (𝑌 +s 𝑋) = (𝑋 +s 𝑌)) |
93 | 2, 8 | addscomd 27282 |
. 2
⊢ (𝜑 → (𝑍 +s 𝑋) = (𝑋 +s 𝑍)) |
94 | 91, 92, 93 | 3brtr4d 5138 |
1
⊢ (𝜑 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)) |