Step | Hyp | Ref
| Expression |
1 | | bdayelon 27119 |
. . . 4
⊢ ( bday ‘𝑌) ∈ On |
2 | | fvex 6856 |
. . . . 5
⊢ ( bday ‘𝑌) ∈ V |
3 | 2 | elon 6327 |
. . . 4
⊢ (( bday ‘𝑌) ∈ On ↔ Ord ( bday ‘𝑌)) |
4 | 1, 3 | mpbi 229 |
. . 3
⊢ Ord
( bday ‘𝑌) |
5 | | bdayelon 27119 |
. . . 4
⊢ ( bday ‘𝑍) ∈ On |
6 | | fvex 6856 |
. . . . 5
⊢ ( bday ‘𝑍) ∈ V |
7 | 6 | elon 6327 |
. . . 4
⊢ (( bday ‘𝑍) ∈ On ↔ Ord ( bday ‘𝑍)) |
8 | 5, 7 | mpbi 229 |
. . 3
⊢ Ord
( bday ‘𝑍) |
9 | | ordtri3or 6350 |
. . 3
⊢ ((Ord
( bday ‘𝑌) ∧ Ord ( bday
‘𝑍)) →
(( bday ‘𝑌) ∈ ( bday
‘𝑍) ∨
( bday ‘𝑌) = ( bday
‘𝑍) ∨
( bday ‘𝑍) ∈ ( bday
‘𝑌))) |
10 | 4, 8, 9 | mp2an 691 |
. 2
⊢ (( bday ‘𝑌) ∈ ( bday
‘𝑍) ∨
( bday ‘𝑌) = ( bday
‘𝑍) ∨
( bday ‘𝑍) ∈ ( bday
‘𝑌)) |
11 | | simpl 484 |
. . . . . 6
⊢ ((𝜑 ∧ (
bday ‘𝑌)
∈ ( bday ‘𝑍)) → 𝜑) |
12 | | addsproplem.1 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
13 | 11, 12 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌)
∈ ( bday ‘𝑍)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
14 | | addspropord.2 |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ No
) |
15 | 11, 14 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌)
∈ ( bday ‘𝑍)) → 𝑋 ∈ No
) |
16 | | addspropord.3 |
. . . . . 6
⊢ (𝜑 → 𝑌 ∈ No
) |
17 | 11, 16 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌)
∈ ( bday ‘𝑍)) → 𝑌 ∈ No
) |
18 | | addspropord.4 |
. . . . . 6
⊢ (𝜑 → 𝑍 ∈ No
) |
19 | 11, 18 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌)
∈ ( bday ‘𝑍)) → 𝑍 ∈ No
) |
20 | | addspropord.5 |
. . . . . 6
⊢ (𝜑 → 𝑌 <s 𝑍) |
21 | 11, 20 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌)
∈ ( bday ‘𝑍)) → 𝑌 <s 𝑍) |
22 | | simpr 486 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌)
∈ ( bday ‘𝑍)) → ( bday
‘𝑌) ∈
( bday ‘𝑍)) |
23 | 13, 15, 17, 19, 21, 22 | addsproplem4 27287 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝑌)
∈ ( bday ‘𝑍)) → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)) |
24 | 23 | ex 414 |
. . 3
⊢ (𝜑 → ((
bday ‘𝑌)
∈ ( bday ‘𝑍) → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))) |
25 | | simpl 484 |
. . . . . 6
⊢ ((𝜑 ∧ (
bday ‘𝑌) =
( bday ‘𝑍)) → 𝜑) |
26 | 25, 12 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌) =
( bday ‘𝑍)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
27 | 25, 14 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌) =
( bday ‘𝑍)) → 𝑋 ∈ No
) |
28 | 25, 16 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌) =
( bday ‘𝑍)) → 𝑌 ∈ No
) |
29 | 25, 18 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌) =
( bday ‘𝑍)) → 𝑍 ∈ No
) |
30 | 25, 20 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌) =
( bday ‘𝑍)) → 𝑌 <s 𝑍) |
31 | | simpr 486 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑌) =
( bday ‘𝑍)) → ( bday
‘𝑌) = ( bday ‘𝑍)) |
32 | 26, 27, 28, 29, 30, 31 | addsproplem6 27289 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝑌) =
( bday ‘𝑍)) → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)) |
33 | 32 | ex 414 |
. . 3
⊢ (𝜑 → ((
bday ‘𝑌) =
( bday ‘𝑍) → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))) |
34 | 12 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑍)
∈ ( bday ‘𝑌)) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) ∈
((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
35 | 14 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑍)
∈ ( bday ‘𝑌)) → 𝑋 ∈ No
) |
36 | 16 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑍)
∈ ( bday ‘𝑌)) → 𝑌 ∈ No
) |
37 | 18 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑍)
∈ ( bday ‘𝑌)) → 𝑍 ∈ No
) |
38 | 20 | adantr 482 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑍)
∈ ( bday ‘𝑌)) → 𝑌 <s 𝑍) |
39 | | simpr 486 |
. . . . 5
⊢ ((𝜑 ∧ (
bday ‘𝑍)
∈ ( bday ‘𝑌)) → ( bday
‘𝑍) ∈
( bday ‘𝑌)) |
40 | 34, 35, 36, 37, 38, 39 | addsproplem5 27288 |
. . . 4
⊢ ((𝜑 ∧ (
bday ‘𝑍)
∈ ( bday ‘𝑌)) → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)) |
41 | 40 | ex 414 |
. . 3
⊢ (𝜑 → ((
bday ‘𝑍)
∈ ( bday ‘𝑌) → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))) |
42 | 24, 33, 41 | 3jaod 1429 |
. 2
⊢ (𝜑 → (((
bday ‘𝑌)
∈ ( bday ‘𝑍) ∨ ( bday
‘𝑌) = ( bday ‘𝑍) ∨ ( bday
‘𝑍) ∈
( bday ‘𝑌)) → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))) |
43 | 10, 42 | mpi 20 |
1
⊢ (𝜑 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)) |