Step | Hyp | Ref
| Expression |
1 | | negsfn 27380 |
. . . 4
⊢
-us Fn No |
2 | | fnfun 6622 |
. . . 4
⊢ (
-us Fn No → Fun -us
) |
3 | 1, 2 | ax-mp 5 |
. . 3
⊢ Fun
-us |
4 | | fvex 6875 |
. . . 4
⊢ ( R
‘𝐴) ∈
V |
5 | 4 | funimaex 6609 |
. . 3
⊢ (Fun
-us → ( -us “ ( R ‘𝐴)) ∈ V) |
6 | 3, 5 | mp1i 13 |
. 2
⊢ (𝜑 → ( -us “ (
R ‘𝐴)) ∈
V) |
7 | | fvex 6875 |
. . . 4
⊢ ( L
‘𝐴) ∈
V |
8 | 7 | funimaex 6609 |
. . 3
⊢ (Fun
-us → ( -us “ ( L ‘𝐴)) ∈ V) |
9 | 3, 8 | mp1i 13 |
. 2
⊢ (𝜑 → ( -us “ (
L ‘𝐴)) ∈
V) |
10 | | rightssold 27267 |
. . . 4
⊢ ( R
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) |
11 | | imass2 6074 |
. . . 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 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ ∀𝑥 ∈
No ∀𝑦 ∈ No
((( bday ‘𝑥) ∪ ( bday
‘𝑦)) ∈
(( bday ‘𝐴) ∪ ( bday
‘𝐵)) → ((
-us ‘𝑥)
∈ No ∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us
‘𝑥))))) |
15 | | oldssno 27249 |
. . . . . . . . 9
⊢ ( O
‘( bday ‘𝐴)) ⊆ No
|
16 | 15 | sseli 3958 |
. . . . . . . 8
⊢ (𝑎 ∈ ( O ‘( bday ‘𝐴)) → 𝑎 ∈ No
) |
17 | 16 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ 𝑎 ∈ No ) |
18 | | 0sno 27223 |
. . . . . . . 8
⊢
0s ∈ No |
19 | 18 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ 0s ∈ No ) |
20 | | bday0s 27225 |
. . . . . . . . . 10
⊢ ( bday ‘ 0s ) = ∅ |
21 | 20 | uneq2i 4140 |
. . . . . . . . 9
⊢ (( bday ‘𝑎) ∪ ( bday
‘ 0s )) = (( bday
‘𝑎) ∪
∅) |
22 | | un0 4370 |
. . . . . . . . 9
⊢ (( bday ‘𝑎) ∪ ∅) = (
bday ‘𝑎) |
23 | 21, 22 | eqtri 2759 |
. . . . . . . 8
⊢ (( bday ‘𝑎) ∪ ( bday
‘ 0s )) = ( bday
‘𝑎) |
24 | | oldbdayim 27276 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑎) ∈
( bday ‘𝐴)) |
25 | 24 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ ( bday ‘𝑎) ∈ ( bday
‘𝐴)) |
26 | | elun1 4156 |
. . . . . . . . 9
⊢ (( bday ‘𝑎) ∈ ( bday
‘𝐴) →
( bday ‘𝑎) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵))) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ ( bday ‘𝑎) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵))) |
28 | 23, 27 | eqeltrid 2836 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ (( bday ‘𝑎) ∪ ( bday
‘ 0s )) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵))) |
29 | 14, 17, 19, 28 | negsproplem1 27384 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ (( -us ‘𝑎) ∈ No
∧ (𝑎 <s
0s → ( -us ‘ 0s ) <s (
-us ‘𝑎)))) |
30 | 29 | simpld 495 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ ( -us ‘𝑎) ∈ No
) |
31 | 30 | ralrimiva 3145 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ ( O ‘(
bday ‘𝐴))(
-us ‘𝑎)
∈ No ) |
32 | 1 | fndmi 6626 |
. . . . . 6
⊢ dom
-us = No |
33 | 15, 32 | sseqtrri 3999 |
. . . . 5
⊢ ( O
‘( bday ‘𝐴)) ⊆ dom
-us |
34 | | funimass4 6927 |
. . . . 5
⊢ ((Fun
-us ∧ ( O ‘( bday
‘𝐴)) ⊆
dom -us ) → (( -us “ ( O ‘( bday ‘𝐴))) ⊆ No
↔ ∀𝑎
∈ ( O ‘( bday ‘𝐴))( -us ‘𝑎) ∈ No
)) |
35 | 3, 33, 34 | mp2an 690 |
. . . 4
⊢ ((
-us “ ( O ‘( bday
‘𝐴))) ⊆
No ↔ ∀𝑎 ∈ ( O ‘(
bday ‘𝐴))(
-us ‘𝑎)
∈ No ) |
36 | 31, 35 | sylibr 233 |
. . 3
⊢ (𝜑 → ( -us “ (
O ‘( bday ‘𝐴))) ⊆ No
) |
37 | 12, 36 | sstrid 3973 |
. 2
⊢ (𝜑 → ( -us “ (
R ‘𝐴)) ⊆ No ) |
38 | | leftssold 27266 |
. . . 4
⊢ ( L
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) |
39 | | imass2 6074 |
. . . 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 3973 |
. 2
⊢ (𝜑 → ( -us “ (
L ‘𝐴)) ⊆ No ) |
42 | | rightssno 27269 |
. . . . . . 7
⊢ ( R
‘𝐴) ⊆ No |
43 | | fvelimab 6934 |
. . . . . . 7
⊢ ((
-us Fn No ∧ ( R ‘𝐴) ⊆
No ) → (𝑎
∈ ( -us “ ( R ‘𝐴)) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)( -us ‘𝑥𝑅) = 𝑎)) |
44 | 1, 42, 43 | mp2an 690 |
. . . . . 6
⊢ (𝑎 ∈ ( -us “
( R ‘𝐴)) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)( -us ‘𝑥𝑅) = 𝑎) |
45 | | leftssno 27268 |
. . . . . . 7
⊢ ( L
‘𝐴) ⊆ No |
46 | | fvelimab 6934 |
. . . . . . 7
⊢ ((
-us Fn No ∧ ( L ‘𝐴) ⊆
No ) → (𝑏
∈ ( -us “ ( L ‘𝐴)) ↔ ∃𝑥𝐿 ∈ ( L ‘𝐴)( -us ‘𝑥𝐿) = 𝑏)) |
47 | 1, 45, 46 | mp2an 690 |
. . . . . 6
⊢ (𝑏 ∈ ( -us “
( L ‘𝐴)) ↔
∃𝑥𝐿 ∈ ( L ‘𝐴)( -us ‘𝑥𝐿) = 𝑏) |
48 | 44, 47 | anbi12i 627 |
. . . . 5
⊢ ((𝑎 ∈ ( -us “
( R ‘𝐴)) ∧ 𝑏 ∈ ( -us “
( L ‘𝐴))) ↔
(∃𝑥𝑅 ∈ ( R ‘𝐴)( -us ‘𝑥𝑅) = 𝑎 ∧ ∃𝑥𝐿 ∈ ( L ‘𝐴)( -us ‘𝑥𝐿) = 𝑏)) |
49 | | reeanv 3225 |
. . . . 5
⊢
(∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑥𝐿 ∈ ( L ‘𝐴)(( -us ‘𝑥𝑅) = 𝑎 ∧ ( -us
‘𝑥𝐿) = 𝑏) ↔ (∃𝑥𝑅 ∈ ( R ‘𝐴)( -us ‘𝑥𝑅) = 𝑎 ∧ ∃𝑥𝐿 ∈ ( L ‘𝐴)( -us ‘𝑥𝐿) = 𝑏)) |
50 | 48, 49 | bitr4i 277 |
. . . 4
⊢ ((𝑎 ∈ ( -us “
( R ‘𝐴)) ∧ 𝑏 ∈ ( -us “
( L ‘𝐴))) ↔
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑥𝐿 ∈ ( L ‘𝐴)(( -us ‘𝑥𝑅) = 𝑎 ∧ ( -us
‘𝑥𝐿) = 𝑏)) |
51 | | lltropt 27260 |
. . . . . . . . 9
⊢ ( L
‘𝐴) <<s ( R
‘𝐴) |
52 | 51 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ( L ‘𝐴) <<s ( R ‘𝐴)) |
53 | | simprr 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 ∈ ( L ‘𝐴)) |
54 | | simprl 769 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝑅 ∈ ( R ‘𝐴)) |
55 | 52, 53, 54 | ssltsepcd 27191 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 <s 𝑥𝑅) |
56 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ∀𝑥 ∈
No ∀𝑦 ∈
No ((( bday
‘𝑥) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵)) → (( -us ‘𝑥) ∈
No ∧ (𝑥 <s
𝑦 → ( -us
‘𝑦) <s (
-us ‘𝑥))))) |
57 | 45 | sseli 3958 |
. . . . . . . . . 10
⊢ (𝑥𝐿 ∈ ( L
‘𝐴) → 𝑥𝐿 ∈
No ) |
58 | 57 | ad2antll 727 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 ∈ No ) |
59 | 42 | sseli 3958 |
. . . . . . . . . . 11
⊢ (𝑥𝑅 ∈ ( R
‘𝐴) → 𝑥𝑅 ∈
No ) |
60 | 59 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑥𝑅 ∈ ( R
‘𝐴) ∧ 𝑥𝐿 ∈ ( L
‘𝐴)) → 𝑥𝑅 ∈
No ) |
61 | 60 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝑅 ∈ No ) |
62 | 38 | sseli 3958 |
. . . . . . . . . . . . 13
⊢ (𝑥𝐿 ∈ ( L
‘𝐴) → 𝑥𝐿 ∈ ( O
‘( bday ‘𝐴))) |
63 | 62 | ad2antll 727 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝐿 ∈ ( O ‘( bday ‘𝐴))) |
64 | | oldbdayim 27276 |
. . . . . . . . . . . 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 3962 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥𝑅 ∈ ( R ‘𝐴)) → 𝑥𝑅 ∈ ( O ‘( bday ‘𝐴))) |
68 | 67 | adantrr 715 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → 𝑥𝑅 ∈ ( O ‘( bday ‘𝐴))) |
69 | | oldbdayim 27276 |
. . . . . . . . . . . 12
⊢ (𝑥𝑅 ∈ ( O
‘( bday ‘𝐴)) → ( bday
‘𝑥𝑅) ∈ ( bday ‘𝐴)) |
70 | 68, 69 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ( bday ‘𝑥𝑅) ∈ ( bday ‘𝐴)) |
71 | | bdayelon 27174 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝑥𝐿) ∈
On |
72 | | bdayelon 27174 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝑥𝑅) ∈
On |
73 | | bdayelon 27174 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝐴) ∈ On |
74 | | onunel 6442 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑥𝐿) ∈ On ∧ ( bday ‘𝑥𝑅) ∈ On ∧ ( bday ‘𝐴) ∈ On) → ((( bday ‘𝑥𝐿) ∪ ( bday ‘𝑥𝑅)) ∈ ( bday ‘𝐴) ↔ (( bday
‘𝑥𝐿) ∈ ( bday ‘𝐴) ∧ ( bday
‘𝑥𝑅) ∈ ( bday ‘𝐴)))) |
75 | 71, 72, 73, 74 | mp3an 1461 |
. . . . . . . . . . 11
⊢ ((( bday ‘𝑥𝐿) ∪ ( bday ‘𝑥𝑅)) ∈ ( bday ‘𝐴) ↔ (( bday
‘𝑥𝐿) ∈ ( bday ‘𝐴) ∧ ( bday
‘𝑥𝑅) ∈ ( bday ‘𝐴))) |
76 | 65, 70, 75 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → (( bday ‘𝑥𝐿) ∪ ( bday ‘𝑥𝑅)) ∈ ( bday ‘𝐴)) |
77 | | elun1 4156 |
. . . . . . . . . 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 27384 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → (( -us
‘𝑥𝐿) ∈ No ∧ (𝑥𝐿 <s 𝑥𝑅 → ( -us
‘𝑥𝑅) <s ( -us
‘𝑥𝐿)))) |
80 | 79 | simprd 496 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → (𝑥𝐿 <s 𝑥𝑅 → ( -us
‘𝑥𝑅) <s ( -us
‘𝑥𝐿))) |
81 | 55, 80 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ( -us
‘𝑥𝑅) <s ( -us
‘𝑥𝐿)) |
82 | | breq12 5130 |
. . . . . 6
⊢ (((
-us ‘𝑥𝑅) = 𝑎 ∧ ( -us ‘𝑥𝐿) = 𝑏) → (( -us
‘𝑥𝑅) <s ( -us
‘𝑥𝐿) ↔ 𝑎 <s 𝑏)) |
83 | 81, 82 | syl5ibcom 244 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥𝑅 ∈ ( R ‘𝐴) ∧ 𝑥𝐿 ∈ ( L ‘𝐴))) → ((( -us
‘𝑥𝑅) = 𝑎 ∧ ( -us ‘𝑥𝐿) = 𝑏) → 𝑎 <s 𝑏)) |
84 | 83 | rexlimdvva 3210 |
. . . 4
⊢ (𝜑 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑥𝐿 ∈ ( L ‘𝐴)(( -us ‘𝑥𝑅) = 𝑎 ∧ ( -us
‘𝑥𝐿) = 𝑏) → 𝑎 <s 𝑏)) |
85 | 50, 84 | biimtrid 241 |
. . 3
⊢ (𝜑 → ((𝑎 ∈ ( -us “ ( R
‘𝐴)) ∧ 𝑏 ∈ ( -us “
( L ‘𝐴))) →
𝑎 <s 𝑏)) |
86 | 85 | 3impib 1116 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ ( -us “ ( R
‘𝐴)) ∧ 𝑏 ∈ ( -us “
( L ‘𝐴))) →
𝑎 <s 𝑏) |
87 | 6, 9, 37, 41, 86 | ssltd 27189 |
1
⊢ (𝜑 → ( -us “ (
R ‘𝐴)) <<s (
-us “ ( L ‘𝐴))) |