Step | Hyp | Ref
| Expression |
1 | | addsproplem.1 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
2 | | uncom 4114 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) =
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌))) |
3 | 2 | eleq2i 2830 |
. . . . . . . . 9
⊢ (((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) ↔
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌)))) |
4 | 3 | imbi1i 350 |
. . . . . . . 8
⊢
((((( 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 𝑥))))) |
5 | 4 | ralbii 3097 |
. . . . . . 7
⊢
(∀𝑧 ∈
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 𝑥))))) |
6 | 5 | 2ralbii 3128 |
. . . . . 6
⊢
(∀𝑥 ∈
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 𝑥))))) |
7 | 1, 6 | sylib 217 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑍)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑌))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
8 | | addspropord.2 |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ No
) |
9 | | addspropord.4 |
. . . . 5
⊢ (𝜑 → 𝑍 ∈ No
) |
10 | 7, 8, 9 | addsproplem3 27286 |
. . . 4
⊢ (𝜑 → ((𝑋 +s 𝑍) ∈ No
∧ ({𝑎 ∣
∃𝑐 ∈ ( L
‘𝑋)𝑎 = (𝑐 +s 𝑍)} ∪ {𝑏 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑏 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑍)} ∧ {(𝑋 +s 𝑍)} <<s ({𝑒 ∣ ∃𝑔 ∈ ( R ‘𝑋)𝑒 = (𝑔 +s 𝑍)} ∪ {𝑓 ∣ ∃ℎ ∈ ( R ‘𝑍)𝑓 = (𝑋 +s ℎ)}))) |
11 | 10 | simp2d 1144 |
. . 3
⊢ (𝜑 → ({𝑎 ∣ ∃𝑐 ∈ ( L ‘𝑋)𝑎 = (𝑐 +s 𝑍)} ∪ {𝑏 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑏 = (𝑋 +s 𝑑)}) <<s {(𝑋 +s 𝑍)}) |
12 | | addsproplem4.6 |
. . . . . . . 8
⊢ (𝜑 → (
bday ‘𝑌)
∈ ( bday ‘𝑍)) |
13 | | bdayelon 27119 |
. . . . . . . . 9
⊢ ( bday ‘𝑍) ∈ On |
14 | | addspropord.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑌 ∈ No
) |
15 | | oldbday 27233 |
. . . . . . . . 9
⊢ ((( bday ‘𝑍) ∈ On ∧ 𝑌 ∈ No )
→ (𝑌 ∈ ( O
‘( bday ‘𝑍)) ↔ ( bday
‘𝑌) ∈
( bday ‘𝑍))) |
16 | 13, 14, 15 | sylancr 588 |
. . . . . . . 8
⊢ (𝜑 → (𝑌 ∈ ( O ‘(
bday ‘𝑍))
↔ ( bday ‘𝑌) ∈ ( bday
‘𝑍))) |
17 | 12, 16 | mpbird 257 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ ( O ‘(
bday ‘𝑍))) |
18 | | addspropord.5 |
. . . . . . 7
⊢ (𝜑 → 𝑌 <s 𝑍) |
19 | | breq1 5109 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → (𝑦 <s 𝑍 ↔ 𝑌 <s 𝑍)) |
20 | | leftval 27196 |
. . . . . . . 8
⊢ ( L
‘𝑍) = {𝑦 ∈ ( O ‘( bday ‘𝑍)) ∣ 𝑦 <s 𝑍} |
21 | 19, 20 | elrab2 3649 |
. . . . . . 7
⊢ (𝑌 ∈ ( L ‘𝑍) ↔ (𝑌 ∈ ( O ‘(
bday ‘𝑍))
∧ 𝑌 <s 𝑍)) |
22 | 17, 18, 21 | sylanbrc 584 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ ( L ‘𝑍)) |
23 | | eqid 2737 |
. . . . . 6
⊢ (𝑋 +s 𝑌) = (𝑋 +s 𝑌) |
24 | | oveq2 7366 |
. . . . . . 7
⊢ (𝑑 = 𝑌 → (𝑋 +s 𝑑) = (𝑋 +s 𝑌)) |
25 | 24 | rspceeqv 3596 |
. . . . . 6
⊢ ((𝑌 ∈ ( L ‘𝑍) ∧ (𝑋 +s 𝑌) = (𝑋 +s 𝑌)) → ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑌) = (𝑋 +s 𝑑)) |
26 | 22, 23, 25 | sylancl 587 |
. . . . 5
⊢ (𝜑 → ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑌) = (𝑋 +s 𝑑)) |
27 | | ovex 7391 |
. . . . . 6
⊢ (𝑋 +s 𝑌) ∈ V |
28 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑏 = (𝑋 +s 𝑌) → (𝑏 = (𝑋 +s 𝑑) ↔ (𝑋 +s 𝑌) = (𝑋 +s 𝑑))) |
29 | 28 | rexbidv 3176 |
. . . . . 6
⊢ (𝑏 = (𝑋 +s 𝑌) → (∃𝑑 ∈ ( L ‘𝑍)𝑏 = (𝑋 +s 𝑑) ↔ ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑌) = (𝑋 +s 𝑑))) |
30 | 27, 29 | elab 3631 |
. . . . 5
⊢ ((𝑋 +s 𝑌) ∈ {𝑏 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑏 = (𝑋 +s 𝑑)} ↔ ∃𝑑 ∈ ( L ‘𝑍)(𝑋 +s 𝑌) = (𝑋 +s 𝑑)) |
31 | 26, 30 | sylibr 233 |
. . . 4
⊢ (𝜑 → (𝑋 +s 𝑌) ∈ {𝑏 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑏 = (𝑋 +s 𝑑)}) |
32 | | elun2 4138 |
. . . 4
⊢ ((𝑋 +s 𝑌) ∈ {𝑏 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑏 = (𝑋 +s 𝑑)} → (𝑋 +s 𝑌) ∈ ({𝑎 ∣ ∃𝑐 ∈ ( L ‘𝑋)𝑎 = (𝑐 +s 𝑍)} ∪ {𝑏 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑏 = (𝑋 +s 𝑑)})) |
33 | 31, 32 | syl 17 |
. . 3
⊢ (𝜑 → (𝑋 +s 𝑌) ∈ ({𝑎 ∣ ∃𝑐 ∈ ( L ‘𝑋)𝑎 = (𝑐 +s 𝑍)} ∪ {𝑏 ∣ ∃𝑑 ∈ ( L ‘𝑍)𝑏 = (𝑋 +s 𝑑)})) |
34 | | ovex 7391 |
. . . . 5
⊢ (𝑋 +s 𝑍) ∈ V |
35 | 34 | snid 4623 |
. . . 4
⊢ (𝑋 +s 𝑍) ∈ {(𝑋 +s 𝑍)} |
36 | 35 | a1i 11 |
. . 3
⊢ (𝜑 → (𝑋 +s 𝑍) ∈ {(𝑋 +s 𝑍)}) |
37 | 11, 33, 36 | ssltsepcd 27136 |
. 2
⊢ (𝜑 → (𝑋 +s 𝑌) <s (𝑋 +s 𝑍)) |
38 | 14, 8 | addscomd 27282 |
. 2
⊢ (𝜑 → (𝑌 +s 𝑋) = (𝑋 +s 𝑌)) |
39 | 9, 8 | addscomd 27282 |
. 2
⊢ (𝜑 → (𝑍 +s 𝑋) = (𝑋 +s 𝑍)) |
40 | 37, 38, 39 | 3brtr4d 5138 |
1
⊢ (𝜑 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)) |