Proof of Theorem precsexlem2
| Step | Hyp | Ref
| Expression |
| 1 | | precsexlem.3 |
. . 3
⊢ 𝑅 = (2nd ∘ 𝐹) |
| 2 | 1 | fveq1i 6907 |
. 2
⊢ (𝑅‘∅) =
((2nd ∘ 𝐹)‘∅) |
| 3 | | rdgfnon 8458 |
. . . 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 }, ∅〉) Fn On |
| 4 | | precsexlem.1 |
. . . . 5
⊢ 𝐹 = 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 | 4 | fneq1i 6665 |
. . . 4
⊢ (𝐹 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) |
| 6 | 3, 5 | mpbir 231 |
. . 3
⊢ 𝐹 Fn On |
| 7 | | 0elon 6438 |
. . 3
⊢ ∅
∈ On |
| 8 | | fvco2 7006 |
. . 3
⊢ ((𝐹 Fn On ∧ ∅ ∈ On)
→ ((2nd ∘ 𝐹)‘∅) = (2nd
‘(𝐹‘∅))) |
| 9 | 6, 7, 8 | mp2an 692 |
. 2
⊢
((2nd ∘ 𝐹)‘∅) = (2nd
‘(𝐹‘∅)) |
| 10 | 4 | fveq1i 6907 |
. . . . 5
⊢ (𝐹‘∅) = (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 }, ∅〉)‘∅) |
| 11 | | opex 5469 |
. . . . . 6
⊢ 〈{
0s }, ∅〉 ∈ V |
| 12 | 11 | rdg0 8461 |
. . . . 5
⊢
(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 }, ∅〉)‘∅) = 〈{ 0s },
∅〉 |
| 13 | 10, 12 | eqtri 2765 |
. . . 4
⊢ (𝐹‘∅) = 〈{
0s }, ∅〉 |
| 14 | 13 | fveq2i 6909 |
. . 3
⊢
(2nd ‘(𝐹‘∅)) = (2nd
‘〈{ 0s }, ∅〉) |
| 15 | | snex 5436 |
. . . 4
⊢ {
0s } ∈ V |
| 16 | | 0ex 5307 |
. . . 4
⊢ ∅
∈ V |
| 17 | 15, 16 | op2nd 8023 |
. . 3
⊢
(2nd ‘〈{ 0s }, ∅〉) =
∅ |
| 18 | 14, 17 | eqtri 2765 |
. 2
⊢
(2nd ‘(𝐹‘∅)) = ∅ |
| 19 | 2, 9, 18 | 3eqtri 2769 |
1
⊢ (𝑅‘∅) =
∅ |