Step | Hyp | Ref
| Expression |
1 | | negsproplem4.1 |
. . 3
⊢ (𝜑 → 𝐴 ∈ No
) |
2 | | negsproplem4.2 |
. . 3
⊢ (𝜑 → 𝐵 ∈ No
) |
3 | | negsproplem6.4 |
. . 3
⊢ (𝜑 → (
bday ‘𝐴) =
( bday ‘𝐵)) |
4 | | negsproplem4.3 |
. . 3
⊢ (𝜑 → 𝐴 <s 𝐵) |
5 | | nodense 26991 |
. . 3
⊢ (((𝐴 ∈
No ∧ 𝐵 ∈
No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∃𝑑 ∈ No
(( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵)) |
6 | 1, 2, 3, 4, 5 | syl22anc 837 |
. 2
⊢ (𝜑 → ∃𝑑 ∈ No
(( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵)) |
7 | | negsproplem.1 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
8 | | uncom 4111 |
. . . . . . . . . 10
⊢ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) = (( bday ‘𝐵) ∪ ( bday
‘𝐴)) |
9 | 8 | eleq2i 2829 |
. . . . . . . . 9
⊢ ((( bday ‘𝑥) ∪ ( bday
‘𝑦)) ∈
(( bday ‘𝐴) ∪ ( bday
‘𝐵)) ↔
(( bday ‘𝑥) ∪ ( bday
‘𝑦)) ∈
(( bday ‘𝐵) ∪ ( bday
‘𝐴))) |
10 | 9 | imbi1i 349 |
. . . . . . . 8
⊢ (((( bday ‘𝑥) ∪ ( bday
‘𝑦)) ∈
(( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) ↔ ((( bday
‘𝑥) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝐵) ∪
( bday ‘𝐴)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
11 | 10 | 2ralbii 3125 |
. . . . . . 7
⊢
(∀𝑥 ∈
No ∀𝑦 ∈ No
((( bday ‘𝑥) ∪ ( bday
‘𝑦)) ∈
(( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥)))) ↔ ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐵) ∪ ( bday
‘𝐴)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
12 | 7, 11 | sylib 217 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐵) ∪ ( bday
‘𝐴)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
13 | 12, 2 | negsproplem3 34316 |
. . . . 5
⊢ (𝜑 → (( -us ‘𝐵) ∈
No ∧ ( -us “ ( R ‘𝐵)) <<s {( -us ‘𝐵)} ∧ {( -us ‘𝐵)} <<s ( -us “ ( L ‘𝐵)))) |
14 | 13 | simp1d 1142 |
. . . 4
⊢ (𝜑 → ( -us ‘𝐵) ∈
No ) |
15 | 14 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐵) ∈ No
) |
16 | 7 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ∀𝑥 ∈ No
∀𝑦 ∈ No ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥) ∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
17 | | simprl 769 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 ∈ No
) |
18 | | 0sno 27116 |
. . . . . 6
⊢ 0s
∈ No |
19 | 18 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 0s ∈
No ) |
20 | | bday0s 27118 |
. . . . . . . 8
⊢ ( bday ‘ 0s ) = ∅ |
21 | 20 | uneq2i 4118 |
. . . . . . 7
⊢ (( bday ‘𝑑) ∪ ( bday
‘ 0s )) = (( bday ‘𝑑) ∪
∅) |
22 | | un0 4348 |
. . . . . . 7
⊢ (( bday ‘𝑑) ∪ ∅) = (
bday ‘𝑑) |
23 | 21, 22 | eqtri 2765 |
. . . . . 6
⊢ (( bday ‘𝑑) ∪ ( bday
‘ 0s )) = ( bday ‘𝑑) |
24 | | simprr1 1221 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( bday
‘𝑑) ∈
( bday ‘𝐴)) |
25 | | elun1 4134 |
. . . . . . 7
⊢ (( bday ‘𝑑) ∈ ( bday
‘𝐴) →
( bday ‘𝑑) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵))) |
26 | 24, 25 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( bday
‘𝑑) ∈
(( bday ‘𝐴) ∪ ( bday
‘𝐵))) |
27 | 23, 26 | eqeltrid 2842 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → (( bday
‘𝑑) ∪
( bday ‘ 0s )) ∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵))) |
28 | 16, 17, 19, 27 | negsproplem1 34314 |
. . . 4
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → (( -us ‘𝑑) ∈ No
∧ (𝑑 <s 0s → (
-us ‘ 0s ) <s ( -us ‘𝑑)))) |
29 | 28 | simpld 495 |
. . 3
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝑑) ∈ No
) |
30 | 7, 1 | negsproplem3 34316 |
. . . . 5
⊢ (𝜑 → (( -us ‘𝐴) ∈
No ∧ ( -us “ ( R ‘𝐴)) <<s {( -us ‘𝐴)} ∧ {( -us ‘𝐴)} <<s ( -us “ ( L ‘𝐴)))) |
31 | 30 | simp1d 1142 |
. . . 4
⊢ (𝜑 → ( -us ‘𝐴) ∈
No ) |
32 | 31 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐴) ∈ No
) |
33 | 13 | simp3d 1144 |
. . . . 5
⊢ (𝜑 → {( -us ‘𝐵)} <<s ( -us “ ( L
‘𝐵))) |
34 | 33 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → {( -us ‘𝐵)} <<s ( -us “ ( L ‘𝐵))) |
35 | | fvex 6852 |
. . . . . 6
⊢ ( -us
‘𝐵) ∈
V |
36 | 35 | snid 4620 |
. . . . 5
⊢ ( -us
‘𝐵) ∈ {( -us
‘𝐵)} |
37 | 36 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐵) ∈ {( -us ‘𝐵)}) |
38 | | negsfn 34310 |
. . . . 5
⊢ -us Fn
No |
39 | | leftssno 27160 |
. . . . 5
⊢ ( L
‘𝐵) ⊆ No |
40 | | bdayelon 27067 |
. . . . . . . . 9
⊢ ( bday ‘𝐴) ∈ On |
41 | | oldbday 27178 |
. . . . . . . . 9
⊢ ((( bday ‘𝐴) ∈ On ∧ 𝑑 ∈ No )
→ (𝑑 ∈ ( O
‘( bday ‘𝐴)) ↔ ( bday
‘𝑑) ∈
( bday ‘𝐴))) |
42 | 40, 17, 41 | sylancr 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → (𝑑 ∈ ( O ‘(
bday ‘𝐴))
↔ ( bday ‘𝑑) ∈ ( bday
‘𝐴))) |
43 | 24, 42 | mpbird 256 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 ∈ ( O ‘(
bday ‘𝐴))) |
44 | 3 | fveq2d 6843 |
. . . . . . . 8
⊢ (𝜑 → ( O ‘( bday ‘𝐴)) = ( O ‘( bday
‘𝐵))) |
45 | 44 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( O ‘( bday ‘𝐴)) = ( O ‘( bday
‘𝐵))) |
46 | 43, 45 | eleqtrd 2840 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 ∈ ( O ‘(
bday ‘𝐵))) |
47 | | simprr3 1223 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 <s 𝐵) |
48 | | leftval 27144 |
. . . . . . 7
⊢ ( L
‘𝐵) = {𝑑 ∈ ( O ‘( bday ‘𝐵)) ∣ 𝑑 <s 𝐵} |
49 | 48 | rabeq2i 3427 |
. . . . . 6
⊢ (𝑑 ∈ ( L ‘𝐵) ↔ (𝑑 ∈ ( O ‘(
bday ‘𝐵))
∧ 𝑑 <s 𝐵)) |
50 | 46, 47, 49 | sylanbrc 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 ∈ ( L ‘𝐵)) |
51 | | fnfvima 7179 |
. . . . 5
⊢ (( -us Fn
No ∧ ( L ‘𝐵) ⊆ No
∧ 𝑑 ∈ ( L
‘𝐵)) → ( -us
‘𝑑) ∈ ( -us
“ ( L ‘𝐵))) |
52 | 38, 39, 50, 51 | mp3an12i 1465 |
. . . 4
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝑑) ∈ ( -us “ ( L ‘𝐵))) |
53 | 34, 37, 52 | ssltsepcd 27084 |
. . 3
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐵) <s ( -us ‘𝑑)) |
54 | 30 | simp2d 1143 |
. . . . 5
⊢ (𝜑 → ( -us “ ( R
‘𝐴)) <<s {( -us
‘𝐴)}) |
55 | 54 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us “ ( R ‘𝐴)) <<s {( -us ‘𝐴)}) |
56 | | rightssno 27161 |
. . . . 5
⊢ ( R
‘𝐴) ⊆ No |
57 | | simprr2 1222 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝐴 <s 𝑑) |
58 | | rightval 27145 |
. . . . . . 7
⊢ ( R
‘𝐴) = {𝑑 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑑} |
59 | 58 | rabeq2i 3427 |
. . . . . 6
⊢ (𝑑 ∈ ( R ‘𝐴) ↔ (𝑑 ∈ ( O ‘(
bday ‘𝐴))
∧ 𝐴 <s 𝑑)) |
60 | 43, 57, 59 | sylanbrc 583 |
. . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 ∈ ( R ‘𝐴)) |
61 | | fnfvima 7179 |
. . . . 5
⊢ (( -us Fn
No ∧ ( R ‘𝐴) ⊆ No
∧ 𝑑 ∈ ( R
‘𝐴)) → ( -us
‘𝑑) ∈ ( -us
“ ( R ‘𝐴))) |
62 | 38, 56, 60, 61 | mp3an12i 1465 |
. . . 4
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝑑) ∈ ( -us “ ( R ‘𝐴))) |
63 | | fvex 6852 |
. . . . . 6
⊢ ( -us
‘𝐴) ∈
V |
64 | 63 | snid 4620 |
. . . . 5
⊢ ( -us
‘𝐴) ∈ {( -us
‘𝐴)} |
65 | 64 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐴) ∈ {( -us ‘𝐴)}) |
66 | 55, 62, 65 | ssltsepcd 27084 |
. . 3
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝑑) <s ( -us ‘𝐴)) |
67 | 15, 29, 32, 53, 66 | slttrd 27058 |
. 2
⊢ ((𝜑 ∧ (𝑑 ∈ No
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐵) <s ( -us ‘𝐴)) |
68 | 6, 67 | rexlimddv 3156 |
1
⊢ (𝜑 → ( -us ‘𝐵) <s ( -us ‘𝐴)) |