| 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 27737 | . . 3
⊢ (((𝐴 ∈ 
No  ∧ 𝐵 ∈
 No ) ∧ (( bday
‘𝐴) = ( bday ‘𝐵) ∧ 𝐴 <s 𝐵)) → ∃𝑑 ∈  No 
(( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵)) | 
| 6 | 1, 2, 3, 4, 5 | syl22anc 839 | . 2
⊢ (𝜑 → ∃𝑑 ∈  No 
(( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵)) | 
| 7 |  | negsproplem.1 | . . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈  No 
∀𝑦 ∈  No  ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥)
∈  No  ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥))))) | 
| 8 |  | uncom 4158 | . . . . . . . . . 10
⊢ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) = (( bday ‘𝐵) ∪ ( bday
‘𝐴)) | 
| 9 | 8 | eleq2i 2833 | . . . . . . . . 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 3128 | . . . . . . 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 218 | . . . . . 6
⊢ (𝜑 → ∀𝑥 ∈  No 
∀𝑦 ∈  No  ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐵) ∪ ( bday
‘𝐴)) → ((
-us ‘𝑥)
∈  No  ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥))))) | 
| 13 | 12, 2 | negsproplem3 28062 | . . . . 5
⊢ (𝜑 → (( -us
‘𝐵) ∈  No  ∧ ( -us “ ( R ‘𝐵)) <<s {( -us
‘𝐵)} ∧ {(
-us ‘𝐵)}
<<s ( -us “ ( L ‘𝐵)))) | 
| 14 | 13 | simp1d 1143 | . . . 4
⊢ (𝜑 → ( -us
‘𝐵) ∈  No ) | 
| 15 | 14 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐵) ∈ 
No ) | 
| 16 | 7 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ∀𝑥 ∈  No 
∀𝑦 ∈  No  ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥)
∈  No  ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥))))) | 
| 17 |  | simprl 771 | . . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 ∈  No
) | 
| 18 |  | 0sno 27871 | . . . . . 6
⊢ 
0s ∈  No | 
| 19 | 18 | a1i 11 | . . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 0s ∈  No ) | 
| 20 |  | bday0s 27873 | . . . . . . . 8
⊢ ( bday ‘ 0s ) = ∅ | 
| 21 | 20 | uneq2i 4165 | . . . . . . 7
⊢ (( bday ‘𝑑) ∪ ( bday
‘ 0s )) = (( bday
‘𝑑) ∪
∅) | 
| 22 |  | un0 4394 | . . . . . . 7
⊢ (( bday ‘𝑑) ∪ ∅) = (
bday ‘𝑑) | 
| 23 | 21, 22 | eqtri 2765 | . . . . . 6
⊢ (( bday ‘𝑑) ∪ ( bday
‘ 0s )) = ( bday
‘𝑑) | 
| 24 |  | simprr1 1222 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( bday
‘𝑑) ∈
( bday ‘𝐴)) | 
| 25 |  | elun1 4182 | . . . . . . 7
⊢ (( bday ‘𝑑) ∈ ( bday
‘𝐴) →
( bday ‘𝑑) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵))) | 
| 26 | 24, 25 | syl 17 | . . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( bday
‘𝑑) ∈
(( bday ‘𝐴) ∪ ( bday
‘𝐵))) | 
| 27 | 23, 26 | eqeltrid 2845 | . . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → (( bday
‘𝑑) ∪
( bday ‘ 0s )) ∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵))) | 
| 28 | 16, 17, 19, 27 | negsproplem1 28060 | . . . 4
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → (( -us ‘𝑑) ∈ 
No  ∧ (𝑑 <s
0s → ( -us ‘ 0s ) <s (
-us ‘𝑑)))) | 
| 29 | 28 | simpld 494 | . . 3
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝑑) ∈ 
No ) | 
| 30 | 7, 1 | negsproplem3 28062 | . . . . 5
⊢ (𝜑 → (( -us
‘𝐴) ∈  No  ∧ ( -us “ ( R ‘𝐴)) <<s {( -us
‘𝐴)} ∧ {(
-us ‘𝐴)}
<<s ( -us “ ( L ‘𝐴)))) | 
| 31 | 30 | simp1d 1143 | . . . 4
⊢ (𝜑 → ( -us
‘𝐴) ∈  No ) | 
| 32 | 31 | adantr 480 | . . 3
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐴) ∈ 
No ) | 
| 33 | 13 | simp3d 1145 | . . . . 5
⊢ (𝜑 → {( -us
‘𝐵)} <<s (
-us “ ( L ‘𝐵))) | 
| 34 | 33 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → {( -us ‘𝐵)} <<s ( -us
“ ( L ‘𝐵))) | 
| 35 |  | fvex 6919 | . . . . . 6
⊢ (
-us ‘𝐵)
∈ V | 
| 36 | 35 | snid 4662 | . . . . 5
⊢ (
-us ‘𝐵)
∈ {( -us ‘𝐵)} | 
| 37 | 36 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐵) ∈ {( -us
‘𝐵)}) | 
| 38 |  | negsfn 28055 | . . . . 5
⊢ 
-us Fn  No | 
| 39 |  | leftssno 27919 | . . . . 5
⊢ ( L
‘𝐵) ⊆  No | 
| 40 |  | bdayelon 27821 | . . . . . . . . 9
⊢ ( bday ‘𝐴) ∈ On | 
| 41 |  | oldbday 27939 | . . . . . . . . 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 257 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 ∈ ( O ‘(
bday ‘𝐴))) | 
| 44 | 3 | fveq2d 6910 | . . . . . . . 8
⊢ (𝜑 → ( O ‘( bday ‘𝐴)) = ( O ‘( bday
‘𝐵))) | 
| 45 | 44 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( O ‘( bday ‘𝐴)) = ( O ‘( bday
‘𝐵))) | 
| 46 | 43, 45 | eleqtrd 2843 | . . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 ∈ ( O ‘(
bday ‘𝐵))) | 
| 47 |  | simprr3 1224 | . . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 <s 𝐵) | 
| 48 |  | leftval 27902 | . . . . . . 7
⊢ ( L
‘𝐵) = {𝑑 ∈ ( O ‘( bday ‘𝐵)) ∣ 𝑑 <s 𝐵} | 
| 49 | 48 | reqabi 3460 | . . . . . 6
⊢ (𝑑 ∈ ( L ‘𝐵) ↔ (𝑑 ∈ ( O ‘(
bday ‘𝐵))
∧ 𝑑 <s 𝐵)) | 
| 50 | 46, 47, 49 | sylanbrc 583 | . . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 ∈ ( L ‘𝐵)) | 
| 51 |  | fnfvima 7253 | . . . . 5
⊢ ((
-us Fn  No  ∧ ( L ‘𝐵) ⊆ 
No  ∧ 𝑑 ∈ (
L ‘𝐵)) → (
-us ‘𝑑)
∈ ( -us “ ( L ‘𝐵))) | 
| 52 | 38, 39, 50, 51 | mp3an12i 1467 | . . . 4
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝑑) ∈ ( -us
“ ( L ‘𝐵))) | 
| 53 | 34, 37, 52 | ssltsepcd 27839 | . . 3
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐵) <s ( -us
‘𝑑)) | 
| 54 | 30 | simp2d 1144 | . . . . 5
⊢ (𝜑 → ( -us “ (
R ‘𝐴)) <<s {(
-us ‘𝐴)}) | 
| 55 | 54 | adantr 480 | . . . 4
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us “ ( R
‘𝐴)) <<s {(
-us ‘𝐴)}) | 
| 56 |  | rightssno 27920 | . . . . 5
⊢ ( R
‘𝐴) ⊆  No | 
| 57 |  | simprr2 1223 | . . . . . 6
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝐴 <s 𝑑) | 
| 58 |  | rightval 27903 | . . . . . . 7
⊢ ( R
‘𝐴) = {𝑑 ∈ ( O ‘( bday ‘𝐴)) ∣ 𝐴 <s 𝑑} | 
| 59 | 58 | reqabi 3460 | . . . . . 6
⊢ (𝑑 ∈ ( R ‘𝐴) ↔ (𝑑 ∈ ( O ‘(
bday ‘𝐴))
∧ 𝐴 <s 𝑑)) | 
| 60 | 43, 57, 59 | sylanbrc 583 | . . . . 5
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → 𝑑 ∈ ( R ‘𝐴)) | 
| 61 |  | fnfvima 7253 | . . . . 5
⊢ ((
-us Fn  No  ∧ ( R ‘𝐴) ⊆ 
No  ∧ 𝑑 ∈ (
R ‘𝐴)) → (
-us ‘𝑑)
∈ ( -us “ ( R ‘𝐴))) | 
| 62 | 38, 56, 60, 61 | mp3an12i 1467 | . . . 4
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝑑) ∈ ( -us
“ ( R ‘𝐴))) | 
| 63 |  | fvex 6919 | . . . . . 6
⊢ (
-us ‘𝐴)
∈ V | 
| 64 | 63 | snid 4662 | . . . . 5
⊢ (
-us ‘𝐴)
∈ {( -us ‘𝐴)} | 
| 65 | 64 | a1i 11 | . . . 4
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐴) ∈ {( -us
‘𝐴)}) | 
| 66 | 55, 62, 65 | ssltsepcd 27839 | . . 3
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝑑) <s ( -us
‘𝐴)) | 
| 67 | 15, 29, 32, 53, 66 | slttrd 27804 | . 2
⊢ ((𝜑 ∧ (𝑑 ∈  No 
∧ (( bday ‘𝑑) ∈ ( bday
‘𝐴) ∧
𝐴 <s 𝑑 ∧ 𝑑 <s 𝐵))) → ( -us ‘𝐵) <s ( -us
‘𝐴)) | 
| 68 | 6, 67 | rexlimddv 3161 | 1
⊢ (𝜑 → ( -us
‘𝐵) <s (
-us ‘𝐴)) |