Step | Hyp | Ref
| Expression |
1 | | bdayelon 27067 |
. . . 4
⊢ ( bday ‘𝐴) ∈ On |
2 | | bdayelon 27067 |
. . . 4
⊢ ( bday ‘𝐵) ∈ On |
3 | 1, 2 | onun2i 6436 |
. . 3
⊢ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) ∈
On |
4 | | risset 3219 |
. . 3
⊢ ((( bday ‘𝐴) ∪ ( bday
‘𝐵)) ∈ On
↔ ∃𝑎 ∈ On
𝑎 = (( bday ‘𝐴) ∪ ( bday
‘𝐵))) |
5 | 3, 4 | mpbi 229 |
. 2
⊢
∃𝑎 ∈ On
𝑎 = (( bday ‘𝐴) ∪ ( bday
‘𝐵)) |
6 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑎 = 𝑏 → (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) ↔ 𝑏 = (( bday
‘𝑝) ∪
( bday ‘𝑞)))) |
7 | 6 | imbi1d 341 |
. . . . . . . 8
⊢ (𝑎 = 𝑏 → ((𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))) ↔ (𝑏 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))))) |
8 | 7 | 2ralbidv 3210 |
. . . . . . 7
⊢ (𝑎 = 𝑏 → (∀𝑝 ∈ No
∀𝑞 ∈ No (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))) ↔ ∀𝑝 ∈
No ∀𝑞 ∈
No (𝑏 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))))) |
9 | | fveq2 6839 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑥 → ( bday
‘𝑝) = ( bday ‘𝑥)) |
10 | 9 | uneq1d 4120 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑥 → (( bday
‘𝑝) ∪
( bday ‘𝑞)) = (( bday
‘𝑥) ∪
( bday ‘𝑞))) |
11 | 10 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑝 = 𝑥 → (𝑏 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) ↔ 𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑞)))) |
12 | | fveq2 6839 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑥 → ( -us ‘𝑝) = ( -us ‘𝑥)) |
13 | 12 | eleq1d 2822 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑥 → (( -us ‘𝑝) ∈ No
↔ ( -us ‘𝑥)
∈ No )) |
14 | | breq1 5106 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑥 → (𝑝 <s 𝑞 ↔ 𝑥 <s 𝑞)) |
15 | 12 | breq2d 5115 |
. . . . . . . . . . 11
⊢ (𝑝 = 𝑥 → (( -us ‘𝑞) <s ( -us ‘𝑝) ↔ ( -us ‘𝑞) <s ( -us ‘𝑥))) |
16 | 14, 15 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑝 = 𝑥 → ((𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)) ↔ (𝑥 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑥)))) |
17 | 13, 16 | anbi12d 631 |
. . . . . . . . 9
⊢ (𝑝 = 𝑥 → ((( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝))) ↔ (( -us ‘𝑥) ∈
No ∧ (𝑥 <s
𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑥))))) |
18 | 11, 17 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑝 = 𝑥 → ((𝑏 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))) ↔ (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑞)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑥)))))) |
19 | | fveq2 6839 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑦 → ( bday
‘𝑞) = ( bday ‘𝑦)) |
20 | 19 | uneq2d 4121 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑦 → (( bday
‘𝑥) ∪
( bday ‘𝑞)) = (( bday
‘𝑥) ∪
( bday ‘𝑦))) |
21 | 20 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑞 = 𝑦 → (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑞)) ↔ 𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)))) |
22 | | breq2 5107 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑦 → (𝑥 <s 𝑞 ↔ 𝑥 <s 𝑦)) |
23 | | fveq2 6839 |
. . . . . . . . . . . 12
⊢ (𝑞 = 𝑦 → ( -us ‘𝑞) = ( -us ‘𝑦)) |
24 | 23 | breq1d 5113 |
. . . . . . . . . . 11
⊢ (𝑞 = 𝑦 → (( -us ‘𝑞) <s ( -us ‘𝑥) ↔ ( -us ‘𝑦) <s ( -us ‘𝑥))) |
25 | 22, 24 | imbi12d 344 |
. . . . . . . . . 10
⊢ (𝑞 = 𝑦 → ((𝑥 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑥)) ↔ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) |
26 | 25 | anbi2d 629 |
. . . . . . . . 9
⊢ (𝑞 = 𝑦 → ((( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑥))) ↔ (( -us ‘𝑥) ∈
No ∧ (𝑥 <s
𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
27 | 21, 26 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑞 = 𝑦 → ((𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑞)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑥)))) ↔ (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))))) |
28 | 18, 27 | cbvral2vw 3225 |
. . . . . . 7
⊢
(∀𝑝 ∈
No ∀𝑞 ∈ No
(𝑏 = (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑝) ∈ No ∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))) ↔ ∀𝑥 ∈ No
∀𝑦 ∈ No (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
29 | 8, 28 | bitrdi 286 |
. . . . . 6
⊢ (𝑎 = 𝑏 → (∀𝑝 ∈ No
∀𝑞 ∈ No (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))) ↔ ∀𝑥 ∈
No ∀𝑦 ∈
No (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))))) |
30 | | raleq 3307 |
. . . . . . . . . . 11
⊢ (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (∀𝑏 ∈ 𝑎 ∀𝑥 ∈ No
∀𝑦 ∈ No (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) ↔ ∀𝑏 ∈ ((
bday ‘𝑝) ∪
( bday ‘𝑞))∀𝑥 ∈ No
∀𝑦 ∈ No (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))))) |
31 | | ralrot3 3274 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
No ∀𝑦 ∈ No
∀𝑏 ∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞))(𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) ↔ ∀𝑏 ∈ ((
bday ‘𝑝) ∪
( bday ‘𝑞))∀𝑥 ∈ No
∀𝑦 ∈ No (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
32 | | r19.23v 3177 |
. . . . . . . . . . . . . 14
⊢
(∀𝑏 ∈
(( bday ‘𝑝) ∪ ( bday
‘𝑞))(𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) ↔ (∃𝑏 ∈ ((
bday ‘𝑝) ∪
( bday ‘𝑞))𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
33 | | risset 3219 |
. . . . . . . . . . . . . . 15
⊢ ((( bday ‘𝑥) ∪ ( bday
‘𝑦)) ∈
(( bday ‘𝑝) ∪ ( bday
‘𝑞)) ↔
∃𝑏 ∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞))𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦))) |
34 | 33 | imbi1i 349 |
. . . . . . . . . . . . . 14
⊢ (((( bday ‘𝑥) ∪ ( bday
‘𝑦)) ∈
(( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) ↔ (∃𝑏 ∈ (( bday
‘𝑝) ∪
( bday ‘𝑞))𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
35 | 32, 34 | bitr4i 277 |
. . . . . . . . . . . . 13
⊢
(∀𝑏 ∈
(( bday ‘𝑝) ∪ ( bday
‘𝑞))(𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) ↔ ((( bday ‘𝑥) ∪ ( bday
‘𝑦)) ∈
(( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
36 | 35 | 2ralbii 3125 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
No ∀𝑦 ∈ No
∀𝑏 ∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞))(𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) ↔ ∀𝑥 ∈
No ∀𝑦 ∈
No ((( bday
‘𝑥) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
37 | 31, 36 | bitr3i 276 |
. . . . . . . . . . 11
⊢
(∀𝑏 ∈
(( bday ‘𝑝) ∪ ( bday
‘𝑞))∀𝑥 ∈ No
∀𝑦 ∈ No (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) ↔ ∀𝑥 ∈
No ∀𝑦 ∈
No ((( bday
‘𝑥) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
38 | 30, 37 | bitrdi 286 |
. . . . . . . . . 10
⊢ (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (∀𝑏 ∈ 𝑎 ∀𝑥 ∈ No
∀𝑦 ∈ No (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) ↔ ∀𝑥 ∈
No ∀𝑦 ∈
No ((( bday
‘𝑥) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))))) |
39 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈
No ∧ 𝑞 ∈
No ) ∧ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
40 | | simpll 765 |
. . . . . . . . . . . . . 14
⊢ (((𝑝 ∈
No ∧ 𝑞 ∈
No ) ∧ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) → 𝑝 ∈ No
) |
41 | 39, 40 | negsproplem3 34316 |
. . . . . . . . . . . . 13
⊢ (((𝑝 ∈
No ∧ 𝑞 ∈
No ) ∧ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) → (( -us ‘𝑝) ∈ No
∧ ( -us “ ( R ‘𝑝)) <<s {( -us ‘𝑝)} ∧ {( -us ‘𝑝)} <<s ( -us “ ( L ‘𝑝)))) |
42 | 41 | simp1d 1142 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈
No ∧ 𝑞 ∈
No ) ∧ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) → ( -us ‘𝑝) ∈ No
) |
43 | | simplr 767 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈
No ∧ 𝑞 ∈
No ) ∧ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) ∧ 𝑝 <s 𝑞) → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
44 | | simplll 773 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈
No ∧ 𝑞 ∈
No ) ∧ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) ∧ 𝑝 <s 𝑞) → 𝑝 ∈ No
) |
45 | | simpllr 774 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈
No ∧ 𝑞 ∈
No ) ∧ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) ∧ 𝑝 <s 𝑞) → 𝑞 ∈ No
) |
46 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((((𝑝 ∈
No ∧ 𝑞 ∈
No ) ∧ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) ∧ 𝑝 <s 𝑞) → 𝑝 <s 𝑞) |
47 | 43, 44, 45, 46 | negsproplem7 34320 |
. . . . . . . . . . . . 13
⊢ ((((𝑝 ∈
No ∧ 𝑞 ∈
No ) ∧ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) ∧ 𝑝 <s 𝑞) → ( -us ‘𝑞) <s ( -us ‘𝑝)) |
48 | 47 | ex 413 |
. . . . . . . . . . . 12
⊢ (((𝑝 ∈
No ∧ 𝑞 ∈
No ) ∧ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) → (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝))) |
49 | 42, 48 | jca 512 |
. . . . . . . . . . 11
⊢ (((𝑝 ∈
No ∧ 𝑞 ∈
No ) ∧ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))) |
50 | 49 | expcom 414 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
No ∀𝑦 ∈ No
((( bday ‘𝑥) ∪ ( bday
‘𝑦)) ∈
(( bday ‘𝑝) ∪ ( bday
‘𝑞)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) → ((𝑝 ∈ No
∧ 𝑞 ∈ No ) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝))))) |
51 | 38, 50 | syl6bi 252 |
. . . . . . . . 9
⊢ (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (∀𝑏 ∈ 𝑎 ∀𝑥 ∈ No
∀𝑦 ∈ No (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) → ((𝑝 ∈ No
∧ 𝑞 ∈ No ) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))))) |
52 | 51 | com3l 89 |
. . . . . . . 8
⊢
(∀𝑏 ∈
𝑎 ∀𝑥 ∈
No ∀𝑦 ∈
No (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) → ((𝑝 ∈ No
∧ 𝑞 ∈ No ) → (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))))) |
53 | 52 | ralrimivv 3193 |
. . . . . . 7
⊢
(∀𝑏 ∈
𝑎 ∀𝑥 ∈
No ∀𝑦 ∈
No (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) → ∀𝑝 ∈
No ∀𝑞 ∈
No (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝))))) |
54 | 53 | a1i 11 |
. . . . . 6
⊢ (𝑎 ∈ On → (∀𝑏 ∈ 𝑎 ∀𝑥 ∈ No
∀𝑦 ∈ No (𝑏 = (( bday
‘𝑥) ∪
( bday ‘𝑦)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) → ∀𝑝 ∈
No ∀𝑞 ∈
No (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))))) |
55 | 29, 54 | tfis2 7785 |
. . . . 5
⊢ (𝑎 ∈ On → ∀𝑝 ∈
No ∀𝑞 ∈
No (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝))))) |
56 | | fveq2 6839 |
. . . . . . . . 9
⊢ (𝑝 = 𝐴 → ( bday
‘𝑝) = ( bday ‘𝐴)) |
57 | 56 | uneq1d 4120 |
. . . . . . . 8
⊢ (𝑝 = 𝐴 → (( bday
‘𝑝) ∪
( bday ‘𝑞)) = (( bday
‘𝐴) ∪
( bday ‘𝑞))) |
58 | 57 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑝 = 𝐴 → (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) ↔ 𝑎 = (( bday
‘𝐴) ∪
( bday ‘𝑞)))) |
59 | | fveq2 6839 |
. . . . . . . . 9
⊢ (𝑝 = 𝐴 → ( -us ‘𝑝) = ( -us ‘𝐴)) |
60 | 59 | eleq1d 2822 |
. . . . . . . 8
⊢ (𝑝 = 𝐴 → (( -us ‘𝑝) ∈ No
↔ ( -us ‘𝐴)
∈ No )) |
61 | | breq1 5106 |
. . . . . . . . 9
⊢ (𝑝 = 𝐴 → (𝑝 <s 𝑞 ↔ 𝐴 <s 𝑞)) |
62 | 59 | breq2d 5115 |
. . . . . . . . 9
⊢ (𝑝 = 𝐴 → (( -us ‘𝑞) <s ( -us ‘𝑝) ↔ ( -us ‘𝑞) <s ( -us ‘𝐴))) |
63 | 61, 62 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑝 = 𝐴 → ((𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)) ↔ (𝐴 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝐴)))) |
64 | 60, 63 | anbi12d 631 |
. . . . . . 7
⊢ (𝑝 = 𝐴 → ((( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝))) ↔ (( -us ‘𝐴) ∈
No ∧ (𝐴 <s
𝑞 → ( -us ‘𝑞) <s ( -us ‘𝐴))))) |
65 | 58, 64 | imbi12d 344 |
. . . . . 6
⊢ (𝑝 = 𝐴 → ((𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))) ↔ (𝑎 = (( bday
‘𝐴) ∪
( bday ‘𝑞)) → (( -us ‘𝐴) ∈ No
∧ (𝐴 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝐴)))))) |
66 | | fveq2 6839 |
. . . . . . . . 9
⊢ (𝑞 = 𝐵 → ( bday
‘𝑞) = ( bday ‘𝐵)) |
67 | 66 | uneq2d 4121 |
. . . . . . . 8
⊢ (𝑞 = 𝐵 → (( bday
‘𝐴) ∪
( bday ‘𝑞)) = (( bday
‘𝐴) ∪
( bday ‘𝐵))) |
68 | 67 | eqeq2d 2748 |
. . . . . . 7
⊢ (𝑞 = 𝐵 → (𝑎 = (( bday
‘𝐴) ∪
( bday ‘𝑞)) ↔ 𝑎 = (( bday
‘𝐴) ∪
( bday ‘𝐵)))) |
69 | | breq2 5107 |
. . . . . . . . 9
⊢ (𝑞 = 𝐵 → (𝐴 <s 𝑞 ↔ 𝐴 <s 𝐵)) |
70 | | fveq2 6839 |
. . . . . . . . . 10
⊢ (𝑞 = 𝐵 → ( -us ‘𝑞) = ( -us ‘𝐵)) |
71 | 70 | breq1d 5113 |
. . . . . . . . 9
⊢ (𝑞 = 𝐵 → (( -us ‘𝑞) <s ( -us ‘𝐴) ↔ ( -us ‘𝐵) <s ( -us ‘𝐴))) |
72 | 69, 71 | imbi12d 344 |
. . . . . . . 8
⊢ (𝑞 = 𝐵 → ((𝐴 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝐴)) ↔ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))) |
73 | 72 | anbi2d 629 |
. . . . . . 7
⊢ (𝑞 = 𝐵 → ((( -us ‘𝐴) ∈ No
∧ (𝐴 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝐴))) ↔ (( -us ‘𝐴) ∈
No ∧ (𝐴 <s
𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴))))) |
74 | 68, 73 | imbi12d 344 |
. . . . . 6
⊢ (𝑞 = 𝐵 → ((𝑎 = (( bday
‘𝐴) ∪
( bday ‘𝑞)) → (( -us ‘𝐴) ∈ No
∧ (𝐴 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝐴)))) ↔ (𝑎 = (( bday
‘𝐴) ∪
( bday ‘𝐵)) → (( -us ‘𝐴) ∈ No
∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))))) |
75 | 65, 74 | rspc2v 3588 |
. . . . 5
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (∀𝑝 ∈ No
∀𝑞 ∈ No (𝑎 = (( bday
‘𝑝) ∪
( bday ‘𝑞)) → (( -us ‘𝑝) ∈ No
∧ (𝑝 <s 𝑞 → ( -us ‘𝑞) <s ( -us ‘𝑝)))) → (𝑎 = (( bday
‘𝐴) ∪
( bday ‘𝐵)) → (( -us ‘𝐴) ∈ No
∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))))) |
76 | 55, 75 | syl5com 31 |
. . . 4
⊢ (𝑎 ∈ On → ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (𝑎 = (( bday
‘𝐴) ∪
( bday ‘𝐵)) → (( -us ‘𝐴) ∈ No
∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))))) |
77 | 76 | com23 86 |
. . 3
⊢ (𝑎 ∈ On → (𝑎 = (( bday
‘𝐴) ∪
( bday ‘𝐵)) → ((𝐴 ∈ No
∧ 𝐵 ∈ No ) → (( -us ‘𝐴) ∈ No
∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))))) |
78 | 77 | rexlimiv 3143 |
. 2
⊢
(∃𝑎 ∈ On
𝑎 = (( bday ‘𝐴) ∪ ( bday
‘𝐵)) →
((𝐴 ∈ No ∧ 𝐵 ∈ No )
→ (( -us ‘𝐴)
∈ No ∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴))))) |
79 | 5, 78 | ax-mp 5 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → (( -us ‘𝐴) ∈ No
∧ (𝐴 <s 𝐵 → ( -us ‘𝐵) <s ( -us ‘𝐴)))) |