Step | Hyp | Ref
| Expression |
1 | | negsfn 34310 |
. . . 4
⊢ -us Fn
No |
2 | | fnfun 6599 |
. . . 4
⊢ ( -us Fn
No → Fun -us ) |
3 | 1, 2 | ax-mp 5 |
. . 3
⊢ Fun
-us |
4 | | fvex 6852 |
. . . 4
⊢ ( R
‘𝐴) ∈
V |
5 | 4 | funimaex 6586 |
. . 3
⊢ (Fun -us
→ ( -us “ ( R ‘𝐴)) ∈ V) |
6 | 3, 5 | mp1i 13 |
. 2
⊢ (𝜑 → ( -us “ ( R
‘𝐴)) ∈
V) |
7 | | fvex 6852 |
. . . 4
⊢ ( L
‘𝐴) ∈
V |
8 | 7 | funimaex 6586 |
. . 3
⊢ (Fun -us
→ ( -us “ ( L ‘𝐴)) ∈ V) |
9 | 3, 8 | mp1i 13 |
. 2
⊢ (𝜑 → ( -us “ ( L
‘𝐴)) ∈
V) |
10 | | rightssold 27159 |
. . . 4
⊢ ( R
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) |
11 | | imass2 6052 |
. . . 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 27142 |
. . . . . . . . 9
⊢ ( O
‘( bday ‘𝐴)) ⊆ No
|
16 | 15 | sseli 3938 |
. . . . . . . 8
⊢ (𝑎 ∈ ( O ‘( bday ‘𝐴)) → 𝑎 ∈ No
) |
17 | 16 | adantl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ 𝑎 ∈ No ) |
18 | | 0sno 27116 |
. . . . . . . 8
⊢ 0s
∈ No |
19 | 18 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ 0s ∈ No ) |
20 | | bday0s 27118 |
. . . . . . . . . 10
⊢ ( bday ‘ 0s ) = ∅ |
21 | 20 | uneq2i 4118 |
. . . . . . . . 9
⊢ (( bday ‘𝑎) ∪ ( bday
‘ 0s )) = (( bday ‘𝑎) ∪
∅) |
22 | | un0 4348 |
. . . . . . . . 9
⊢ (( bday ‘𝑎) ∪ ∅) = (
bday ‘𝑎) |
23 | 21, 22 | eqtri 2765 |
. . . . . . . 8
⊢ (( bday ‘𝑎) ∪ ( bday
‘ 0s )) = ( bday ‘𝑎) |
24 | | oldbdayim 27168 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ( O ‘( bday ‘𝐴)) → ( bday
‘𝑎) ∈
( bday ‘𝐴)) |
25 | 24 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ ( bday ‘𝑎) ∈ ( bday
‘𝐴)) |
26 | | elun1 4134 |
. . . . . . . . 9
⊢ (( bday ‘𝑎) ∈ ( bday
‘𝐴) →
( bday ‘𝑎) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵))) |
27 | 25, 26 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ ( bday ‘𝑎) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵))) |
28 | 23, 27 | eqeltrid 2842 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ (( bday ‘𝑎) ∪ ( bday
‘ 0s )) ∈ (( bday ‘𝐴) ∪ (
bday ‘𝐵))) |
29 | 14, 17, 19, 28 | negsproplem1 34314 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ (( -us ‘𝑎)
∈ No ∧ (𝑎 <s 0s → ( -us ‘ 0s ) <s (
-us ‘𝑎)))) |
30 | 29 | simpld 495 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ ( O ‘(
bday ‘𝐴)))
→ ( -us ‘𝑎)
∈ No ) |
31 | 30 | ralrimiva 3141 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ ( O ‘(
bday ‘𝐴))( -us
‘𝑎) ∈ No ) |
32 | 1 | fndmi 6603 |
. . . . . 6
⊢ dom -us =
No |
33 | 15, 32 | sseqtrri 3979 |
. . . . 5
⊢ ( O
‘( bday ‘𝐴)) ⊆ dom -us |
34 | | funimass4 6904 |
. . . . 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 3953 |
. 2
⊢ (𝜑 → ( -us “ ( R
‘𝐴)) ⊆ No ) |
38 | | leftssold 27158 |
. . . 4
⊢ ( L
‘𝐴) ⊆ ( O
‘( bday ‘𝐴)) |
39 | | imass2 6052 |
. . . 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 3953 |
. 2
⊢ (𝜑 → ( -us “ ( L
‘𝐴)) ⊆ No ) |
42 | | rightssno 27161 |
. . . . . . 7
⊢ ( R
‘𝐴) ⊆ No |
43 | | fvelimab 6911 |
. . . . . . 7
⊢ (( -us Fn
No ∧ ( R ‘𝐴) ⊆ No )
→ (𝑎 ∈ ( -us
“ ( R ‘𝐴))
↔ ∃𝑥R
∈ ( R ‘𝐴)( -us
‘𝑥R) =
𝑎)) |
44 | 1, 42, 43 | mp2an 690 |
. . . . . 6
⊢ (𝑎 ∈ ( -us “ ( R
‘𝐴)) ↔
∃𝑥R ∈
( R ‘𝐴)( -us
‘𝑥R) =
𝑎) |
45 | | leftssno 27160 |
. . . . . . 7
⊢ ( L
‘𝐴) ⊆ No |
46 | | fvelimab 6911 |
. . . . . . 7
⊢ (( -us Fn
No ∧ ( L ‘𝐴) ⊆ No )
→ (𝑏 ∈ ( -us
“ ( L ‘𝐴))
↔ ∃𝑥L
∈ ( L ‘𝐴)( -us
‘𝑥L) =
𝑏)) |
47 | 1, 45, 46 | mp2an 690 |
. . . . . 6
⊢ (𝑏 ∈ ( -us “ ( L
‘𝐴)) ↔
∃𝑥L ∈
( L ‘𝐴)( -us
‘𝑥L) =
𝑏) |
48 | 44, 47 | anbi12i 627 |
. . . . 5
⊢ ((𝑎 ∈ ( -us “ ( R
‘𝐴)) ∧ 𝑏 ∈ ( -us “ ( L
‘𝐴))) ↔
(∃𝑥R
∈ ( R ‘𝐴)( -us
‘𝑥R) =
𝑎 ∧ ∃𝑥L ∈ ( L
‘𝐴)( -us ‘𝑥L) = 𝑏)) |
49 | | reeanv 3215 |
. . . . 5
⊢
(∃𝑥R ∈ ( R ‘𝐴)∃𝑥L ∈ ( L ‘𝐴)(( -us ‘𝑥R) = 𝑎 ∧ ( -us ‘𝑥L) = 𝑏) ↔ (∃𝑥R ∈ ( R
‘𝐴)( -us ‘𝑥R) = 𝑎 ∧ ∃𝑥L ∈ ( L ‘𝐴)( -us ‘𝑥L) = 𝑏)) |
50 | 48, 49 | bitr4i 277 |
. . . 4
⊢ ((𝑎 ∈ ( -us “ ( R
‘𝐴)) ∧ 𝑏 ∈ ( -us “ ( L
‘𝐴))) ↔
∃𝑥R ∈
( R ‘𝐴)∃𝑥L ∈ ( L
‘𝐴)(( -us
‘𝑥R) =
𝑎 ∧ ( -us ‘𝑥L) = 𝑏)) |
51 | | negsproplem2.1 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐴 ∈ No
) |
52 | | lltropt 27153 |
. . . . . . . . . 10
⊢ (𝐴 ∈
No → ( L ‘𝐴) <<s ( R ‘𝐴)) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ( L ‘𝐴) <<s ( R ‘𝐴)) |
54 | 53 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → ( L ‘𝐴) <<s ( R ‘𝐴)) |
55 | | simprr 771 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → 𝑥L ∈ ( L ‘𝐴)) |
56 | | simprl 769 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → 𝑥R ∈ ( R ‘𝐴)) |
57 | 54, 55, 56 | ssltsepcd 27084 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → 𝑥L <s 𝑥R) |
58 | 13 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → ∀𝑥 ∈
No ∀𝑦 ∈
No ((( bday
‘𝑥) ∪
( bday ‘𝑦)) ∈ (( bday
‘𝐴) ∪
( bday ‘𝐵)) → (( -us ‘𝑥) ∈ No
∧ (𝑥 <s 𝑦 → ( -us ‘𝑦) <s ( -us ‘𝑥))))) |
59 | 45 | sseli 3938 |
. . . . . . . . . 10
⊢ (𝑥L ∈ ( L
‘𝐴) → 𝑥L ∈ No ) |
60 | 59 | ad2antll 727 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → 𝑥L ∈ No
) |
61 | 42 | sseli 3938 |
. . . . . . . . . . 11
⊢ (𝑥R ∈ ( R
‘𝐴) → 𝑥R ∈ No ) |
62 | 61 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝑥R ∈ ( R
‘𝐴) ∧ 𝑥L ∈ ( L
‘𝐴)) → 𝑥R ∈ No ) |
63 | 62 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → 𝑥R ∈ No
) |
64 | 38 | sseli 3938 |
. . . . . . . . . . . . 13
⊢ (𝑥L ∈ ( L
‘𝐴) → 𝑥L ∈ ( O
‘( bday ‘𝐴))) |
65 | 64 | ad2antll 727 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → 𝑥L ∈ ( O ‘( bday ‘𝐴))) |
66 | | oldbdayim 27168 |
. . . . . . . . . . . 12
⊢ (𝑥L ∈ ( O
‘( bday ‘𝐴)) → ( bday
‘𝑥L) ∈ (
bday ‘𝐴)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → ( bday ‘𝑥L) ∈ (
bday ‘𝐴)) |
68 | 10 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ( R ‘𝐴) ⊆ ( O ‘( bday ‘𝐴))) |
69 | 68 | sselda 3942 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥R ∈ ( R ‘𝐴)) → 𝑥R ∈ ( O ‘( bday ‘𝐴))) |
70 | 69 | adantrr 715 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → 𝑥R ∈ ( O ‘( bday ‘𝐴))) |
71 | | oldbdayim 27168 |
. . . . . . . . . . . 12
⊢ (𝑥R ∈ ( O
‘( bday ‘𝐴)) → ( bday
‘𝑥R) ∈ (
bday ‘𝐴)) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → ( bday ‘𝑥R) ∈ (
bday ‘𝐴)) |
73 | | bdayelon 27067 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝑥L) ∈ On |
74 | | bdayelon 27067 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝑥R) ∈ On |
75 | | bdayelon 27067 |
. . . . . . . . . . . 12
⊢ ( bday ‘𝐴) ∈ On |
76 | | onunel 34103 |
. . . . . . . . . . . 12
⊢ ((( bday ‘𝑥L) ∈ On ∧ ( bday ‘𝑥R) ∈ On ∧ ( bday ‘𝐴) ∈ On) → ((( bday ‘𝑥L) ∪ (
bday ‘𝑥R)) ∈ (
bday ‘𝐴)
↔ (( bday ‘𝑥L) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑥R) ∈ (
bday ‘𝐴)))) |
77 | 73, 74, 75, 76 | mp3an 1461 |
. . . . . . . . . . 11
⊢ ((( bday ‘𝑥L) ∪ (
bday ‘𝑥R)) ∈ (
bday ‘𝐴)
↔ (( bday ‘𝑥L) ∈ (
bday ‘𝐴) ∧
( bday ‘𝑥R) ∈ (
bday ‘𝐴))) |
78 | 67, 72, 77 | sylanbrc 583 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → (( bday ‘𝑥L) ∪ (
bday ‘𝑥R)) ∈ (
bday ‘𝐴)) |
79 | | elun1 4134 |
. . . . . . . . . 10
⊢ ((( bday ‘𝑥L) ∪ (
bday ‘𝑥R)) ∈ (
bday ‘𝐴)
→ (( bday ‘𝑥L) ∪ (
bday ‘𝑥R)) ∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵))) |
80 | 78, 79 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → (( bday ‘𝑥L) ∪ (
bday ‘𝑥R)) ∈ (( bday ‘𝐴) ∪ ( bday
‘𝐵))) |
81 | 58, 60, 63, 80 | negsproplem1 34314 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → (( -us ‘𝑥L) ∈ No ∧ (𝑥L <s 𝑥R → ( -us ‘𝑥R) <s ( -us
‘𝑥L)))) |
82 | 81 | simprd 496 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → (𝑥L <s 𝑥R → ( -us ‘𝑥R) <s ( -us
‘𝑥L))) |
83 | 57, 82 | mpd 15 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → ( -us ‘𝑥R) <s ( -us
‘𝑥L)) |
84 | | breq12 5108 |
. . . . . 6
⊢ ((( -us
‘𝑥R) =
𝑎 ∧ ( -us ‘𝑥L) = 𝑏) → (( -us ‘𝑥R) <s ( -us
‘𝑥L)
↔ 𝑎 <s 𝑏)) |
85 | 83, 84 | syl5ibcom 244 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥R ∈ ( R ‘𝐴) ∧ 𝑥L ∈ ( L ‘𝐴))) → ((( -us ‘𝑥R) = 𝑎 ∧ ( -us ‘𝑥L) = 𝑏) → 𝑎 <s 𝑏)) |
86 | 85 | rexlimdvva 3203 |
. . . 4
⊢ (𝜑 → (∃𝑥R ∈ ( R ‘𝐴)∃𝑥L ∈ ( L ‘𝐴)(( -us ‘𝑥R) = 𝑎 ∧ ( -us ‘𝑥L) = 𝑏) → 𝑎 <s 𝑏)) |
87 | 50, 86 | biimtrid 241 |
. . 3
⊢ (𝜑 → ((𝑎 ∈ ( -us “ ( R ‘𝐴)) ∧ 𝑏 ∈ ( -us “ ( L ‘𝐴))) → 𝑎 <s 𝑏)) |
88 | 87 | 3impib 1116 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ ( -us “ ( R ‘𝐴)) ∧ 𝑏 ∈ ( -us “ ( L ‘𝐴))) → 𝑎 <s 𝑏) |
89 | 6, 9, 37, 41, 88 | ssltd 27082 |
1
⊢ (𝜑 → ( -us “ ( R
‘𝐴)) <<s ( -us
“ ( L ‘𝐴))) |