| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | negsunif.2 | . . . 4
⊢ (𝜑 → 𝐴 = (𝐿 |s 𝑅)) | 
| 2 |  | negsunif.1 | . . . . 5
⊢ (𝜑 → 𝐿 <<s 𝑅) | 
| 3 | 2 | scutcld 27848 | . . . 4
⊢ (𝜑 → (𝐿 |s 𝑅) ∈  No
) | 
| 4 | 1, 3 | eqeltrd 2841 | . . 3
⊢ (𝜑 → 𝐴 ∈  No
) | 
| 5 |  | negsval 28057 | . . 3
⊢ (𝐴 ∈ 
No  → ( -us ‘𝐴) = (( -us “ ( R
‘𝐴)) |s (
-us “ ( L ‘𝐴)))) | 
| 6 | 4, 5 | syl 17 | . 2
⊢ (𝜑 → ( -us
‘𝐴) = ((
-us “ ( R ‘𝐴)) |s ( -us “ ( L
‘𝐴)))) | 
| 7 |  | negscut2 28072 | . . . 4
⊢ (𝐴 ∈ 
No  → ( -us “ ( R ‘𝐴)) <<s ( -us “ ( L
‘𝐴))) | 
| 8 | 4, 7 | syl 17 | . . 3
⊢ (𝜑 → ( -us “ (
R ‘𝐴)) <<s (
-us “ ( L ‘𝐴))) | 
| 9 | 2, 1 | cofcutr2d 27960 | . . . . 5
⊢ (𝜑 → ∀𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ 𝑅 𝑑 ≤s 𝑐) | 
| 10 |  | negsfn 28055 | . . . . . . . 8
⊢ 
-us Fn  No | 
| 11 |  | ssltss2 27834 | . . . . . . . . 9
⊢ (𝐿 <<s 𝑅 → 𝑅 ⊆  No
) | 
| 12 | 2, 11 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝑅 ⊆  No
) | 
| 13 |  | breq2 5147 | . . . . . . . . 9
⊢ (𝑏 = ( -us ‘𝑑) → (( -us
‘𝑐) ≤s 𝑏 ↔ ( -us
‘𝑐) ≤s (
-us ‘𝑑))) | 
| 14 | 13 | rexima 7258 | . . . . . . . 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 3178 | . . . . . 6
⊢ (𝜑 → (∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ 𝑅 ( -us ‘𝑐) ≤s ( -us ‘𝑑))) | 
| 17 | 12 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → 𝑅 ⊆  No
) | 
| 18 | 17 | sselda 3983 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ 𝑑 ∈ 𝑅) → 𝑑 ∈  No
) | 
| 19 |  | rightssno 27920 | . . . . . . . . . . 11
⊢ ( R
‘𝐴) ⊆  No | 
| 20 | 19 | sseli 3979 | . . . . . . . . . 10
⊢ (𝑐 ∈ ( R ‘𝐴) → 𝑐 ∈  No
) | 
| 21 | 20 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ 𝑑 ∈ 𝑅) → 𝑐 ∈  No
) | 
| 22 | 18, 21 | slenegd 28080 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) ∧ 𝑑 ∈ 𝑅) → (𝑑 ≤s 𝑐 ↔ ( -us ‘𝑐) ≤s ( -us
‘𝑑))) | 
| 23 | 22 | rexbidva 3177 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ( R ‘𝐴)) → (∃𝑑 ∈ 𝑅 𝑑 ≤s 𝑐 ↔ ∃𝑑 ∈ 𝑅 ( -us ‘𝑐) ≤s ( -us ‘𝑑))) | 
| 24 | 23 | ralbidva 3176 | . . . . . 6
⊢ (𝜑 → (∀𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ 𝑅 𝑑 ≤s 𝑐 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ 𝑅 ( -us ‘𝑐) ≤s ( -us ‘𝑑))) | 
| 25 | 16, 24 | bitr4d 282 | . . . . 5
⊢ (𝜑 → (∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑑 ∈ 𝑅 𝑑 ≤s 𝑐)) | 
| 26 | 9, 25 | mpbird 257 | . . . 4
⊢ (𝜑 → ∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏) | 
| 27 |  | breq1 5146 | . . . . . . 7
⊢ (𝑎 = ( -us ‘𝑐) → (𝑎 ≤s 𝑏 ↔ ( -us ‘𝑐) ≤s 𝑏)) | 
| 28 | 27 | rexbidv 3179 | . . . . . 6
⊢ (𝑎 = ( -us ‘𝑐) → (∃𝑏 ∈ ( -us “
𝑅)𝑎 ≤s 𝑏 ↔ ∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏)) | 
| 29 | 28 | ralima 7257 | . . . . 5
⊢ ((
-us Fn  No  ∧ ( R ‘𝐴) ⊆ 
No ) → (∀𝑎 ∈ ( -us “ ( R
‘𝐴))∃𝑏 ∈ ( -us “
𝑅)𝑎 ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏)) | 
| 30 | 10, 19, 29 | mp2an 692 | . . . 4
⊢
(∀𝑎 ∈ (
-us “ ( R ‘𝐴))∃𝑏 ∈ ( -us “ 𝑅)𝑎 ≤s 𝑏 ↔ ∀𝑐 ∈ ( R ‘𝐴)∃𝑏 ∈ ( -us “ 𝑅)( -us ‘𝑐) ≤s 𝑏) | 
| 31 | 26, 30 | sylibr 234 | . . 3
⊢ (𝜑 → ∀𝑎 ∈ ( -us “ ( R
‘𝐴))∃𝑏 ∈ ( -us “
𝑅)𝑎 ≤s 𝑏) | 
| 32 | 2, 1 | cofcutr1d 27959 | . . . . 5
⊢ (𝜑 → ∀𝑐 ∈ ( L ‘𝐴)∃𝑑 ∈ 𝐿 𝑐 ≤s 𝑑) | 
| 33 |  | ssltss1 27833 | . . . . . . . . 9
⊢ (𝐿 <<s 𝑅 → 𝐿 ⊆  No
) | 
| 34 | 2, 33 | syl 17 | . . . . . . . 8
⊢ (𝜑 → 𝐿 ⊆  No
) | 
| 35 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝑏 = ( -us ‘𝑑) → (𝑏 ≤s ( -us ‘𝑐) ↔ ( -us
‘𝑑) ≤s (
-us ‘𝑐))) | 
| 36 | 35 | rexima 7258 | . . . . . . . 8
⊢ ((
-us Fn  No  ∧ 𝐿 ⊆  No )
→ (∃𝑏 ∈ (
-us “ 𝐿)𝑏 ≤s ( -us ‘𝑐) ↔ ∃𝑑 ∈ 𝐿 ( -us ‘𝑑) ≤s ( -us ‘𝑐))) | 
| 37 | 10, 34, 36 | sylancr 587 | . . . . . . 7
⊢ (𝜑 → (∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐) ↔ ∃𝑑 ∈ 𝐿 ( -us ‘𝑑) ≤s ( -us ‘𝑐))) | 
| 38 | 37 | ralbidv 3178 | . . . . . 6
⊢ (𝜑 → (∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐) ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑑 ∈ 𝐿 ( -us ‘𝑑) ≤s ( -us ‘𝑐))) | 
| 39 |  | leftssno 27919 | . . . . . . . . . . 11
⊢ ( L
‘𝐴) ⊆  No | 
| 40 | 39 | sseli 3979 | . . . . . . . . . 10
⊢ (𝑐 ∈ ( L ‘𝐴) → 𝑐 ∈  No
) | 
| 41 | 40 | ad2antlr 727 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ ( L ‘𝐴)) ∧ 𝑑 ∈ 𝐿) → 𝑐 ∈  No
) | 
| 42 | 34 | adantr 480 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ ( L ‘𝐴)) → 𝐿 ⊆  No
) | 
| 43 | 42 | sselda 3983 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑐 ∈ ( L ‘𝐴)) ∧ 𝑑 ∈ 𝐿) → 𝑑 ∈  No
) | 
| 44 | 41, 43 | slenegd 28080 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑐 ∈ ( L ‘𝐴)) ∧ 𝑑 ∈ 𝐿) → (𝑐 ≤s 𝑑 ↔ ( -us ‘𝑑) ≤s ( -us
‘𝑐))) | 
| 45 | 44 | rexbidva 3177 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑐 ∈ ( L ‘𝐴)) → (∃𝑑 ∈ 𝐿 𝑐 ≤s 𝑑 ↔ ∃𝑑 ∈ 𝐿 ( -us ‘𝑑) ≤s ( -us ‘𝑐))) | 
| 46 | 45 | ralbidva 3176 | . . . . . 6
⊢ (𝜑 → (∀𝑐 ∈ ( L ‘𝐴)∃𝑑 ∈ 𝐿 𝑐 ≤s 𝑑 ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑑 ∈ 𝐿 ( -us ‘𝑑) ≤s ( -us ‘𝑐))) | 
| 47 | 38, 46 | bitr4d 282 | . . . . 5
⊢ (𝜑 → (∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐) ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑑 ∈ 𝐿 𝑐 ≤s 𝑑)) | 
| 48 | 32, 47 | mpbird 257 | . . . 4
⊢ (𝜑 → ∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐)) | 
| 49 |  | breq2 5147 | . . . . . . 7
⊢ (𝑎 = ( -us ‘𝑐) → (𝑏 ≤s 𝑎 ↔ 𝑏 ≤s ( -us ‘𝑐))) | 
| 50 | 49 | rexbidv 3179 | . . . . . 6
⊢ (𝑎 = ( -us ‘𝑐) → (∃𝑏 ∈ ( -us “
𝐿)𝑏 ≤s 𝑎 ↔ ∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐))) | 
| 51 | 50 | ralima 7257 | . . . . 5
⊢ ((
-us Fn  No  ∧ ( L ‘𝐴) ⊆ 
No ) → (∀𝑎 ∈ ( -us “ ( L
‘𝐴))∃𝑏 ∈ ( -us “
𝐿)𝑏 ≤s 𝑎 ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐))) | 
| 52 | 10, 39, 51 | mp2an 692 | . . . 4
⊢
(∀𝑎 ∈ (
-us “ ( L ‘𝐴))∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s 𝑎 ↔ ∀𝑐 ∈ ( L ‘𝐴)∃𝑏 ∈ ( -us “ 𝐿)𝑏 ≤s ( -us ‘𝑐)) | 
| 53 | 48, 52 | sylibr 234 | . . 3
⊢ (𝜑 → ∀𝑎 ∈ ( -us “ ( L
‘𝐴))∃𝑏 ∈ ( -us “
𝐿)𝑏 ≤s 𝑎) | 
| 54 |  | fnfun 6668 | . . . . . . 7
⊢ (
-us Fn  No  → Fun -us
) | 
| 55 | 10, 54 | ax-mp 5 | . . . . . 6
⊢ Fun
-us | 
| 56 |  | ssltex2 27832 | . . . . . . 7
⊢ (𝐿 <<s 𝑅 → 𝑅 ∈ V) | 
| 57 | 2, 56 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ V) | 
| 58 |  | funimaexg 6653 | . . . . . 6
⊢ ((Fun
-us ∧ 𝑅
∈ V) → ( -us “ 𝑅) ∈ V) | 
| 59 | 55, 57, 58 | sylancr 587 | . . . . 5
⊢ (𝜑 → ( -us “
𝑅) ∈
V) | 
| 60 |  | snex 5436 | . . . . . 6
⊢ {(
-us ‘𝐴)}
∈ V | 
| 61 | 60 | a1i 11 | . . . . 5
⊢ (𝜑 → {( -us
‘𝐴)} ∈
V) | 
| 62 |  | imassrn 6089 | . . . . . . 7
⊢ (
-us “ 𝑅)
⊆ ran -us | 
| 63 |  | negsfo 28085 | . . . . . . . 8
⊢ 
-us : No –onto→ No | 
| 64 |  | forn 6823 | . . . . . . . 8
⊢ (
-us : No –onto→ No  → ran
-us =  No ) | 
| 65 | 63, 64 | ax-mp 5 | . . . . . . 7
⊢ ran
-us =  No | 
| 66 | 62, 65 | sseqtri 4032 | . . . . . 6
⊢ (
-us “ 𝑅)
⊆  No | 
| 67 | 66 | a1i 11 | . . . . 5
⊢ (𝜑 → ( -us “
𝑅) ⊆  No ) | 
| 68 | 4 | negscld 28069 | . . . . . 6
⊢ (𝜑 → ( -us
‘𝐴) ∈  No ) | 
| 69 | 68 | snssd 4809 | . . . . 5
⊢ (𝜑 → {( -us
‘𝐴)} ⊆  No ) | 
| 70 |  | velsn 4642 | . . . . . . . 8
⊢ (𝑎 ∈ {( -us
‘𝐴)} ↔ 𝑎 = ( -us ‘𝐴)) | 
| 71 |  | fvelimab 6981 | . . . . . . . . . . 11
⊢ ((
-us Fn  No  ∧ 𝑅 ⊆  No )
→ (𝑏 ∈ (
-us “ 𝑅)
↔ ∃𝑑 ∈
𝑅 ( -us
‘𝑑) = 𝑏)) | 
| 72 | 10, 12, 71 | sylancr 587 | . . . . . . . . . 10
⊢ (𝜑 → (𝑏 ∈ ( -us “ 𝑅) ↔ ∃𝑑 ∈ 𝑅 ( -us ‘𝑑) = 𝑏)) | 
| 73 | 1 | sneqd 4638 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → {𝐴} = {(𝐿 |s 𝑅)}) | 
| 74 | 73 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → {𝐴} = {(𝐿 |s 𝑅)}) | 
| 75 |  | scutcut 27846 | . . . . . . . . . . . . . . . . . 18
⊢ (𝐿 <<s 𝑅 → ((𝐿 |s 𝑅) ∈  No 
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) | 
| 76 | 2, 75 | syl 17 | . . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((𝐿 |s 𝑅) ∈  No 
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) | 
| 77 | 76 | simp3d 1145 | . . . . . . . . . . . . . . . 16
⊢ (𝜑 → {(𝐿 |s 𝑅)} <<s 𝑅) | 
| 78 | 77 | adantr 480 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → {(𝐿 |s 𝑅)} <<s 𝑅) | 
| 79 | 74, 78 | eqbrtrd 5165 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → {𝐴} <<s 𝑅) | 
| 80 |  | snidg 4660 | . . . . . . . . . . . . . . . 16
⊢ (𝐴 ∈ 
No  → 𝐴 ∈
{𝐴}) | 
| 81 | 4, 80 | syl 17 | . . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐴 ∈ {𝐴}) | 
| 82 | 81 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝐴 ∈ {𝐴}) | 
| 83 |  | simpr 484 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝑑 ∈ 𝑅) | 
| 84 | 79, 82, 83 | ssltsepcd 27839 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝐴 <s 𝑑) | 
| 85 | 4 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝐴 ∈  No
) | 
| 86 | 12 | sselda 3983 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → 𝑑 ∈  No
) | 
| 87 | 85, 86 | sltnegd 28079 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → (𝐴 <s 𝑑 ↔ ( -us ‘𝑑) <s ( -us
‘𝐴))) | 
| 88 | 84, 87 | mpbid 232 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → ( -us ‘𝑑) <s ( -us
‘𝐴)) | 
| 89 |  | breq1 5146 | . . . . . . . . . . . 12
⊢ ((
-us ‘𝑑) =
𝑏 → (( -us
‘𝑑) <s (
-us ‘𝐴)
↔ 𝑏 <s (
-us ‘𝐴))) | 
| 90 | 88, 89 | syl5ibcom 245 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑑 ∈ 𝑅) → (( -us ‘𝑑) = 𝑏 → 𝑏 <s ( -us ‘𝐴))) | 
| 91 | 90 | rexlimdva 3155 | . . . . . . . . . 10
⊢ (𝜑 → (∃𝑑 ∈ 𝑅 ( -us ‘𝑑) = 𝑏 → 𝑏 <s ( -us ‘𝐴))) | 
| 92 | 72, 91 | sylbid 240 | . . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s ( -us ‘𝐴))) | 
| 93 |  | breq2 5147 | . . . . . . . . . 10
⊢ (𝑎 = ( -us ‘𝐴) → (𝑏 <s 𝑎 ↔ 𝑏 <s ( -us ‘𝐴))) | 
| 94 | 93 | imbi2d 340 | . . . . . . . . 9
⊢ (𝑎 = ( -us ‘𝐴) → ((𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s 𝑎) ↔ (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s ( -us ‘𝐴)))) | 
| 95 | 92, 94 | syl5ibrcom 247 | . . . . . . . 8
⊢ (𝜑 → (𝑎 = ( -us ‘𝐴) → (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s 𝑎))) | 
| 96 | 70, 95 | biimtrid 242 | . . . . . . 7
⊢ (𝜑 → (𝑎 ∈ {( -us ‘𝐴)} → (𝑏 ∈ ( -us “ 𝑅) → 𝑏 <s 𝑎))) | 
| 97 | 96 | 3imp 1111 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ {( -us ‘𝐴)} ∧ 𝑏 ∈ ( -us “ 𝑅)) → 𝑏 <s 𝑎) | 
| 98 | 97 | 3com23 1127 | . . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ ( -us “ 𝑅) ∧ 𝑎 ∈ {( -us ‘𝐴)}) → 𝑏 <s 𝑎) | 
| 99 | 59, 61, 67, 69, 98 | ssltd 27836 | . . . 4
⊢ (𝜑 → ( -us “
𝑅) <<s {(
-us ‘𝐴)}) | 
| 100 | 6 | sneqd 4638 | . . . 4
⊢ (𝜑 → {( -us
‘𝐴)} = {((
-us “ ( R ‘𝐴)) |s ( -us “ ( L
‘𝐴)))}) | 
| 101 | 99, 100 | breqtrd 5169 | . . 3
⊢ (𝜑 → ( -us “
𝑅) <<s {((
-us “ ( R ‘𝐴)) |s ( -us “ ( L
‘𝐴)))}) | 
| 102 |  | ssltex1 27831 | . . . . . . 7
⊢ (𝐿 <<s 𝑅 → 𝐿 ∈ V) | 
| 103 | 2, 102 | syl 17 | . . . . . 6
⊢ (𝜑 → 𝐿 ∈ V) | 
| 104 |  | funimaexg 6653 | . . . . . 6
⊢ ((Fun
-us ∧ 𝐿
∈ V) → ( -us “ 𝐿) ∈ V) | 
| 105 | 55, 103, 104 | sylancr 587 | . . . . 5
⊢ (𝜑 → ( -us “
𝐿) ∈
V) | 
| 106 |  | imassrn 6089 | . . . . . . 7
⊢ (
-us “ 𝐿)
⊆ ran -us | 
| 107 | 106, 65 | sseqtri 4032 | . . . . . 6
⊢ (
-us “ 𝐿)
⊆  No | 
| 108 | 107 | a1i 11 | . . . . 5
⊢ (𝜑 → ( -us “
𝐿) ⊆  No ) | 
| 109 |  | fvelimab 6981 | . . . . . . . . . 10
⊢ ((
-us Fn  No  ∧ 𝐿 ⊆  No )
→ (𝑏 ∈ (
-us “ 𝐿)
↔ ∃𝑐 ∈
𝐿 ( -us
‘𝑐) = 𝑏)) | 
| 110 | 10, 34, 109 | sylancr 587 | . . . . . . . . 9
⊢ (𝜑 → (𝑏 ∈ ( -us “ 𝐿) ↔ ∃𝑐 ∈ 𝐿 ( -us ‘𝑐) = 𝑏)) | 
| 111 | 2 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝐿 <<s 𝑅) | 
| 112 | 111, 75 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → ((𝐿 |s 𝑅) ∈  No 
∧ 𝐿 <<s {(𝐿 |s 𝑅)} ∧ {(𝐿 |s 𝑅)} <<s 𝑅)) | 
| 113 | 112 | simp2d 1144 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝐿 <<s {(𝐿 |s 𝑅)}) | 
| 114 | 73 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → {𝐴} = {(𝐿 |s 𝑅)}) | 
| 115 | 113, 114 | breqtrrd 5171 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝐿 <<s {𝐴}) | 
| 116 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝑐 ∈ 𝐿) | 
| 117 | 81 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝐴 ∈ {𝐴}) | 
| 118 | 115, 116,
117 | ssltsepcd 27839 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝑐 <s 𝐴) | 
| 119 | 34 | sselda 3983 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝑐 ∈  No
) | 
| 120 | 4 | adantr 480 | . . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → 𝐴 ∈  No
) | 
| 121 | 119, 120 | sltnegd 28079 | . . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → (𝑐 <s 𝐴 ↔ ( -us ‘𝐴) <s ( -us
‘𝑐))) | 
| 122 | 118, 121 | mpbid 232 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → ( -us ‘𝐴) <s ( -us
‘𝑐)) | 
| 123 |  | breq2 5147 | . . . . . . . . . . 11
⊢ ((
-us ‘𝑐) =
𝑏 → (( -us
‘𝐴) <s (
-us ‘𝑐)
↔ ( -us ‘𝐴) <s 𝑏)) | 
| 124 | 122, 123 | syl5ibcom 245 | . . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑐 ∈ 𝐿) → (( -us ‘𝑐) = 𝑏 → ( -us ‘𝐴) <s 𝑏)) | 
| 125 | 124 | rexlimdva 3155 | . . . . . . . . 9
⊢ (𝜑 → (∃𝑐 ∈ 𝐿 ( -us ‘𝑐) = 𝑏 → ( -us ‘𝐴) <s 𝑏)) | 
| 126 | 110, 125 | sylbid 240 | . . . . . . . 8
⊢ (𝜑 → (𝑏 ∈ ( -us “ 𝐿) → ( -us
‘𝐴) <s 𝑏)) | 
| 127 |  | breq1 5146 | . . . . . . . . 9
⊢ (𝑎 = ( -us ‘𝐴) → (𝑎 <s 𝑏 ↔ ( -us ‘𝐴) <s 𝑏)) | 
| 128 | 127 | imbi2d 340 | . . . . . . . 8
⊢ (𝑎 = ( -us ‘𝐴) → ((𝑏 ∈ ( -us “ 𝐿) → 𝑎 <s 𝑏) ↔ (𝑏 ∈ ( -us “ 𝐿) → ( -us
‘𝐴) <s 𝑏))) | 
| 129 | 126, 128 | syl5ibrcom 247 | . . . . . . 7
⊢ (𝜑 → (𝑎 = ( -us ‘𝐴) → (𝑏 ∈ ( -us “ 𝐿) → 𝑎 <s 𝑏))) | 
| 130 | 70, 129 | biimtrid 242 | . . . . . 6
⊢ (𝜑 → (𝑎 ∈ {( -us ‘𝐴)} → (𝑏 ∈ ( -us “ 𝐿) → 𝑎 <s 𝑏))) | 
| 131 | 130 | 3imp 1111 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ {( -us ‘𝐴)} ∧ 𝑏 ∈ ( -us “ 𝐿)) → 𝑎 <s 𝑏) | 
| 132 | 61, 105, 69, 108, 131 | ssltd 27836 | . . . 4
⊢ (𝜑 → {( -us
‘𝐴)} <<s (
-us “ 𝐿)) | 
| 133 | 100, 132 | eqbrtrrd 5167 | . . 3
⊢ (𝜑 → {(( -us “
( R ‘𝐴)) |s (
-us “ ( L ‘𝐴)))} <<s ( -us “
𝐿)) | 
| 134 | 8, 31, 53, 101, 133 | cofcut1d 27955 | . 2
⊢ (𝜑 → (( -us “
( R ‘𝐴)) |s (
-us “ ( L ‘𝐴))) = (( -us “ 𝑅) |s ( -us “
𝐿))) | 
| 135 | 6, 134 | eqtrd 2777 | 1
⊢ (𝜑 → ( -us
‘𝐴) = ((
-us “ 𝑅)
|s ( -us “ 𝐿))) |