Proof of Theorem precsexlem3
Step | Hyp | Ref
| Expression |
1 | | nnon 7870 |
. . 3
⊢ (𝐼 ∈ ω → 𝐼 ∈ On) |
2 | | opex 5460 |
. . . . 5
⊢
〈(𝑙 ∪
({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 ∈
V |
3 | 2 | csbex 5305 |
. . . 4
⊢
⦋(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
𝑥𝑅)}))〉 ∈
V |
4 | 3 | csbex 5305 |
. . 3
⊢
⦋(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
𝑥𝑅)}))〉 ∈
V |
5 | | precsexlem.1 |
. . . 4
⊢ 𝐹 = 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 | | fveq2 6891 |
. . . . 5
⊢ (𝑝 = (𝐹‘𝐼) → (1st ‘𝑝) = (1st
‘(𝐹‘𝐼))) |
7 | | fveq2 6891 |
. . . . . 6
⊢ (𝑝 = (𝐹‘𝐼) → (2nd ‘𝑝) = (2nd
‘(𝐹‘𝐼))) |
8 | 7 | csbeq1d 3893 |
. . . . 5
⊢ (𝑝 = (𝐹‘𝐼) → ⦋(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
𝑥𝑅)}))〉 =
⦋(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
𝑥𝑅)}))〉) |
9 | 6, 8 | csbeq12dv 3898 |
. . . 4
⊢ (𝑝 = (𝐹‘𝐼) → ⦋(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
𝑥𝑅)}))〉 =
⦋(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
𝑥𝑅)}))〉) |
10 | 5, 9 | rdgsucmpt 8445 |
. . 3
⊢ ((𝐼 ∈ On ∧
⦋(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
𝑥𝑅)}))〉 ∈ V)
→ (𝐹‘suc 𝐼) =
⦋(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
𝑥𝑅)}))〉) |
11 | 1, 4, 10 | sylancl 585 |
. 2
⊢ (𝐼 ∈ ω → (𝐹‘suc 𝐼) = ⦋(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
𝑥𝑅)}))〉) |
12 | | precsexlem.2 |
. . . . . 6
⊢ 𝐿 = (1st ∘ 𝐹) |
13 | 12 | fveq1i 6892 |
. . . . 5
⊢ (𝐿‘𝐼) = ((1st ∘ 𝐹)‘𝐼) |
14 | | rdgfnon 8432 |
. . . . . . 7
⊢
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 }, ∅〉) Fn On |
15 | 5 | fneq1i 6645 |
. . . . . . 7
⊢ (𝐹 Fn On ↔ 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 }, ∅〉) Fn On) |
16 | 14, 15 | mpbir 230 |
. . . . . 6
⊢ 𝐹 Fn On |
17 | | fvco2 6989 |
. . . . . 6
⊢ ((𝐹 Fn On ∧ 𝐼 ∈ On) → ((1st ∘
𝐹)‘𝐼) = (1st ‘(𝐹‘𝐼))) |
18 | 16, 1, 17 | sylancr 586 |
. . . . 5
⊢ (𝐼 ∈ ω →
((1st ∘ 𝐹)‘𝐼) = (1st ‘(𝐹‘𝐼))) |
19 | 13, 18 | eqtrid 2779 |
. . . 4
⊢ (𝐼 ∈ ω → (𝐿‘𝐼) = (1st ‘(𝐹‘𝐼))) |
20 | | precsexlem.3 |
. . . . . . 7
⊢ 𝑅 = (2nd ∘ 𝐹) |
21 | 20 | fveq1i 6892 |
. . . . . 6
⊢ (𝑅‘𝐼) = ((2nd ∘ 𝐹)‘𝐼) |
22 | | fvco2 6989 |
. . . . . . 7
⊢ ((𝐹 Fn On ∧ 𝐼 ∈ On) → ((2nd ∘
𝐹)‘𝐼) = (2nd ‘(𝐹‘𝐼))) |
23 | 16, 1, 22 | sylancr 586 |
. . . . . 6
⊢ (𝐼 ∈ ω →
((2nd ∘ 𝐹)‘𝐼) = (2nd ‘(𝐹‘𝐼))) |
24 | 21, 23 | eqtrid 2779 |
. . . . 5
⊢ (𝐼 ∈ ω → (𝑅‘𝐼) = (2nd ‘(𝐹‘𝐼))) |
25 | 24 | csbeq1d 3893 |
. . . 4
⊢ (𝐼 ∈ ω →
⦋(𝑅‘𝐼) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 =
⦋(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
𝑥𝑅)}))〉) |
26 | 19, 25 | csbeq12dv 3898 |
. . 3
⊢ (𝐼 ∈ ω →
⦋(𝐿‘𝐼) / 𝑙⦌⦋(𝑅‘𝐼) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 =
⦋(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
𝑥𝑅)}))〉) |
27 | | fvex 6904 |
. . . . . 6
⊢ (𝑅‘𝐼) ∈ V |
28 | | rexeq 3316 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑅‘𝐼) → (∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
↔ ∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿))) |
29 | 28 | rexbidv 3173 |
. . . . . . . . . 10
⊢ (𝑟 = (𝑅‘𝐼) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)
↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿))) |
30 | 29 | abbidv 2796 |
. . . . . . . . 9
⊢ (𝑟 = (𝑅‘𝐼) → {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)} =
{𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)}) |
31 | 30 | uneq2d 4159 |
. . . . . . . 8
⊢ (𝑟 = (𝑅‘𝐼) → ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)}) =
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})) |
32 | 31 | uneq2d 4159 |
. . . . . . 7
⊢ (𝑟 = (𝑅‘𝐼) → (𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})) =
(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)}))) |
33 | | id 22 |
. . . . . . . 8
⊢ (𝑟 = (𝑅‘𝐼) → 𝑟 = (𝑅‘𝐼)) |
34 | | rexeq 3316 |
. . . . . . . . . . 11
⊢ (𝑟 = (𝑅‘𝐼) → (∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)
↔ ∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅))) |
35 | 34 | rexbidv 3173 |
. . . . . . . . . 10
⊢ (𝑟 = (𝑅‘𝐼) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅))) |
36 | 35 | abbidv 2796 |
. . . . . . . . 9
⊢ (𝑟 = (𝑅‘𝐼) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝑅 ∈
(𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}) |
37 | 36 | uneq2d 4159 |
. . . . . . . 8
⊢ (𝑟 = (𝑅‘𝐼) → ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}) =
({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)})) |
38 | 33, 37 | uneq12d 4160 |
. . . . . . 7
⊢ (𝑟 = (𝑅‘𝐼) → (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)})) =
((𝑅‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))) |
39 | 32, 38 | opeq12d 4877 |
. . . . . 6
⊢ (𝑟 = (𝑅‘𝐼) → 〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 = 〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉) |
40 | 27, 39 | csbie 3925 |
. . . . 5
⊢
⦋(𝑅‘𝐼) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 = 〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 |
41 | 40 | csbeq2i 3897 |
. . . 4
⊢
⦋(𝐿‘𝐼) / 𝑙⦌⦋(𝑅‘𝐼) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 =
⦋(𝐿‘𝐼) / 𝑙⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 |
42 | | fvex 6904 |
. . . . 5
⊢ (𝐿‘𝐼) ∈ V |
43 | | id 22 |
. . . . . . 7
⊢ (𝑙 = (𝐿‘𝐼) → 𝑙 = (𝐿‘𝐼)) |
44 | | rexeq 3316 |
. . . . . . . . . 10
⊢ (𝑙 = (𝐿‘𝐼) → (∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)
↔ ∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅))) |
45 | 44 | rexbidv 3173 |
. . . . . . . . 9
⊢ (𝑙 = (𝐿‘𝐼) → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)
↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅))) |
46 | 45 | abbidv 2796 |
. . . . . . . 8
⊢ (𝑙 = (𝐿‘𝐼) → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)} =
{𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈
(𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}) |
47 | 46 | uneq1d 4158 |
. . . . . . 7
⊢ (𝑙 = (𝐿‘𝐼) → ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)}) =
({𝑎 ∣ ∃𝑥𝑅 ∈ ( R
‘𝐴)∃𝑦𝐿 ∈
(𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})) |
48 | 43, 47 | uneq12d 4160 |
. . . . . 6
⊢ (𝑙 = (𝐿‘𝐼) → (𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)})) =
((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝑅)}
∪ {𝑎 ∣
∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝐿)}))) |
49 | | rexeq 3316 |
. . . . . . . . . 10
⊢ (𝑙 = (𝐿‘𝐼) → (∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)
↔ ∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿))) |
50 | 49 | rexbidv 3173 |
. . . . . . . . 9
⊢ (𝑙 = (𝐿‘𝐼) → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)
↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿))) |
51 | 50 | abbidv 2796 |
. . . . . . . 8
⊢ (𝑙 = (𝐿‘𝐼) → {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)} =
{𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}) |
52 | 51 | uneq1d 4158 |
. . . . . . 7
⊢ (𝑙 = (𝐿‘𝐼) → ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}) =
({𝑎 ∣ ∃𝑥𝐿 ∈
{𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)})) |
53 | 52 | uneq2d 4159 |
. . . . . 6
⊢ (𝑙 = (𝐿‘𝐼) → ((𝑅‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)})) =
((𝑅‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s
𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿
-s 𝐴)
·s 𝑦𝐿)) /su
𝑥𝐿)}
∪ {𝑎 ∣
∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅
-s 𝐴)
·s 𝑦𝑅)) /su
𝑥𝑅)}))) |
54 | 48, 53 | opeq12d 4877 |
. . . . 5
⊢ (𝑙 = (𝐿‘𝐼) → 〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 =
〈((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉) |
55 | 42, 54 | csbie 3925 |
. . . 4
⊢
⦋(𝐿‘𝐼) / 𝑙⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 =
〈((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 |
56 | 41, 55 | eqtri 2755 |
. . 3
⊢
⦋(𝐿‘𝐼) / 𝑙⦌⦋(𝑅‘𝐼) / 𝑟⦌〈(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 =
〈((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉 |
57 | 26, 56 | eqtr3di 2782 |
. 2
⊢ (𝐼 ∈ ω →
⦋(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
𝑥𝑅)}))〉 =
〈((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉) |
58 | 11, 57 | eqtrd 2767 |
1
⊢ (𝐼 ∈ ω → (𝐹‘suc 𝐼) = 〈((𝐿‘𝐼) ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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
𝑥𝑅)}))〉) |