Step | Hyp | Ref
| Expression |
1 | | negsunif.2 |
. . . 4
⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅)) |
2 | | negsunif.1 |
. . . . 5
⊢ (𝜑 → 𝐿 <<s 𝑅) |
3 | 2 | scutcld 27230 |
. . . 4
⊢ (𝜑 → (𝐿 |s 𝑅) ∈ No
) |
4 | 1, 3 | eqeltrd 2832 |
. . 3
⊢ (𝜑 → 𝐴 ∈ No
) |
5 | | negsval 27416 |
. . 3
⊢ (𝐴 ∈
No → ( -us ‘𝐴) = (( -us “ ( R
‘𝐴)) |s (
-us “ ( L ‘𝐴)))) |
6 | 4, 5 | syl 17 |
. 2
⊢ (𝜑 → ( -us
‘𝐴) = ((
-us “ ( R ‘𝐴)) |s ( -us “ ( L
‘𝐴)))) |
7 | | negscut2 27430 |
. . . 4
⊢ (𝐴 ∈
No → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L
‘𝐴))) |
8 | 4, 7 | syl 17 |
. . 3
⊢ (𝜑 → ( -us “ (
R ‘𝐴)) <<s (
-us “ ( L ‘𝐴))) |
9 | 2, 1 | cofcutr2d 27333 |
. . . . 5
⊢ (𝜑 → ∀𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ 𝑅 𝑑 ≤s 𝑐) |
10 | | negsfn 27414 |
. . . . . . . 8
⊢
-us Fn No |
11 | | ssltss2 27217 |
. . . . . . . . 9
⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆ No
) |
12 | 2, 11 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝑅 ⊆ No
) |
13 | | breq2 5145 |
. . . . . . . . 9
⊢ (𝑏 = ( -us ‘𝑑) → (( -us
‘𝑐) ≤s 𝑏 ↔ ( -us
‘𝑐) ≤s (
-us ‘𝑑))) |
14 | 13 | imaeqsexv 7344 |
. . . . . . . 8
⊢ ((
-us Fn No ∧ 𝑅 ⊆ No )
→ (∃𝑏 ∈ (
-us “ 𝑅)(
-us ‘𝑐)
≤s 𝑏 ↔ ∃𝑑 ∈ 𝑅 ( -us ‘𝑐) ≤s ( -us ‘𝑑))) |
15 | 10, 12, 14 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏 ↔ ∃𝑑 ∈ 𝑅 ( -us ‘𝑐) ≤s ( -us ‘𝑑))) |
16 | 15 | ralbidv 3176 |
. . . . . 6
⊢ (𝜑 → (∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ 𝑅 ( -us ‘𝑐) ≤s ( -us ‘𝑑))) |
17 | 12 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 𝑅 ⊆ No
) |
18 | 17 | sselda 3978 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ 𝑑 ∈ 𝑅) → 𝑑 ∈ No
) |
19 | | rightssno 27299 |
. . . . . . . . . . 11
⊢ ( R
‘𝐴) ⊆ No |
20 | 19 | sseli 3974 |
. . . . . . . . . 10
⊢ (𝑐 ∈ ( R ‘𝐴) → 𝑐 ∈ No
) |
21 | 20 | ad2antlr 725 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ 𝑑 ∈ 𝑅) → 𝑐 ∈ No
) |
22 | | sleneg 27436 |
. . . . . . . . 9
⊢ ((𝑑 ∈
No ∧ 𝑐 ∈
No ) → (𝑑 ≤s 𝑐 ↔ ( -us ‘𝑐) ≤s ( -us
‘𝑑))) |
23 | 18, 21, 22 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ 𝑑 ∈ 𝑅) → (𝑑 ≤s 𝑐 ↔ ( -us ‘𝑐) ≤s ( -us
‘𝑑))) |
24 | 23 | rexbidva 3175 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → (∃𝑑 ∈ 𝑅 𝑑 ≤s 𝑐 ↔ ∃𝑑 ∈ 𝑅 ( -us ‘𝑐) ≤s ( -us ‘𝑑))) |
25 | 24 | ralbidva 3174 |
. . . . . 6
⊢ (𝜑 → (∀𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ 𝑅 𝑑 ≤s 𝑐 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ 𝑅 ( -us ‘𝑐) ≤s ( -us ‘𝑑))) |
26 | 16, 25 | bitr4d 281 |
. . . . 5
⊢ (𝜑 → (∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ 𝑅 𝑑 ≤s 𝑐)) |
27 | 9, 26 | mpbird 256 |
. . . 4
⊢ (𝜑 → ∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏) |
28 | | breq1 5144 |
. . . . . . 7
⊢ (𝑎 = ( -us ‘𝑐) → (𝑎 ≤s 𝑏 ↔ ( -us ‘𝑐) ≤s 𝑏)) |
29 | 28 | rexbidv 3177 |
. . . . . 6
⊢ (𝑎 = ( -us ‘𝑐) → (∃𝑏 ∈ ( -us “
𝑅)𝑎 ≤s 𝑏 ↔ ∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏)) |
30 | 29 | imaeqsalv 7345 |
. . . . 5
⊢ ((
-us Fn No ∧ ( R ‘𝐴) ⊆
No ) → (∀𝑎 ∈ ( -us “ ( R
‘𝐴))∃𝑏 ∈ ( -us “
𝑅)𝑎 ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏)) |
31 | 10, 19, 30 | mp2an 690 |
. . . 4
⊢
(∀𝑎 ∈ (
-us “ ( R ‘𝐴))∃𝑏 ∈ ( -us “ 𝑅)𝑎 ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏) |
32 | 27, 31 | sylibr 233 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ ( -us “ ( R
‘𝐴))∃𝑏 ∈ ( -us “
𝑅)𝑎 ≤s 𝑏) |
33 | 2, 1 | cofcutr1d 27332 |
. . . . 5
⊢ (𝜑 → ∀𝑐 ∈ ( L ‘𝐴)∃𝑑 ∈ 𝐿 𝑐 ≤s 𝑑) |
34 | | ssltss1 27216 |
. . . . . . . . 9
⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆ No
) |
35 | 2, 34 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐿 ⊆ No
) |
36 | | breq1 5144 |
. . . . . . . . 9
⊢ (𝑏 = ( -us ‘𝑑) → (𝑏 ≤s ( -us ‘𝑐) ↔ ( -us
‘𝑑) ≤s (
-us ‘𝑐))) |
37 | 36 | imaeqsexv 7344 |
. . . . . . . 8
⊢ ((
-us Fn No ∧ 𝐿 ⊆ No )
→ (∃𝑏 ∈ (
-us “ 𝐿)𝑏 ≤s ( -us ‘𝑐) ↔ ∃𝑑 ∈ 𝐿 ( -us ‘𝑑) ≤s ( -us ‘𝑐))) |
38 | 10, 35, 37 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐) ↔ ∃𝑑 ∈ 𝐿 ( -us ‘𝑑) ≤s ( -us ‘𝑐))) |
39 | 38 | ralbidv 3176 |
. . . . . 6
⊢ (𝜑 → (∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐) ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑑 ∈ 𝐿 ( -us ‘𝑑) ≤s ( -us ‘𝑐))) |
40 | | leftssno 27298 |
. . . . . . . . . . 11
⊢ ( L
‘𝐴) ⊆ No |
41 | 40 | sseli 3974 |
. . . . . . . . . 10
⊢ (𝑐 ∈ ( L ‘𝐴) → 𝑐 ∈ No
) |
42 | 41 | ad2antlr 725 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ ( L ‘𝐴)) ∧ 𝑑 ∈ 𝐿) → 𝑐 ∈ No
) |
43 | 35 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ( L ‘𝐴)) → 𝐿 ⊆ No
) |
44 | 43 | sselda 3978 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ ( L ‘𝐴)) ∧ 𝑑 ∈ 𝐿) → 𝑑 ∈ No
) |
45 | | sleneg 27436 |
. . . . . . . . 9
⊢ ((𝑐 ∈
No ∧ 𝑑 ∈
No ) → (𝑐 ≤s 𝑑 ↔ ( -us ‘𝑑) ≤s ( -us
‘𝑐))) |
46 | 42, 44, 45 | syl2anc 584 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ( L ‘𝐴)) ∧ 𝑑 ∈ 𝐿) → (𝑐 ≤s 𝑑 ↔ ( -us ‘𝑑) ≤s ( -us
‘𝑐))) |
47 | 46 | rexbidva 3175 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ( L ‘𝐴)) → (∃𝑑 ∈ 𝐿 𝑐 ≤s 𝑑 ↔ ∃𝑑 ∈ 𝐿 ( -us ‘𝑑) ≤s ( -us ‘𝑐))) |
48 | 47 | ralbidva 3174 |
. . . . . 6
⊢ (𝜑 → (∀𝑐 ∈ ( L ‘𝐴)∃𝑑 ∈ 𝐿 𝑐 ≤s 𝑑 ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑑 ∈ 𝐿 ( -us ‘𝑑) ≤s ( -us ‘𝑐))) |
49 | 39, 48 | bitr4d 281 |
. . . . 5
⊢ (𝜑 → (∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐) ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑑 ∈ 𝐿 𝑐 ≤s 𝑑)) |
50 | 33, 49 | mpbird 256 |
. . . 4
⊢ (𝜑 → ∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐)) |
51 | | breq2 5145 |
. . . . . . 7
⊢ (𝑎 = ( -us ‘𝑐) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s ( -us ‘𝑐))) |
52 | 51 | rexbidv 3177 |
. . . . . 6
⊢ (𝑎 = ( -us ‘𝑐) → (∃𝑏 ∈ ( -us “
𝐿)𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐))) |
53 | 52 | imaeqsalv 7345 |
. . . . 5
⊢ ((
-us Fn No ∧ ( L ‘𝐴) ⊆
No ) → (∀𝑎 ∈ ( -us “ ( L
‘𝐴))∃𝑏 ∈ ( -us “
𝐿)𝑏 ≤s 𝑎 ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐))) |
54 | 10, 40, 53 | mp2an 690 |
. . . 4
⊢
(∀𝑎 ∈ (
-us “ ( L ‘𝐴))∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s 𝑎 ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐)) |
55 | 50, 54 | sylibr 233 |
. . 3
⊢ (𝜑 → ∀𝑎 ∈ ( -us “ ( L
‘𝐴))∃𝑏 ∈ ( -us “
𝐿)𝑏 ≤s 𝑎) |
56 | | fnfun 6638 |
. . . . . . 7
⊢ (
-us Fn No → Fun -us
) |
57 | 10, 56 | ax-mp 5 |
. . . . . 6
⊢ Fun
-us |
58 | | ssltex2 27215 |
. . . . . . 7
⊢ (𝐿 <<s 𝑅 → 𝑅 ∈ V) |
59 | 2, 58 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ V) |
60 | | funimaexg 6623 |
. . . . . 6
⊢ ((Fun
-us ∧ 𝑅
∈ V) → ( -us “ 𝑅) ∈ V) |
61 | 57, 59, 60 | sylancr 587 |
. . . . 5
⊢ (𝜑 → ( -us “
𝑅) ∈
V) |
62 | | snex 5424 |
. . . . . 6
⊢ {(
-us ‘𝐴)}
∈ V |
63 | 62 | a1i 11 |
. . . . 5
⊢ (𝜑 → {( -us
‘𝐴)} ∈
V) |
64 | | imassrn 6060 |
. . . . . . 7
⊢ (
-us “ 𝑅)
⊆ ran -us |
65 | | negsfo 27441 |
. . . . . . . 8
⊢
-us : No –onto→ No
|
66 | | forn 6795 |
. . . . . . . 8
⊢ (
-us : No –onto→ No → ran
-us = No ) |
67 | 65, 66 | ax-mp 5 |
. . . . . . 7
⊢ ran
-us = No |
68 | 64, 67 | sseqtri 4014 |
. . . . . 6
⊢ (
-us “ 𝑅)
⊆ No |
69 | 68 | a1i 11 |
. . . . 5
⊢ (𝜑 → ( -us “
𝑅) ⊆ No ) |
70 | 4 | negscld 27427 |
. . . . . 6
⊢ (𝜑 → ( -us
‘𝐴) ∈ No ) |
71 | 70 | snssd 4805 |
. . . . 5
⊢ (𝜑 → {( -us
‘𝐴)} ⊆ No ) |
72 | | velsn 4638 |
. . . . . . . 8
⊢ (𝑎 ∈ {( -us
‘𝐴)} ↔ 𝑎 = ( -us ‘𝐴)) |
73 | | fvelimab 6950 |
. . . . . . . . . . 11
⊢ ((
-us Fn No ∧ 𝑅 ⊆ No )
→ (𝑏 ∈ (
-us “ 𝑅)
↔ ∃𝑑 ∈
𝑅 ( -us
‘𝑑) = 𝑏)) |
74 | 10, 12, 73 | sylancr 587 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑏 ∈ ( -us “ 𝑅) ↔ ∃𝑑 ∈ 𝑅 ( -us ‘𝑑) = 𝑏)) |
75 | 1 | sneqd 4634 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝐴} = {(𝐿 |s 𝑅)}) |
76 | 75 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → {𝐴} = {(𝐿 |s 𝑅)}) |
77 | | scutcut 27228 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐿 <<s 𝑅 → ((𝐿 |s 𝑅) ∈ No
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) |
78 | 2, 77 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 |s 𝑅) ∈ No
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) |
79 | 78 | simp3d 1144 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → {(𝐿 |s 𝑅)} <<s 𝑅) |
80 | 79 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → {(𝐿 |s 𝑅)} <<s 𝑅) |
81 | 76, 80 | eqbrtrd 5163 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → {𝐴} <<s 𝑅) |
82 | | snidg 4656 |
. . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈
No → 𝐴 ∈
{𝐴}) |
83 | 4, 82 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ {𝐴}) |
84 | 83 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝐴 ∈ {𝐴}) |
85 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝑑 ∈ 𝑅) |
86 | 81, 84, 85 | ssltsepcd 27221 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝐴 <s 𝑑) |
87 | 4 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝐴 ∈ No
) |
88 | 12 | sselda 3978 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝑑 ∈ No
) |
89 | | sltneg 27435 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈
No ∧ 𝑑 ∈
No ) → (𝐴 <s 𝑑 ↔ ( -us ‘𝑑) <s ( -us
‘𝐴))) |
90 | 87, 88, 89 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → (𝐴 <s 𝑑 ↔ ( -us ‘𝑑) <s ( -us
‘𝐴))) |
91 | 86, 90 | mpbid 231 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → ( -us ‘𝑑) <s ( -us
‘𝐴)) |
92 | | breq1 5144 |
. . . . . . . . . . . 12
⊢ ((
-us ‘𝑑) =
𝑏 → (( -us
‘𝑑) <s (
-us ‘𝐴)
↔ 𝑏 <s (
-us ‘𝐴))) |
93 | 91, 92 | syl5ibcom 244 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → (( -us ‘𝑑) = 𝑏 → 𝑏 <s ( -us ‘𝐴))) |
94 | 93 | rexlimdva 3154 |
. . . . . . . . . 10
⊢ (𝜑 → (∃𝑑 ∈ 𝑅 ( -us ‘𝑑) = 𝑏 → 𝑏 <s ( -us ‘𝐴))) |
95 | 74, 94 | sylbid 239 |
. . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s ( -us ‘𝐴))) |
96 | | breq2 5145 |
. . . . . . . . . 10
⊢ (𝑎 = ( -us ‘𝐴) → (𝑏 <s 𝑎 ↔ 𝑏 <s ( -us ‘𝐴))) |
97 | 96 | imbi2d 340 |
. . . . . . . . 9
⊢ (𝑎 = ( -us ‘𝐴) → ((𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s 𝑎) ↔ (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s ( -us ‘𝐴)))) |
98 | 95, 97 | syl5ibrcom 246 |
. . . . . . . 8
⊢ (𝜑 → (𝑎 = ( -us ‘𝐴) → (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s 𝑎))) |
99 | 72, 98 | biimtrid 241 |
. . . . . . 7
⊢ (𝜑 → (𝑎 ∈ {( -us ‘𝐴)} → (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s 𝑎))) |
100 | 99 | 3imp 1111 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ {( -us ‘𝐴)} ∧ 𝑏 ∈ ( -us “ 𝑅)) → 𝑏 <s 𝑎) |
101 | 100 | 3com23 1126 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ ( -us “ 𝑅) ∧ 𝑎 ∈ {( -us ‘𝐴)}) → 𝑏 <s 𝑎) |
102 | 61, 63, 69, 71, 101 | ssltd 27219 |
. . . 4
⊢ (𝜑 → ( -us “
𝑅) <<s {(
-us ‘𝐴)}) |
103 | 6 | sneqd 4634 |
. . . 4
⊢ (𝜑 → {( -us
‘𝐴)} = {((
-us “ ( R ‘𝐴)) |s ( -us “ ( L
‘𝐴)))}) |
104 | 102, 103 | breqtrd 5167 |
. . 3
⊢ (𝜑 → ( -us “
𝑅) <<s {((
-us “ ( R ‘𝐴)) |s ( -us “ ( L
‘𝐴)))}) |
105 | | ssltex1 27214 |
. . . . . . 7
⊢ (𝐿 <<s 𝑅 → 𝐿 ∈ V) |
106 | 2, 105 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐿 ∈ V) |
107 | | funimaexg 6623 |
. . . . . 6
⊢ ((Fun
-us ∧ 𝐿
∈ V) → ( -us “ 𝐿) ∈ V) |
108 | 57, 106, 107 | sylancr 587 |
. . . . 5
⊢ (𝜑 → ( -us “
𝐿) ∈
V) |
109 | | imassrn 6060 |
. . . . . . 7
⊢ (
-us “ 𝐿)
⊆ ran -us |
110 | 109, 67 | sseqtri 4014 |
. . . . . 6
⊢ (
-us “ 𝐿)
⊆ No |
111 | 110 | a1i 11 |
. . . . 5
⊢ (𝜑 → ( -us “
𝐿) ⊆ No ) |
112 | | fvelimab 6950 |
. . . . . . . . . 10
⊢ ((
-us Fn No ∧ 𝐿 ⊆ No )
→ (𝑏 ∈ (
-us “ 𝐿)
↔ ∃𝑐 ∈
𝐿 ( -us
‘𝑐) = 𝑏)) |
113 | 10, 35, 112 | sylancr 587 |
. . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ ( -us “ 𝐿) ↔ ∃𝑐 ∈ 𝐿 ( -us ‘𝑐) = 𝑏)) |
114 | 2 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝐿 <<s 𝑅) |
115 | 114, 77 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → ((𝐿 |s 𝑅) ∈ No
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) |
116 | 115 | simp2d 1143 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝐿 <<s {(𝐿 |s 𝑅)}) |
117 | 75 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → {𝐴} = {(𝐿 |s 𝑅)}) |
118 | 116, 117 | breqtrrd 5169 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝐿 <<s {𝐴}) |
119 | | simpr 485 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝑐 ∈ 𝐿) |
120 | 83 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝐴 ∈ {𝐴}) |
121 | 118, 119,
120 | ssltsepcd 27221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝑐 <s 𝐴) |
122 | 35 | sselda 3978 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝑐 ∈ No
) |
123 | 4 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝐴 ∈ No
) |
124 | | sltneg 27435 |
. . . . . . . . . . . . 13
⊢ ((𝑐 ∈
No ∧ 𝐴 ∈
No ) → (𝑐 <s 𝐴 ↔ ( -us ‘𝐴) <s ( -us
‘𝑐))) |
125 | 122, 123,
124 | syl2anc 584 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → (𝑐 <s 𝐴 ↔ ( -us ‘𝐴) <s ( -us
‘𝑐))) |
126 | 121, 125 | mpbid 231 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → ( -us ‘𝐴) <s ( -us
‘𝑐)) |
127 | | breq2 5145 |
. . . . . . . . . . 11
⊢ ((
-us ‘𝑐) =
𝑏 → (( -us
‘𝐴) <s (
-us ‘𝑐)
↔ ( -us ‘𝐴) <s 𝑏)) |
128 | 126, 127 | syl5ibcom 244 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → (( -us ‘𝑐) = 𝑏 → ( -us ‘𝐴) <s 𝑏)) |
129 | 128 | rexlimdva 3154 |
. . . . . . . . 9
⊢ (𝜑 → (∃𝑐 ∈ 𝐿 ( -us ‘𝑐) = 𝑏 → ( -us ‘𝐴) <s 𝑏)) |
130 | 113, 129 | sylbid 239 |
. . . . . . . 8
⊢ (𝜑 → (𝑏 ∈ ( -us “ 𝐿) → ( -us
‘𝐴) <s 𝑏)) |
131 | | breq1 5144 |
. . . . . . . . 9
⊢ (𝑎 = ( -us ‘𝐴) → (𝑎 <s 𝑏 ↔ ( -us ‘𝐴) <s 𝑏)) |
132 | 131 | imbi2d 340 |
. . . . . . . 8
⊢ (𝑎 = ( -us ‘𝐴) → ((𝑏 ∈ ( -us “ 𝐿) → 𝑎 <s 𝑏) ↔ (𝑏 ∈ ( -us “ 𝐿) → ( -us
‘𝐴) <s 𝑏))) |
133 | 130, 132 | syl5ibrcom 246 |
. . . . . . 7
⊢ (𝜑 → (𝑎 = ( -us ‘𝐴) → (𝑏 ∈ ( -us “ 𝐿) → 𝑎 <s 𝑏))) |
134 | 72, 133 | biimtrid 241 |
. . . . . 6
⊢ (𝜑 → (𝑎 ∈ {( -us ‘𝐴)} → (𝑏 ∈ ( -us “ 𝐿) → 𝑎 <s 𝑏))) |
135 | 134 | 3imp 1111 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ {( -us ‘𝐴)} ∧ 𝑏 ∈ ( -us “ 𝐿)) → 𝑎 <s 𝑏) |
136 | 63, 108, 71, 111, 135 | ssltd 27219 |
. . . 4
⊢ (𝜑 → {( -us
‘𝐴)} <<s (
-us “ 𝐿)) |
137 | 103, 136 | eqbrtrrd 5165 |
. . 3
⊢ (𝜑 → {(( -us “
( R ‘𝐴)) |s (
-us “ ( L ‘𝐴)))} <<s ( -us “
𝐿)) |
138 | 8, 32, 55, 104, 137 | cofcut1d 27328 |
. 2
⊢ (𝜑 → (( -us “
( R ‘𝐴)) |s (
-us “ ( L ‘𝐴))) = (( -us “ 𝑅) |s ( -us “
𝐿))) |
139 | 6, 138 | eqtrd 2771 |
1
⊢ (𝜑 → ( -us
‘𝐴) = ((
-us “ 𝑅)
|s ( -us “ 𝐿))) |