| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | breq2 5147 | . . . 4
⊢ (𝑧 = 𝑥𝑂 → ( 0s
<s 𝑧 ↔
0s <s 𝑥𝑂)) | 
| 2 |  | oveq1 7438 | . . . . . 6
⊢ (𝑧 = 𝑥𝑂 → (𝑧 ·s 𝑦) = (𝑥𝑂 ·s
𝑦)) | 
| 3 | 2 | eqeq1d 2739 | . . . . 5
⊢ (𝑧 = 𝑥𝑂 → ((𝑧 ·s 𝑦) = 1s ↔ (𝑥𝑂
·s 𝑦) =
1s )) | 
| 4 | 3 | rexbidv 3179 | . . . 4
⊢ (𝑧 = 𝑥𝑂 → (∃𝑦 ∈ 
No  (𝑧
·s 𝑦) =
1s ↔ ∃𝑦 ∈  No 
(𝑥𝑂
·s 𝑦) =
1s )) | 
| 5 | 1, 4 | imbi12d 344 | . . 3
⊢ (𝑧 = 𝑥𝑂 → (( 0s
<s 𝑧 → ∃𝑦 ∈ 
No  (𝑧
·s 𝑦) =
1s ) ↔ ( 0s <s 𝑥𝑂 → ∃𝑦 ∈ 
No  (𝑥𝑂 ·s
𝑦) = 1s
))) | 
| 6 |  | breq2 5147 | . . . 4
⊢ (𝑧 = 𝐴 → ( 0s <s 𝑧 ↔ 0s <s
𝐴)) | 
| 7 |  | oveq1 7438 | . . . . . 6
⊢ (𝑧 = 𝐴 → (𝑧 ·s 𝑦) = (𝐴 ·s 𝑦)) | 
| 8 | 7 | eqeq1d 2739 | . . . . 5
⊢ (𝑧 = 𝐴 → ((𝑧 ·s 𝑦) = 1s ↔ (𝐴 ·s 𝑦) = 1s )) | 
| 9 | 8 | rexbidv 3179 | . . . 4
⊢ (𝑧 = 𝐴 → (∃𝑦 ∈  No 
(𝑧 ·s
𝑦) = 1s ↔
∃𝑦 ∈  No  (𝐴 ·s 𝑦) = 1s )) | 
| 10 | 6, 9 | imbi12d 344 | . . 3
⊢ (𝑧 = 𝐴 → (( 0s <s 𝑧 → ∃𝑦 ∈ 
No  (𝑧
·s 𝑦) =
1s ) ↔ ( 0s <s 𝐴 → ∃𝑦 ∈  No 
(𝐴 ·s
𝑦) = 1s
))) | 
| 11 |  | eqid 2737 | . . . . . . . . 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 }, ∅〉) = 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 }, ∅〉) | 
| 12 | 11 | precsexlemcbv 28230 | . . . . . . . 8
⊢
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 }, ∅〉) = 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 }, ∅〉) | 
| 13 |  | eqid 2737 | . . . . . . . 8
⊢
(1st ∘ 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 }, ∅〉)) = (1st ∘ 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 }, ∅〉)) | 
| 14 |  | eqid 2737 | . . . . . . . 8
⊢
(2nd ∘ 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 }, ∅〉)) = (2nd ∘ 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 }, ∅〉)) | 
| 15 |  | simp1 1137 | . . . . . . . 8
⊢ ((𝑧 ∈ 
No  ∧ 0s <s 𝑧 ∧ ∀𝑥𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s ))
→ 𝑧 ∈  No ) | 
| 16 |  | simp2 1138 | . . . . . . . 8
⊢ ((𝑧 ∈ 
No  ∧ 0s <s 𝑧 ∧ ∀𝑥𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s ))
→ 0s <s 𝑧) | 
| 17 |  | simp3 1139 | . . . . . . . 8
⊢ ((𝑧 ∈ 
No  ∧ 0s <s 𝑧 ∧ ∀𝑥𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s ))
→ ∀𝑥𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s
)) | 
| 18 | 12, 13, 14, 15, 16, 17 | precsexlem10 28240 | . . . . . . 7
⊢ ((𝑧 ∈ 
No  ∧ 0s <s 𝑧 ∧ ∀𝑥𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s ))
→ ∪ ((1st ∘ 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 }, ∅〉)) “ ω) <<s ∪ ((2nd ∘ 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 }, ∅〉)) “ ω)) | 
| 19 | 18 | scutcld 27848 | . . . . . 6
⊢ ((𝑧 ∈ 
No  ∧ 0s <s 𝑧 ∧ ∀𝑥𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s ))
→ (∪ ((1st ∘ 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 }, ∅〉)) “ ω) |s ∪ ((2nd ∘ 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 }, ∅〉)) “ ω)) ∈  No ) | 
| 20 |  | eqid 2737 | . . . . . . 7
⊢ (∪ ((1st ∘ 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 }, ∅〉)) “ ω) |s ∪ ((2nd ∘ 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 }, ∅〉)) “ ω)) = (∪ ((1st ∘ 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 }, ∅〉)) “ ω) |s ∪ ((2nd ∘ 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 }, ∅〉)) “ ω)) | 
| 21 | 12, 13, 14, 15, 16, 17, 20 | precsexlem11 28241 | . . . . . 6
⊢ ((𝑧 ∈ 
No  ∧ 0s <s 𝑧 ∧ ∀𝑥𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s ))
→ (𝑧
·s (∪ ((1st ∘
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 }, ∅〉)) “ ω) |s ∪ ((2nd ∘ 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 }, ∅〉)) “ ω))) = 1s
) | 
| 22 |  | oveq2 7439 | . . . . . . . 8
⊢ (𝑦 = (∪
((1st ∘ 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 }, ∅〉)) “ ω) |s ∪ ((2nd ∘ 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 }, ∅〉)) “ ω)) → (𝑧 ·s 𝑦) = (𝑧 ·s (∪ ((1st ∘ 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 }, ∅〉)) “ ω) |s ∪ ((2nd ∘ 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 }, ∅〉)) “ ω)))) | 
| 23 | 22 | eqeq1d 2739 | . . . . . . 7
⊢ (𝑦 = (∪
((1st ∘ 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 }, ∅〉)) “ ω) |s ∪ ((2nd ∘ 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 }, ∅〉)) “ ω)) → ((𝑧 ·s 𝑦) = 1s ↔ (𝑧 ·s (∪ ((1st ∘ 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 }, ∅〉)) “ ω) |s ∪ ((2nd ∘ 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 }, ∅〉)) “ ω))) = 1s
)) | 
| 24 | 23 | rspcev 3622 | . . . . . 6
⊢ (((∪ ((1st ∘ 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 }, ∅〉)) “ ω) |s ∪ ((2nd ∘ 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 }, ∅〉)) “ ω)) ∈  No  ∧ (𝑧 ·s (∪ ((1st ∘ 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 }, ∅〉)) “ ω) |s ∪ ((2nd ∘ 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 }, ∅〉)) “ ω))) = 1s ) →
∃𝑦 ∈  No  (𝑧 ·s 𝑦) = 1s ) | 
| 25 | 19, 21, 24 | syl2anc 584 | . . . . 5
⊢ ((𝑧 ∈ 
No  ∧ 0s <s 𝑧 ∧ ∀𝑥𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s ))
→ ∃𝑦 ∈
 No  (𝑧 ·s 𝑦) = 1s ) | 
| 26 | 25 | 3exp 1120 | . . . 4
⊢ (𝑧 ∈ 
No  → ( 0s <s 𝑧 → (∀𝑥𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s ) →
∃𝑦 ∈  No  (𝑧 ·s 𝑦) = 1s ))) | 
| 27 | 26 | com23 86 | . . 3
⊢ (𝑧 ∈ 
No  → (∀𝑥𝑂 ∈ (( L ‘𝑧) ∪ ( R ‘𝑧))( 0s <s 𝑥𝑂 →
∃𝑦 ∈  No  (𝑥𝑂 ·s
𝑦) = 1s ) →
( 0s <s 𝑧
→ ∃𝑦 ∈
 No  (𝑧 ·s 𝑦) = 1s ))) | 
| 28 | 5, 10, 27 | noinds 27978 | . 2
⊢ (𝐴 ∈ 
No  → ( 0s <s 𝐴 → ∃𝑦 ∈  No 
(𝐴 ·s
𝑦) = 1s
)) | 
| 29 | 28 | imp 406 | 1
⊢ ((𝐴 ∈ 
No  ∧ 0s <s 𝐴) → ∃𝑦 ∈  No 
(𝐴 ·s
𝑦) = 1s
) |