| Step | Hyp | Ref
| Expression |
| 1 | | fo1st 8034 |
. . . . . . . 8
⊢
1st :V–onto→V |
| 2 | | fofun 6821 |
. . . . . . . 8
⊢
(1st :V–onto→V → Fun 1st ) |
| 3 | 1, 2 | ax-mp 5 |
. . . . . . 7
⊢ Fun
1st |
| 4 | | rdgfun 8456 |
. . . . . . . 8
⊢ Fun
rec((𝑝 ∈ V ↦
⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd
‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉), 〈{
0s }, ∅〉) |
| 5 | | precsexlem.1 |
. . . . . . . . 9
⊢ 𝐹 = rec((𝑝 ∈ V ↦
⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd
‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉), 〈{
0s }, ∅〉) |
| 6 | 5 | funeqi 6587 |
. . . . . . . 8
⊢ (Fun
𝐹 ↔ Fun rec((𝑝 ∈ V ↦
⦋(1st ‘𝑝) / 𝑙⦌⦋(2nd
‘𝑝) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})),
(𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))〉), 〈{
0s }, ∅〉)) |
| 7 | 4, 6 | mpbir 231 |
. . . . . . 7
⊢ Fun 𝐹 |
| 8 | | funco 6606 |
. . . . . . 7
⊢ ((Fun
1st ∧ Fun 𝐹)
→ Fun (1st ∘ 𝐹)) |
| 9 | 3, 7, 8 | mp2an 692 |
. . . . . 6
⊢ Fun
(1st ∘ 𝐹) |
| 10 | | precsexlem.2 |
. . . . . . 7
⊢ 𝐿 = (1st ∘ 𝐹) |
| 11 | 10 | funeqi 6587 |
. . . . . 6
⊢ (Fun
𝐿 ↔ Fun
(1st ∘ 𝐹)) |
| 12 | 9, 11 | mpbir 231 |
. . . . 5
⊢ Fun 𝐿 |
| 13 | | dcomex 10487 |
. . . . . 6
⊢ ω
∈ V |
| 14 | 13 | funimaex 6655 |
. . . . 5
⊢ (Fun
𝐿 → (𝐿 “ ω) ∈ V) |
| 15 | 12, 14 | ax-mp 5 |
. . . 4
⊢ (𝐿 “ ω) ∈
V |
| 16 | 15 | uniex 7761 |
. . 3
⊢ ∪ (𝐿
“ ω) ∈ V |
| 17 | 16 | a1i 11 |
. 2
⊢ (𝜑 → ∪ (𝐿
“ ω) ∈ V) |
| 18 | | fo2nd 8035 |
. . . . . . . 8
⊢
2nd :V–onto→V |
| 19 | | fofun 6821 |
. . . . . . . 8
⊢
(2nd :V–onto→V → Fun 2nd ) |
| 20 | 18, 19 | ax-mp 5 |
. . . . . . 7
⊢ Fun
2nd |
| 21 | | funco 6606 |
. . . . . . 7
⊢ ((Fun
2nd ∧ Fun 𝐹)
→ Fun (2nd ∘ 𝐹)) |
| 22 | 20, 7, 21 | mp2an 692 |
. . . . . 6
⊢ Fun
(2nd ∘ 𝐹) |
| 23 | | precsexlem.3 |
. . . . . . 7
⊢ 𝑅 = (2nd ∘ 𝐹) |
| 24 | 23 | funeqi 6587 |
. . . . . 6
⊢ (Fun
𝑅 ↔ Fun
(2nd ∘ 𝐹)) |
| 25 | 22, 24 | mpbir 231 |
. . . . 5
⊢ Fun 𝑅 |
| 26 | 13 | funimaex 6655 |
. . . . 5
⊢ (Fun
𝑅 → (𝑅 “ ω) ∈ V) |
| 27 | 25, 26 | ax-mp 5 |
. . . 4
⊢ (𝑅 “ ω) ∈
V |
| 28 | 27 | uniex 7761 |
. . 3
⊢ ∪ (𝑅
“ ω) ∈ V |
| 29 | 28 | a1i 11 |
. 2
⊢ (𝜑 → ∪ (𝑅
“ ω) ∈ V) |
| 30 | | funiunfv 7268 |
. . . 4
⊢ (Fun
𝐿 → ∪ 𝑖 ∈ ω (𝐿‘𝑖) = ∪ (𝐿 “
ω)) |
| 31 | 12, 30 | ax-mp 5 |
. . 3
⊢ ∪ 𝑖 ∈ ω (𝐿‘𝑖) = ∪ (𝐿 “
ω) |
| 32 | | precsexlem.4 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ No
) |
| 33 | | precsexlem.5 |
. . . . . 6
⊢ (𝜑 → 0s <s 𝐴) |
| 34 | | precsexlem.6 |
. . . . . 6
⊢ (𝜑 → ∀𝑥𝑂 ∈ (( L ‘𝐴) ∪ ( R ‘𝐴))( 0s <s 𝑥𝑂 →
∃𝑦 ∈ No (𝑥𝑂 ·s
𝑦) = 1s
)) |
| 35 | 5, 10, 23, 32, 33, 34 | precsexlem8 28238 |
. . . . 5
⊢ ((𝜑 ∧ 𝑖 ∈ ω) → ((𝐿‘𝑖) ⊆ No
∧ (𝑅‘𝑖) ⊆
No )) |
| 36 | 35 | simpld 494 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ω) → (𝐿‘𝑖) ⊆ No
) |
| 37 | 36 | iunssd 5050 |
. . 3
⊢ (𝜑 → ∪ 𝑖 ∈ ω (𝐿‘𝑖) ⊆ No
) |
| 38 | 31, 37 | eqsstrrid 4023 |
. 2
⊢ (𝜑 → ∪ (𝐿
“ ω) ⊆ No ) |
| 39 | | funiunfv 7268 |
. . . 4
⊢ (Fun
𝑅 → ∪ 𝑖 ∈ ω (𝑅‘𝑖) = ∪ (𝑅 “
ω)) |
| 40 | 25, 39 | ax-mp 5 |
. . 3
⊢ ∪ 𝑖 ∈ ω (𝑅‘𝑖) = ∪ (𝑅 “
ω) |
| 41 | 35 | simprd 495 |
. . . 4
⊢ ((𝜑 ∧ 𝑖 ∈ ω) → (𝑅‘𝑖) ⊆ No
) |
| 42 | 41 | iunssd 5050 |
. . 3
⊢ (𝜑 → ∪ 𝑖 ∈ ω (𝑅‘𝑖) ⊆ No
) |
| 43 | 40, 42 | eqsstrrid 4023 |
. 2
⊢ (𝜑 → ∪ (𝑅
“ ω) ⊆ No ) |
| 44 | 31 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑏 ∈ ∪ 𝑖 ∈ ω (𝐿‘𝑖) ↔ 𝑏 ∈ ∪ (𝐿 “
ω)) |
| 45 | | eliun 4995 |
. . . . . . 7
⊢ (𝑏 ∈ ∪ 𝑖 ∈ ω (𝐿‘𝑖) ↔ ∃𝑖 ∈ ω 𝑏 ∈ (𝐿‘𝑖)) |
| 46 | 44, 45 | bitr3i 277 |
. . . . . 6
⊢ (𝑏 ∈ ∪ (𝐿
“ ω) ↔ ∃𝑖 ∈ ω 𝑏 ∈ (𝐿‘𝑖)) |
| 47 | | funiunfv 7268 |
. . . . . . . . 9
⊢ (Fun
𝑅 → ∪ 𝑗 ∈ ω (𝑅‘𝑗) = ∪ (𝑅 “
ω)) |
| 48 | 25, 47 | ax-mp 5 |
. . . . . . . 8
⊢ ∪ 𝑗 ∈ ω (𝑅‘𝑗) = ∪ (𝑅 “
ω) |
| 49 | 48 | eleq2i 2833 |
. . . . . . 7
⊢ (𝑐 ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ 𝑐 ∈ ∪ (𝑅 “
ω)) |
| 50 | | eliun 4995 |
. . . . . . 7
⊢ (𝑐 ∈ ∪ 𝑗 ∈ ω (𝑅‘𝑗) ↔ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅‘𝑗)) |
| 51 | 49, 50 | bitr3i 277 |
. . . . . 6
⊢ (𝑐 ∈ ∪ (𝑅
“ ω) ↔ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅‘𝑗)) |
| 52 | 46, 51 | anbi12i 628 |
. . . . 5
⊢ ((𝑏 ∈ ∪ (𝐿
“ ω) ∧ 𝑐
∈ ∪ (𝑅 “ ω)) ↔ (∃𝑖 ∈ ω 𝑏 ∈ (𝐿‘𝑖) ∧ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅‘𝑗))) |
| 53 | | reeanv 3229 |
. . . . 5
⊢
(∃𝑖 ∈
ω ∃𝑗 ∈
ω (𝑏 ∈ (𝐿‘𝑖) ∧ 𝑐 ∈ (𝑅‘𝑗)) ↔ (∃𝑖 ∈ ω 𝑏 ∈ (𝐿‘𝑖) ∧ ∃𝑗 ∈ ω 𝑐 ∈ (𝑅‘𝑗))) |
| 54 | 52, 53 | bitr4i 278 |
. . . 4
⊢ ((𝑏 ∈ ∪ (𝐿
“ ω) ∧ 𝑐
∈ ∪ (𝑅 “ ω)) ↔ ∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑏 ∈ (𝐿‘𝑖) ∧ 𝑐 ∈ (𝑅‘𝑗))) |
| 55 | | omun 7909 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑖 ∪ 𝑗) ∈ ω) |
| 56 | | ssun1 4178 |
. . . . . . . . . 10
⊢ 𝑖 ⊆ (𝑖 ∪ 𝑗) |
| 57 | 5, 10, 23 | precsexlem6 28236 |
. . . . . . . . . 10
⊢ ((𝑖 ∈ ω ∧ (𝑖 ∪ 𝑗) ∈ ω ∧ 𝑖 ⊆ (𝑖 ∪ 𝑗)) → (𝐿‘𝑖) ⊆ (𝐿‘(𝑖 ∪ 𝑗))) |
| 58 | 56, 57 | mp3an3 1452 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ω ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝐿‘𝑖) ⊆ (𝐿‘(𝑖 ∪ 𝑗))) |
| 59 | 55, 58 | syldan 591 |
. . . . . . . 8
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝐿‘𝑖) ⊆ (𝐿‘(𝑖 ∪ 𝑗))) |
| 60 | 59 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → (𝐿‘𝑖) ⊆ (𝐿‘(𝑖 ∪ 𝑗))) |
| 61 | 60 | sseld 3982 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → (𝑏 ∈ (𝐿‘𝑖) → 𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)))) |
| 62 | | simpr 484 |
. . . . . . . . 9
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → 𝑗 ∈
ω) |
| 63 | | ssun2 4179 |
. . . . . . . . . 10
⊢ 𝑗 ⊆ (𝑖 ∪ 𝑗) |
| 64 | 5, 10, 23 | precsexlem7 28237 |
. . . . . . . . . 10
⊢ ((𝑗 ∈ ω ∧ (𝑖 ∪ 𝑗) ∈ ω ∧ 𝑗 ⊆ (𝑖 ∪ 𝑗)) → (𝑅‘𝑗) ⊆ (𝑅‘(𝑖 ∪ 𝑗))) |
| 65 | 63, 64 | mp3an3 1452 |
. . . . . . . . 9
⊢ ((𝑗 ∈ ω ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝑅‘𝑗) ⊆ (𝑅‘(𝑖 ∪ 𝑗))) |
| 66 | 62, 55, 65 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑅‘𝑗) ⊆ (𝑅‘(𝑖 ∪ 𝑗))) |
| 67 | 66 | sseld 3982 |
. . . . . . 7
⊢ ((𝑖 ∈ ω ∧ 𝑗 ∈ ω) → (𝑐 ∈ (𝑅‘𝑗) → 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) |
| 68 | 67 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → (𝑐 ∈ (𝑅‘𝑗) → 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) |
| 69 | 32 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → 𝐴 ∈ No
) |
| 70 | 5, 10, 23, 32, 33, 34 | precsexlem8 28238 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → ((𝐿‘(𝑖 ∪ 𝑗)) ⊆ No
∧ (𝑅‘(𝑖 ∪ 𝑗)) ⊆ No
)) |
| 71 | 70 | simpld 494 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝐿‘(𝑖 ∪ 𝑗)) ⊆ No
) |
| 72 | 71 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ 𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗))) → 𝑏 ∈ No
) |
| 73 | 72 | adantrr 717 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → 𝑏 ∈ No
) |
| 74 | 69, 73 | mulscld 28161 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → (𝐴 ·s 𝑏) ∈ No
) |
| 75 | 70 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝑅‘(𝑖 ∪ 𝑗)) ⊆ No
) |
| 76 | 75 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗))) → 𝑐 ∈ No
) |
| 77 | 76 | adantrl 716 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → 𝑐 ∈ No
) |
| 78 | 69, 77 | mulscld 28161 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → (𝐴 ·s 𝑐) ∈ No
) |
| 79 | 74, 78 | jca 511 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → ((𝐴 ·s 𝑏) ∈ No
∧ (𝐴
·s 𝑐)
∈ No )) |
| 80 | 5, 10, 23, 32, 33, 34 | precsexlem9 28239 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → (∀𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗))(𝐴 ·s 𝑏) <s 1s ∧ ∀𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)) 1s <s (𝐴 ·s 𝑐))) |
| 81 | 80 | simpld 494 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → ∀𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗))(𝐴 ·s 𝑏) <s 1s ) |
| 82 | | rsp 3247 |
. . . . . . . . . . . . 13
⊢
(∀𝑏 ∈
(𝐿‘(𝑖 ∪ 𝑗))(𝐴 ·s 𝑏) <s 1s → (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) → (𝐴 ·s 𝑏) <s 1s )) |
| 83 | 81, 82 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) → (𝐴 ·s 𝑏) <s 1s )) |
| 84 | 80 | simprd 495 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → ∀𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)) 1s <s (𝐴 ·s 𝑐)) |
| 85 | | rsp 3247 |
. . . . . . . . . . . . 13
⊢
(∀𝑐 ∈
(𝑅‘(𝑖 ∪ 𝑗)) 1s <s (𝐴 ·s 𝑐) → (𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)) → 1s <s (𝐴 ·s 𝑐))) |
| 86 | 84, 85 | syl 17 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → (𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)) → 1s <s (𝐴 ·s 𝑐))) |
| 87 | 83, 86 | anim12d 609 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → ((𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗))) → ((𝐴 ·s 𝑏) <s 1s ∧ 1s
<s (𝐴
·s 𝑐)))) |
| 88 | 87 | imp 406 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → ((𝐴 ·s 𝑏) <s 1s ∧ 1s
<s (𝐴
·s 𝑐))) |
| 89 | | 1sno 27872 |
. . . . . . . . . . 11
⊢
1s ∈ No |
| 90 | | slttr 27792 |
. . . . . . . . . . 11
⊢ (((𝐴 ·s 𝑏) ∈
No ∧ 1s ∈ No ∧
(𝐴 ·s
𝑐) ∈ No ) → (((𝐴 ·s 𝑏) <s 1s ∧ 1s
<s (𝐴
·s 𝑐))
→ (𝐴
·s 𝑏)
<s (𝐴
·s 𝑐))) |
| 91 | 89, 90 | mp3an2 1451 |
. . . . . . . . . 10
⊢ (((𝐴 ·s 𝑏) ∈
No ∧ (𝐴
·s 𝑐)
∈ No ) → (((𝐴 ·s 𝑏) <s 1s ∧ 1s
<s (𝐴
·s 𝑐))
→ (𝐴
·s 𝑏)
<s (𝐴
·s 𝑐))) |
| 92 | 79, 88, 91 | sylc 65 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → (𝐴 ·s 𝑏) <s (𝐴 ·s 𝑐)) |
| 93 | 33 | ad2antrr 726 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → 0s <s 𝐴) |
| 94 | 73, 77, 69, 93 | sltmul2d 28198 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → (𝑏 <s 𝑐 ↔ (𝐴 ·s 𝑏) <s (𝐴 ·s 𝑐))) |
| 95 | 92, 94 | mpbird 257 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) ∧ (𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗)))) → 𝑏 <s 𝑐) |
| 96 | 95 | ex 412 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑖 ∪ 𝑗) ∈ ω) → ((𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗))) → 𝑏 <s 𝑐)) |
| 97 | 55, 96 | sylan2 593 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑏 ∈ (𝐿‘(𝑖 ∪ 𝑗)) ∧ 𝑐 ∈ (𝑅‘(𝑖 ∪ 𝑗))) → 𝑏 <s 𝑐)) |
| 98 | 61, 68, 97 | syl2and 608 |
. . . . 5
⊢ ((𝜑 ∧ (𝑖 ∈ ω ∧ 𝑗 ∈ ω)) → ((𝑏 ∈ (𝐿‘𝑖) ∧ 𝑐 ∈ (𝑅‘𝑗)) → 𝑏 <s 𝑐)) |
| 99 | 98 | rexlimdvva 3213 |
. . . 4
⊢ (𝜑 → (∃𝑖 ∈ ω ∃𝑗 ∈ ω (𝑏 ∈ (𝐿‘𝑖) ∧ 𝑐 ∈ (𝑅‘𝑗)) → 𝑏 <s 𝑐)) |
| 100 | 54, 99 | biimtrid 242 |
. . 3
⊢ (𝜑 → ((𝑏 ∈ ∪ (𝐿 “ ω) ∧ 𝑐 ∈ ∪ (𝑅
“ ω)) → 𝑏
<s 𝑐)) |
| 101 | 100 | 3impib 1117 |
. 2
⊢ ((𝜑 ∧ 𝑏 ∈ ∪ (𝐿 “ ω) ∧ 𝑐 ∈ ∪ (𝑅
“ ω)) → 𝑏
<s 𝑐) |
| 102 | 17, 29, 38, 43, 101 | ssltd 27836 |
1
⊢ (𝜑 → ∪ (𝐿
“ ω) <<s ∪ (𝑅 “ ω)) |