Step | Hyp | Ref
| Expression |
1 | | bdayelon 27119 |
. . . . 5
⊢ ( bday ‘𝑋) ∈ On |
2 | | bdayelon 27119 |
. . . . 5
⊢ ( bday ‘𝑌) ∈ On |
3 | | naddcl 8624 |
. . . . 5
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑌)
∈ On) → (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On) |
4 | 1, 2, 3 | mp2an 691 |
. . . 4
⊢ (( bday ‘𝑋) +no ( bday
‘𝑌)) ∈
On |
5 | | bdayelon 27119 |
. . . . 5
⊢ ( bday ‘𝑍) ∈ On |
6 | | naddcl 8624 |
. . . . 5
⊢ ((( bday ‘𝑋) ∈ On ∧ (
bday ‘𝑍)
∈ On) → (( bday ‘𝑋) +no ( bday
‘𝑍)) ∈
On) |
7 | 1, 5, 6 | mp2an 691 |
. . . 4
⊢ (( bday ‘𝑋) +no ( bday
‘𝑍)) ∈
On |
8 | 4, 7 | onun2i 6440 |
. . 3
⊢ ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) ∈
On |
9 | | risset 3222 |
. . 3
⊢ (((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) ∈
On ↔ ∃𝑎 ∈
On 𝑎 = ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍)))) |
10 | 8, 9 | mpbi 229 |
. 2
⊢
∃𝑎 ∈ On
𝑎 = ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) |
11 | | eqeq1 2741 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑏 → (𝑎 = ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) ↔ 𝑏 = ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))))) |
12 | 11 | imbi1d 342 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → ((𝑎 = ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) → ((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ (𝑏 = ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) → ((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))) |
13 | 12 | ralbidv 3175 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → (∀𝑧 ∈ No
(𝑎 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ ∀𝑧 ∈ No
(𝑏 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))) |
14 | 13 | 2ralbidv 3213 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(𝑎 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(𝑏 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))) |
15 | | fveq2 6843 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑝 → ( bday
‘𝑥) = ( bday ‘𝑝)) |
16 | 15 | oveq1d 7373 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑝 → (( bday
‘𝑥) +no ( bday ‘𝑦)) = (( bday
‘𝑝) +no ( bday ‘𝑦))) |
17 | 15 | oveq1d 7373 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑝 → (( bday
‘𝑥) +no ( bday ‘𝑧)) = (( bday
‘𝑝) +no ( bday ‘𝑧))) |
18 | 16, 17 | uneq12d 4125 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑝 → ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) = ((( bday
‘𝑝) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧)))) |
19 | 18 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑥 = 𝑝 → (𝑏 = ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) ↔ 𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧))))) |
20 | | oveq1 7365 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑝 → (𝑥 +s 𝑦) = (𝑝 +s 𝑦)) |
21 | 20 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑝 → ((𝑥 +s 𝑦) ∈ No
↔ (𝑝 +s
𝑦) ∈ No )) |
22 | | oveq2 7366 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑝 → (𝑦 +s 𝑥) = (𝑦 +s 𝑝)) |
23 | | oveq2 7366 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑝 → (𝑧 +s 𝑥) = (𝑧 +s 𝑝)) |
24 | 22, 23 | breq12d 5119 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑝 → ((𝑦 +s 𝑥) <s (𝑧 +s 𝑥) ↔ (𝑦 +s 𝑝) <s (𝑧 +s 𝑝))) |
25 | 24 | imbi2d 341 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑝 → ((𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)) ↔ (𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝)))) |
26 | 21, 25 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑥 = 𝑝 → (((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))) ↔ ((𝑝 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝))))) |
27 | 19, 26 | imbi12d 345 |
. . . . . . . 8
⊢ (𝑥 = 𝑝 → ((𝑏 = ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) → ((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ (𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧))) → ((𝑝 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝)))))) |
28 | | fveq2 6843 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑞 → ( bday
‘𝑦) = ( bday ‘𝑞)) |
29 | 28 | oveq2d 7374 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑞 → (( bday
‘𝑝) +no ( bday ‘𝑦)) = (( bday
‘𝑝) +no ( bday ‘𝑞))) |
30 | 29 | uneq1d 4123 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑞 → ((( bday
‘𝑝) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧))) = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧)))) |
31 | 30 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑦 = 𝑞 → (𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧))) ↔ 𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧))))) |
32 | | oveq2 7366 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑞 → (𝑝 +s 𝑦) = (𝑝 +s 𝑞)) |
33 | 32 | eleq1d 2823 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑞 → ((𝑝 +s 𝑦) ∈ No
↔ (𝑝 +s
𝑞) ∈ No )) |
34 | | breq1 5109 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑞 → (𝑦 <s 𝑧 ↔ 𝑞 <s 𝑧)) |
35 | | oveq1 7365 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑞 → (𝑦 +s 𝑝) = (𝑞 +s 𝑝)) |
36 | 35 | breq1d 5116 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑞 → ((𝑦 +s 𝑝) <s (𝑧 +s 𝑝) ↔ (𝑞 +s 𝑝) <s (𝑧 +s 𝑝))) |
37 | 34, 36 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑞 → ((𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝)) ↔ (𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝)))) |
38 | 33, 37 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑦 = 𝑞 → (((𝑝 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝))) ↔ ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝))))) |
39 | 31, 38 | imbi12d 345 |
. . . . . . . 8
⊢ (𝑦 = 𝑞 → ((𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧))) → ((𝑝 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑝) <s (𝑧 +s 𝑝)))) ↔ (𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧))) → ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝)))))) |
40 | | fveq2 6843 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑟 → ( bday
‘𝑧) = ( bday ‘𝑟)) |
41 | 40 | oveq2d 7374 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑟 → (( bday
‘𝑝) +no ( bday ‘𝑧)) = (( bday
‘𝑝) +no ( bday ‘𝑟))) |
42 | 41 | uneq2d 4124 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑟 → ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧))) = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟)))) |
43 | 42 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑧 = 𝑟 → (𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧))) ↔ 𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟))))) |
44 | | breq2 5110 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑟 → (𝑞 <s 𝑧 ↔ 𝑞 <s 𝑟)) |
45 | | oveq1 7365 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑟 → (𝑧 +s 𝑝) = (𝑟 +s 𝑝)) |
46 | 45 | breq2d 5118 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑟 → ((𝑞 +s 𝑝) <s (𝑧 +s 𝑝) ↔ (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))) |
47 | 44, 46 | imbi12d 345 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑟 → ((𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝)) ↔ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) |
48 | 47 | anbi2d 630 |
. . . . . . . . 9
⊢ (𝑧 = 𝑟 → (((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝))) ↔ ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
49 | 43, 48 | imbi12d 345 |
. . . . . . . 8
⊢ (𝑧 = 𝑟 → ((𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑧))) → ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑧 → (𝑞 +s 𝑝) <s (𝑧 +s 𝑝)))) ↔ (𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟))) → ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))) |
50 | 27, 39, 49 | cbvral3vw 3230 |
. . . . . . 7
⊢
(∀𝑥 ∈
No ∀𝑦 ∈ No
∀𝑧 ∈ No (𝑏 = ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) → ((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ ∀𝑝 ∈ No
∀𝑞 ∈ No ∀𝑟 ∈ No
(𝑏 = ((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
51 | 14, 50 | bitrdi 287 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(𝑎 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ ∀𝑝 ∈ No
∀𝑞 ∈ No ∀𝑟 ∈ No
(𝑏 = ((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))))) |
52 | | ralrot3 3277 |
. . . . . . . . 9
⊢
(∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑏 ∈ 𝑎 ∀𝑟 ∈ No
(𝑏 = ((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑏 ∈ 𝑎 ∀𝑝 ∈ No
∀𝑞 ∈ No ∀𝑟 ∈ No
(𝑏 = ((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
53 | | ralcom 3273 |
. . . . . . . . . . 11
⊢
(∀𝑏 ∈
𝑎 ∀𝑟 ∈
No (𝑏 = ((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑟 ∈ No
∀𝑏 ∈ 𝑎 (𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟))) → ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
54 | | r19.23v 3180 |
. . . . . . . . . . . . 13
⊢
(∀𝑏 ∈
𝑎 (𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟))) → ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ (∃𝑏 ∈ 𝑎 𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟))) → ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
55 | | risset 3222 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 ↔ ∃𝑏 ∈ 𝑎 𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟)))) |
56 | 55 | imbi1i 350 |
. . . . . . . . . . . . 13
⊢
((((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 → ((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ (∃𝑏 ∈ 𝑎 𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟))) → ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
57 | 54, 56 | bitr4i 278 |
. . . . . . . . . . . 12
⊢
(∀𝑏 ∈
𝑎 (𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟))) → ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ (((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟))) ∈ 𝑎 → ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
58 | 57 | ralbii 3097 |
. . . . . . . . . . 11
⊢
(∀𝑟 ∈
No ∀𝑏 ∈ 𝑎 (𝑏 = ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟))) → ((𝑝 +s 𝑞) ∈ No
∧ (𝑞 <s 𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑟 ∈ No
(((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 → ((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
59 | 53, 58 | bitri 275 |
. . . . . . . . . 10
⊢
(∀𝑏 ∈
𝑎 ∀𝑟 ∈
No (𝑏 = ((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑟 ∈ No
(((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 → ((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
60 | 59 | 2ralbii 3128 |
. . . . . . . . 9
⊢
(∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑏 ∈ 𝑎 ∀𝑟 ∈ No
(𝑏 = ((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑝 ∈ No
∀𝑞 ∈ No ∀𝑟 ∈ No
(((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 → ((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
61 | 52, 60 | bitr3i 277 |
. . . . . . . 8
⊢
(∀𝑏 ∈
𝑎 ∀𝑝 ∈
No ∀𝑞 ∈
No ∀𝑟 ∈ No
(𝑏 = ((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ↔ ∀𝑝 ∈ No
∀𝑞 ∈ No ∀𝑟 ∈ No
(((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 → ((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
62 | | eleq2 2827 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑎 = (((
bday ‘𝑥) +no
( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) → (((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟))) ∈ 𝑎 ↔ ((( bday
‘𝑝) +no ( bday ‘𝑞)) ∪ (( bday
‘𝑝) +no ( bday ‘𝑟))) ∈ ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))))) |
63 | 62 | imbi1d 342 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (((
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 𝑝)))))) |
64 | 63 | ralbidv 3175 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = (((
bday ‘𝑥) +no
( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) → (∀𝑟 ∈ No
(((( 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 𝑝)))))) |
65 | 64 | 2ralbidv 3213 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = (((
bday ‘𝑥) +no
( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) → (∀𝑝 ∈ No
∀𝑞 ∈ No ∀𝑟 ∈ No
(((( 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 𝑝)))))) |
66 | 65 | anbi1d 631 |
. . . . . . . . . . . . 13
⊢ (𝑎 = (((
bday ‘𝑥) +no
( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) → ((∀𝑝 ∈ No
∀𝑞 ∈ No ∀𝑟 ∈ No
(((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 → ((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
↔ (∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No
)))) |
67 | 66 | biimpcd 249 |
. . . . . . . . . . . 12
⊢
((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 → ((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
→ (𝑎 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
(∀𝑝 ∈ No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No
)))) |
68 | | simpl 484 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
→ ∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
69 | | simprll 778 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
→ 𝑥 ∈ No ) |
70 | | simprlr 779 |
. . . . . . . . . . . . . . 15
⊢
((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
→ 𝑦 ∈ No ) |
71 | 68, 69, 70 | addsproplem3 27286 |
. . . . . . . . . . . . . 14
⊢
((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
→ ((𝑥 +s
𝑦) ∈ No ∧ ({𝑎 ∣ ∃𝑏 ∈ ( L ‘𝑥)𝑎 = (𝑏 +s 𝑦)} ∪ {𝑐 ∣ ∃𝑑 ∈ ( L ‘𝑦)𝑐 = (𝑥 +s 𝑑)}) <<s {(𝑥 +s 𝑦)} ∧ {(𝑥 +s 𝑦)} <<s ({𝑒 ∣ ∃𝑓 ∈ ( R ‘𝑥)𝑒 = (𝑓 +s 𝑦)} ∪ {𝑔 ∣ ∃ℎ ∈ ( R ‘𝑦)𝑔 = (𝑥 +s ℎ)}))) |
72 | 71 | simp1d 1143 |
. . . . . . . . . . . . 13
⊢
((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
→ (𝑥 +s
𝑦) ∈ No ) |
73 | 68 | adantr 482 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
∧ 𝑦 <s 𝑧) → ∀𝑝 ∈
No ∀𝑞 ∈
No ∀𝑟 ∈ No
(((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝))))) |
74 | 69 | adantr 482 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
∧ 𝑦 <s 𝑧) → 𝑥 ∈ No
) |
75 | 70 | adantr 482 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
∧ 𝑦 <s 𝑧) → 𝑦 ∈ No
) |
76 | | simplrr 777 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
∧ 𝑦 <s 𝑧) → 𝑧 ∈ No
) |
77 | | simpr 486 |
. . . . . . . . . . . . . . 15
⊢
(((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
∧ 𝑦 <s 𝑧) → 𝑦 <s 𝑧) |
78 | 73, 74, 75, 76, 77 | addsproplem7 27290 |
. . . . . . . . . . . . . 14
⊢
(((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
∧ 𝑦 <s 𝑧) → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)) |
79 | 78 | ex 414 |
. . . . . . . . . . . . 13
⊢
((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
→ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))) |
80 | 72, 79 | jca 513 |
. . . . . . . . . . . 12
⊢
((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
→ ((𝑥 +s
𝑦) ∈ No ∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) |
81 | 67, 80 | syl6 35 |
. . . . . . . . . . 11
⊢
((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 → ((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ ((𝑥 ∈ No
∧ 𝑦 ∈ No ) ∧ 𝑧 ∈ No ))
→ (𝑎 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
82 | 81 | anassrs 469 |
. . . . . . . . . 10
⊢
(((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 → ((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ (𝑥 ∈ No
∧ 𝑦 ∈ No )) ∧ 𝑧 ∈ No )
→ (𝑎 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
83 | 82 | ralrimiva 3144 |
. . . . . . . . 9
⊢
((∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 → ((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) ∧ (𝑥 ∈ No
∧ 𝑦 ∈ No )) → ∀𝑧 ∈ No
(𝑎 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
84 | 83 | ralrimivva 3198 |
. . . . . . . 8
⊢
(∀𝑝 ∈
No ∀𝑞 ∈ No
∀𝑟 ∈ No (((( bday ‘𝑝) +no (
bday ‘𝑞))
∪ (( bday ‘𝑝) +no ( bday
‘𝑟))) ∈
𝑎 → ((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(𝑎 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
85 | 61, 84 | sylbi 216 |
. . . . . . 7
⊢
(∀𝑏 ∈
𝑎 ∀𝑝 ∈
No ∀𝑞 ∈
No ∀𝑟 ∈ No
(𝑏 = ((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(𝑎 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
86 | 85 | a1i 11 |
. . . . . 6
⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 ∀𝑝 ∈ No
∀𝑞 ∈ No ∀𝑟 ∈ No
(𝑏 = ((( bday ‘𝑝) +no ( bday
‘𝑞)) ∪
(( bday ‘𝑝) +no ( bday
‘𝑟))) →
((𝑝 +s 𝑞) ∈
No ∧ (𝑞 <s
𝑟 → (𝑞 +s 𝑝) <s (𝑟 +s 𝑝)))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ∀𝑧 ∈ No
(𝑎 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))))) |
87 | 51, 86 | tfis2 7794 |
. . . . 5
⊢ (𝑎 ∈ On → ∀𝑥 ∈
No ∀𝑦 ∈
No ∀𝑧 ∈ No
(𝑎 = ((( bday ‘𝑥) +no ( bday
‘𝑦)) ∪
(( bday ‘𝑥) +no ( bday
‘𝑧))) →
((𝑥 +s 𝑦) ∈
No ∧ (𝑦 <s
𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))))) |
88 | | fveq2 6843 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → ( bday
‘𝑥) = ( bday ‘𝑋)) |
89 | 88 | oveq1d 7373 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (( bday
‘𝑥) +no ( bday ‘𝑦)) = (( bday
‘𝑋) +no ( bday ‘𝑦))) |
90 | 88 | oveq1d 7373 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (( bday
‘𝑥) +no ( bday ‘𝑧)) = (( bday
‘𝑋) +no ( bday ‘𝑧))) |
91 | 89, 90 | uneq12d 4125 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) = ((( bday
‘𝑋) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧)))) |
92 | 91 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (𝑎 = ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) ↔ 𝑎 = ((( bday
‘𝑋) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧))))) |
93 | | oveq1 7365 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (𝑥 +s 𝑦) = (𝑋 +s 𝑦)) |
94 | 93 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝑥 +s 𝑦) ∈ No
↔ (𝑋 +s
𝑦) ∈ No )) |
95 | | oveq2 7366 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑦 +s 𝑥) = (𝑦 +s 𝑋)) |
96 | | oveq2 7366 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (𝑧 +s 𝑥) = (𝑧 +s 𝑋)) |
97 | 95, 96 | breq12d 5119 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → ((𝑦 +s 𝑥) <s (𝑧 +s 𝑥) ↔ (𝑦 +s 𝑋) <s (𝑧 +s 𝑋))) |
98 | 97 | imbi2d 341 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → ((𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)) ↔ (𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋)))) |
99 | 94, 98 | anbi12d 632 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥))) ↔ ((𝑋 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋))))) |
100 | 92, 99 | imbi12d 345 |
. . . . . 6
⊢ (𝑥 = 𝑋 → ((𝑎 = ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) → ((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) ↔ (𝑎 = ((( bday
‘𝑋) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧))) → ((𝑋 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋)))))) |
101 | | fveq2 6843 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → ( bday
‘𝑦) = ( bday ‘𝑌)) |
102 | 101 | oveq2d 7374 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → (( bday
‘𝑋) +no ( bday ‘𝑦)) = (( bday
‘𝑋) +no ( bday ‘𝑌))) |
103 | 102 | uneq1d 4123 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ((( bday
‘𝑋) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧))) = ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧)))) |
104 | 103 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (𝑎 = ((( bday
‘𝑋) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧))) ↔ 𝑎 = ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧))))) |
105 | | oveq2 7366 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → (𝑋 +s 𝑦) = (𝑋 +s 𝑌)) |
106 | 105 | eleq1d 2823 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ((𝑋 +s 𝑦) ∈ No
↔ (𝑋 +s
𝑌) ∈ No )) |
107 | | breq1 5109 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → (𝑦 <s 𝑧 ↔ 𝑌 <s 𝑧)) |
108 | | oveq1 7365 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑌 → (𝑦 +s 𝑋) = (𝑌 +s 𝑋)) |
109 | 108 | breq1d 5116 |
. . . . . . . . 9
⊢ (𝑦 = 𝑌 → ((𝑦 +s 𝑋) <s (𝑧 +s 𝑋) ↔ (𝑌 +s 𝑋) <s (𝑧 +s 𝑋))) |
110 | 107, 109 | imbi12d 345 |
. . . . . . . 8
⊢ (𝑦 = 𝑌 → ((𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋)) ↔ (𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋)))) |
111 | 106, 110 | anbi12d 632 |
. . . . . . 7
⊢ (𝑦 = 𝑌 → (((𝑋 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋))) ↔ ((𝑋 +s 𝑌) ∈ No
∧ (𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋))))) |
112 | 104, 111 | imbi12d 345 |
. . . . . 6
⊢ (𝑦 = 𝑌 → ((𝑎 = ((( bday
‘𝑋) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧))) → ((𝑋 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑋) <s (𝑧 +s 𝑋)))) ↔ (𝑎 = ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧))) → ((𝑋 +s 𝑌) ∈ No
∧ (𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋)))))) |
113 | | fveq2 6843 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑍 → ( bday
‘𝑧) = ( bday ‘𝑍)) |
114 | 113 | oveq2d 7374 |
. . . . . . . . 9
⊢ (𝑧 = 𝑍 → (( bday
‘𝑋) +no ( bday ‘𝑧)) = (( bday
‘𝑋) +no ( bday ‘𝑍))) |
115 | 114 | uneq2d 4124 |
. . . . . . . 8
⊢ (𝑧 = 𝑍 → ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧))) = ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍)))) |
116 | 115 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑧 = 𝑍 → (𝑎 = ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧))) ↔ 𝑎 = ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))))) |
117 | | breq2 5110 |
. . . . . . . . 9
⊢ (𝑧 = 𝑍 → (𝑌 <s 𝑧 ↔ 𝑌 <s 𝑍)) |
118 | | oveq1 7365 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑍 → (𝑧 +s 𝑋) = (𝑍 +s 𝑋)) |
119 | 118 | breq2d 5118 |
. . . . . . . . 9
⊢ (𝑧 = 𝑍 → ((𝑌 +s 𝑋) <s (𝑧 +s 𝑋) ↔ (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))) |
120 | 117, 119 | imbi12d 345 |
. . . . . . . 8
⊢ (𝑧 = 𝑍 → ((𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋)) ↔ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)))) |
121 | 120 | anbi2d 630 |
. . . . . . 7
⊢ (𝑧 = 𝑍 → (((𝑋 +s 𝑌) ∈ No
∧ (𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋))) ↔ ((𝑋 +s 𝑌) ∈ No
∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))))) |
122 | 116, 121 | imbi12d 345 |
. . . . . 6
⊢ (𝑧 = 𝑍 → ((𝑎 = ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑧))) → ((𝑋 +s 𝑌) ∈ No
∧ (𝑌 <s 𝑧 → (𝑌 +s 𝑋) <s (𝑧 +s 𝑋)))) ↔ (𝑎 = ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) → ((𝑋 +s 𝑌) ∈ No
∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)))))) |
123 | 100, 112,
122 | rspc3v 3594 |
. . . . 5
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ 𝑍 ∈ No )
→ (∀𝑥 ∈
No ∀𝑦 ∈ No
∀𝑧 ∈ No (𝑎 = ((( bday
‘𝑥) +no ( bday ‘𝑦)) ∪ (( bday
‘𝑥) +no ( bday ‘𝑧))) → ((𝑥 +s 𝑦) ∈ No
∧ (𝑦 <s 𝑧 → (𝑦 +s 𝑥) <s (𝑧 +s 𝑥)))) → (𝑎 = ((( bday
‘𝑋) +no ( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) → ((𝑋 +s 𝑌) ∈ No
∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)))))) |
124 | 87, 123 | syl5com 31 |
. . . 4
⊢ (𝑎 ∈ On → ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ 𝑍 ∈ No )
→ (𝑎 = ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑋 +s 𝑌) ∈
No ∧ (𝑌 <s
𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)))))) |
125 | 124 | com23 86 |
. . 3
⊢ (𝑎 ∈ On → (𝑎 = (((
bday ‘𝑋) +no
( bday ‘𝑌)) ∪ (( bday
‘𝑋) +no ( bday ‘𝑍))) → ((𝑋 ∈ No
∧ 𝑌 ∈ No ∧ 𝑍 ∈ No )
→ ((𝑋 +s
𝑌) ∈ No ∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)))))) |
126 | 125 | rexlimiv 3146 |
. 2
⊢
(∃𝑎 ∈ On
𝑎 = ((( bday ‘𝑋) +no ( bday
‘𝑌)) ∪
(( bday ‘𝑋) +no ( bday
‘𝑍))) →
((𝑋 ∈ No ∧ 𝑌 ∈ No
∧ 𝑍 ∈ No ) → ((𝑋 +s 𝑌) ∈ No
∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋))))) |
127 | 10, 126 | ax-mp 5 |
1
⊢ ((𝑋 ∈
No ∧ 𝑌 ∈
No ∧ 𝑍 ∈ No )
→ ((𝑋 +s
𝑌) ∈ No ∧ (𝑌 <s 𝑍 → (𝑌 +s 𝑋) <s (𝑍 +s 𝑋)))) |