| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | negsfn 28056 | . . . 4
⊢ 
-us Fn  No | 
| 2 |  | fnfun 6667 | . . . 4
⊢ (
-us Fn  No  → Fun -us
) | 
| 3 | 1, 2 | ax-mp 5 | . . 3
⊢ Fun
-us | 
| 4 |  | fvex 6918 | . . . 4
⊢ ( R
‘𝐴) ∈
V | 
| 5 | 4 | funimaex 6654 | . . 3
⊢ (Fun
-us → ( -us “ ( R ‘𝐴)) ∈ V) | 
| 6 | 3, 5 | mp1i 13 | . 2
⊢ (𝜑 → ( -us “ (
R ‘𝐴)) ∈
V) | 
| 7 |  | fvex 6918 | . . . 4
⊢ ( L
‘𝐴) ∈
V | 
| 8 | 7 | funimaex 6654 | . . 3
⊢ (Fun
-us → ( -us “ ( L ‘𝐴)) ∈ V) | 
| 9 | 3, 8 | mp1i 13 | . 2
⊢ (𝜑 → ( -us “ (
L ‘𝐴)) ∈
V) | 
| 10 |  | rightssold 27919 | . . . 4
⊢ ( R
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) | 
| 11 |  | imass2 6119 | . . . 4
⊢ (( R
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) → ( -us “ ( R
‘𝐴)) ⊆ (
-us “ ( O ‘( bday
‘𝐴)))) | 
| 12 | 10, 11 | ax-mp 5 | . . 3
⊢ (
-us “ ( R ‘𝐴)) ⊆ ( -us “ ( O
‘( bday ‘𝐴))) | 
| 13 |  | negsproplem.1 | . . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈  No 
∀𝑦 ∈  No  ((( bday ‘𝑥) ∪ (
bday ‘𝑦))
∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥)
∈  No  ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥))))) | 
| 14 | 13 | adantr 480 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ ∀𝑥 ∈
 No  ∀𝑦 ∈  No 
((( bday ‘𝑥) ∪ ( bday
‘𝑦)) ∈
(( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥)
∈  No  ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥))))) | 
| 15 |  | oldssno 27901 | . . . . . . . . 9
⊢ ( O
‘( bday ‘𝐴)) ⊆  No | 
| 16 | 15 | sseli 3978 | . . . . . . . 8
⊢ (𝑎 ∈ ( O ‘( bday ‘𝐴)) → 𝑎 ∈  No
) | 
| 17 | 16 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ 𝑎 ∈  No ) | 
| 18 |  | 0sno 27872 | . . . . . . . 8
⊢ 
0s ∈  No | 
| 19 | 18 | a1i 11 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ 0s ∈  No ) | 
| 20 |  | bday0s 27874 | . . . . . . . . . 10
⊢ ( bday ‘ 0s ) = ∅ | 
| 21 | 20 | uneq2i 4164 | . . . . . . . . 9
⊢ (( bday ‘𝑎) ∪ ( bday
‘ 0s )) = (( bday
‘𝑎) ∪
∅) | 
| 22 |  | un0 4393 | . . . . . . . . 9
⊢ (( bday ‘𝑎) ∪ ∅) = (
bday ‘𝑎) | 
| 23 | 21, 22 | eqtri 2764 | . . . . . . . 8
⊢ (( bday ‘𝑎) ∪ ( bday
‘ 0s )) = ( bday
‘𝑎) | 
| 24 |  | oldbdayim 27928 | . . . . . . . . . 10
⊢ (𝑎 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑎) ∈
( bday ‘𝐴)) | 
| 25 | 24 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ ( bday ‘𝑎) ∈ ( bday
‘𝐴)) | 
| 26 |  | elun1 4181 | . . . . . . . . 9
⊢ (( bday ‘𝑎) ∈ ( bday
‘𝐴) →
( bday ‘𝑎) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵))) | 
| 27 | 25, 26 | syl 17 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ ( bday ‘𝑎) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵))) | 
| 28 | 23, 27 | eqeltrid 2844 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ (( bday ‘𝑎) ∪ ( bday
‘ 0s )) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵))) | 
| 29 | 14, 17, 19, 28 | negsproplem1 28061 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ (( -us ‘𝑎) ∈  No 
∧ (𝑎 <s
0s → ( -us ‘ 0s ) <s (
-us ‘𝑎)))) | 
| 30 | 29 | simpld 494 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ ( -us ‘𝑎) ∈  No
) | 
| 31 | 30 | ralrimiva 3145 | . . . 4
⊢ (𝜑 → ∀𝑎 ∈ ( O ‘(
bday ‘𝐴))(
-us ‘𝑎)
∈  No ) | 
| 32 | 1 | fndmi 6671 | . . . . . 6
⊢ dom
-us =  No | 
| 33 | 15, 32 | sseqtrri 4032 | . . . . 5
⊢ ( O
‘( bday ‘𝐴)) ⊆ dom
-us | 
| 34 |  | funimass4 6972 | . . . . 5
⊢ ((Fun
-us ∧ ( O ‘( bday
‘𝐴)) ⊆
dom -us ) → (( -us “ ( O ‘( bday ‘𝐴))) ⊆  No
 ↔ ∀𝑎
∈ ( O ‘( bday ‘𝐴))( -us ‘𝑎) ∈  No
)) | 
| 35 | 3, 33, 34 | mp2an 692 | . . . 4
⊢ ((
-us “ ( O ‘( bday
‘𝐴))) ⊆
 No  ↔ ∀𝑎 ∈ ( O ‘(
bday ‘𝐴))(
-us ‘𝑎)
∈  No ) | 
| 36 | 31, 35 | sylibr 234 | . . 3
⊢ (𝜑 → ( -us “ (
O ‘( bday ‘𝐴))) ⊆  No
) | 
| 37 | 12, 36 | sstrid 3994 | . 2
⊢ (𝜑 → ( -us “ (
R ‘𝐴)) ⊆  No ) | 
| 38 |  | leftssold 27918 | . . . 4
⊢ ( L
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) | 
| 39 |  | imass2 6119 | . . . 4
⊢ (( L
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) → ( -us “ ( L
‘𝐴)) ⊆ (
-us “ ( O ‘( bday
‘𝐴)))) | 
| 40 | 38, 39 | ax-mp 5 | . . 3
⊢ (
-us “ ( L ‘𝐴)) ⊆ ( -us “ ( O
‘( bday ‘𝐴))) | 
| 41 | 40, 36 | sstrid 3994 | . 2
⊢ (𝜑 → ( -us “ (
L ‘𝐴)) ⊆  No ) | 
| 42 |  | rightssno 27921 | . . . . . . 7
⊢ ( R
‘𝐴) ⊆  No | 
| 43 |  | fvelimab 6980 | . . . . . . 7
⊢ ((
-us Fn  No  ∧ ( R ‘𝐴) ⊆ 
No ) → (𝑎
∈ ( -us “ ( R ‘𝐴)) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)( -us ‘𝑥𝑅) = 𝑎)) | 
| 44 | 1, 42, 43 | mp2an 692 | . . . . . 6
⊢ (𝑎 ∈ ( -us “
( R ‘𝐴)) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)( -us ‘𝑥𝑅) = 𝑎) | 
| 45 |  | leftssno 27920 | . . . . . . 7
⊢ ( L
‘𝐴) ⊆  No | 
| 46 |  | fvelimab 6980 | . . . . . . 7
⊢ ((
-us Fn  No  ∧ ( L ‘𝐴) ⊆ 
No ) → (𝑏
∈ ( -us “ ( L ‘𝐴)) ↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)( -us ‘𝑥𝐿) = 𝑏)) | 
| 47 | 1, 45, 46 | mp2an 692 | . . . . . 6
⊢ (𝑏 ∈ ( -us “
( L ‘𝐴)) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)( -us ‘𝑥𝐿) = 𝑏) | 
| 48 | 44, 47 | anbi12i 628 | . . . . 5
⊢ ((𝑎 ∈ ( -us “
( R ‘𝐴)) ∧ 𝑏 ∈ ( -us “
( L ‘𝐴))) ↔
(∃𝑥𝑅 ∈ ( R ‘𝐴)( -us ‘𝑥𝑅) = 𝑎 ∧ ∃𝑥𝐿 ∈ ( L ‘𝐴)( -us ‘𝑥𝐿) = 𝑏)) | 
| 49 |  | reeanv 3228 | . . . . 5
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑥𝐿 ∈ ( L ‘𝐴)(( -us ‘𝑥𝑅) = 𝑎 ∧ ( -us
‘𝑥𝐿) = 𝑏) ↔ (∃𝑥𝑅 ∈ ( R ‘𝐴)( -us ‘𝑥𝑅) = 𝑎 ∧ ∃𝑥𝐿 ∈ ( L ‘𝐴)( -us ‘𝑥𝐿) = 𝑏)) | 
| 50 | 48, 49 | bitr4i 278 | . . . 4
⊢ ((𝑎 ∈ ( -us “
( R ‘𝐴)) ∧ 𝑏 ∈ ( -us “
( L ‘𝐴))) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑥𝐿 ∈ ( L ‘𝐴)(( -us ‘𝑥𝑅) = 𝑎 ∧ ( -us
‘𝑥𝐿) = 𝑏)) | 
| 51 |  | lltropt 27912 | . . . . . . . . 9
⊢ ( L
‘𝐴) <<s ( R
‘𝐴) | 
| 52 | 51 | a1i 11 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ( L ‘𝐴) <<s ( R ‘𝐴)) | 
| 53 |  | simprr 772 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 ∈ ( L ‘𝐴)) | 
| 54 |  | simprl 770 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝑅 ∈ ( R ‘𝐴)) | 
| 55 | 52, 53, 54 | ssltsepcd 27840 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 <s 𝑥𝑅) | 
| 56 | 13 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ∀𝑥 ∈ 
No  ∀𝑦 ∈
 No  ((( bday
‘𝑥) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵)) → (( -us ‘𝑥) ∈ 
No  ∧ (𝑥 <s
𝑦 → ( -us
‘𝑦) <s (
-us ‘𝑥))))) | 
| 57 | 45 | sseli 3978 | . . . . . . . . . 10
⊢ (𝑥𝐿 ∈ ( L
‘𝐴) → 𝑥𝐿 ∈
 No ) | 
| 58 | 57 | ad2antll 729 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 ∈  No ) | 
| 59 | 42 | sseli 3978 | . . . . . . . . . . 11
⊢ (𝑥𝑅 ∈ ( R
‘𝐴) → 𝑥𝑅 ∈
 No ) | 
| 60 | 59 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑥𝑅 ∈ ( R
‘𝐴) ∧ 𝑥𝐿 ∈ ( L
‘𝐴)) → 𝑥𝑅 ∈
 No ) | 
| 61 | 60 | adantl 481 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝑅 ∈  No ) | 
| 62 | 38 | sseli 3978 | . . . . . . . . . . . . 13
⊢ (𝑥𝐿 ∈ ( L
‘𝐴) → 𝑥𝐿 ∈ ( O
‘( bday ‘𝐴))) | 
| 63 | 62 | ad2antll 729 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 ∈ ( O ‘( bday ‘𝐴))) | 
| 64 |  | oldbdayim 27928 | . . . . . . . . . . . 12
⊢ (𝑥𝐿 ∈ ( O
‘( bday ‘𝐴)) → ( bday
‘𝑥𝐿) ∈ ( bday ‘𝐴)) | 
| 65 | 63, 64 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ( bday ‘𝑥𝐿) ∈ ( bday ‘𝐴)) | 
| 66 | 10 | a1i 11 | . . . . . . . . . . . . . 14
⊢ (𝜑 → ( R ‘𝐴) ⊆ ( O ‘( bday ‘𝐴))) | 
| 67 | 66 | sselda 3982 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ ( O ‘( bday ‘𝐴))) | 
| 68 | 67 | adantrr 717 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝑅 ∈ ( O ‘( bday ‘𝐴))) | 
| 69 |  | oldbdayim 27928 | . . . . . . . . . . . 12
⊢ (𝑥𝑅 ∈ ( O
‘( bday ‘𝐴)) → ( bday
‘𝑥𝑅) ∈ ( bday ‘𝐴)) | 
| 70 | 68, 69 | syl 17 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ( bday ‘𝑥𝑅) ∈ ( bday ‘𝐴)) | 
| 71 |  | bdayelon 27822 | . . . . . . . . . . . 12
⊢ ( bday ‘𝑥𝐿) ∈
On | 
| 72 |  | bdayelon 27822 | . . . . . . . . . . . 12
⊢ ( bday ‘𝑥𝑅) ∈
On | 
| 73 |  | bdayelon 27822 | . . . . . . . . . . . 12
⊢ ( bday ‘𝐴) ∈ On | 
| 74 |  | onunel 6488 | . . . . . . . . . . . 12
⊢ ((( bday ‘𝑥𝐿) ∈ On ∧ ( bday ‘𝑥𝑅) ∈ On ∧ ( bday ‘𝐴) ∈ On) → ((( bday ‘𝑥𝐿) ∪ ( bday ‘𝑥𝑅)) ∈ ( bday ‘𝐴) ↔ (( bday
‘𝑥𝐿) ∈ ( bday ‘𝐴) ∧ ( bday
‘𝑥𝑅) ∈ ( bday ‘𝐴)))) | 
| 75 | 71, 72, 73, 74 | mp3an 1462 | . . . . . . . . . . 11
⊢ ((( bday ‘𝑥𝐿) ∪ ( bday ‘𝑥𝑅)) ∈ ( bday ‘𝐴) ↔ (( bday
‘𝑥𝐿) ∈ ( bday ‘𝐴) ∧ ( bday
‘𝑥𝑅) ∈ ( bday ‘𝐴))) | 
| 76 | 65, 70, 75 | sylanbrc 583 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → (( bday ‘𝑥𝐿) ∪ ( bday ‘𝑥𝑅)) ∈ ( bday ‘𝐴)) | 
| 77 |  | elun1 4181 | . . . . . . . . . 10
⊢ ((( bday ‘𝑥𝐿) ∪ ( bday ‘𝑥𝑅)) ∈ ( bday ‘𝐴) → (( bday
‘𝑥𝐿) ∪ ( bday ‘𝑥𝑅)) ∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵))) | 
| 78 | 76, 77 | syl 17 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → (( bday ‘𝑥𝐿) ∪ ( bday ‘𝑥𝑅)) ∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵))) | 
| 79 | 56, 58, 61, 78 | negsproplem1 28061 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → (( -us
‘𝑥𝐿) ∈  No  ∧ (𝑥𝐿 <s 𝑥𝑅 → ( -us
‘𝑥𝑅) <s ( -us
‘𝑥𝐿)))) | 
| 80 | 79 | simprd 495 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → (𝑥𝐿 <s 𝑥𝑅 → ( -us
‘𝑥𝑅) <s ( -us
‘𝑥𝐿))) | 
| 81 | 55, 80 | mpd 15 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ( -us
‘𝑥𝑅) <s ( -us
‘𝑥𝐿)) | 
| 82 |  | breq12 5147 | . . . . . 6
⊢ (((
-us ‘𝑥𝑅) = 𝑎 ∧ ( -us ‘𝑥𝐿) = 𝑏) → (( -us
‘𝑥𝑅) <s ( -us
‘𝑥𝐿) ↔ 𝑎 <s 𝑏)) | 
| 83 | 81, 82 | syl5ibcom 245 | . . . . 5
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ((( -us
‘𝑥𝑅) = 𝑎 ∧ ( -us ‘𝑥𝐿) = 𝑏) → 𝑎 <s 𝑏)) | 
| 84 | 83 | rexlimdvva 3212 | . . . 4
⊢ (𝜑 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑥𝐿 ∈ ( L ‘𝐴)(( -us ‘𝑥𝑅) = 𝑎 ∧ ( -us
‘𝑥𝐿) = 𝑏) → 𝑎 <s 𝑏)) | 
| 85 | 50, 84 | biimtrid 242 | . . 3
⊢ (𝜑 → ((𝑎 ∈ ( -us “ ( R
‘𝐴)) ∧ 𝑏 ∈ ( -us “
( L ‘𝐴))) →
𝑎 <s 𝑏)) | 
| 86 | 85 | 3impib 1116 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ ( -us “ ( R
‘𝐴)) ∧ 𝑏 ∈ ( -us “
( L ‘𝐴))) →
𝑎 <s 𝑏) | 
| 87 | 6, 9, 37, 41, 86 | ssltd 27837 | 1
⊢ (𝜑 → ( -us “ (
R ‘𝐴)) <<s (
-us “ ( L ‘𝐴))) |