Theorem precsexlem3 28622

Description: Lemma for surreal reciprocals. Calculate the value of the recursive function at a successor. (Contributed by Scott Fenton, 12-Mar-2025.)

Hypotheses

Ref	Expression
precsexlem.1	⊢ 𝐹 = 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 }, ∅⟩)
precsexlem.2	⊢ 𝐿 = (1st ∘ 𝐹)
precsexlem.3	⊢ 𝑅 = (2nd ∘ 𝐹)

Assertion

Ref	Expression
precsexlem3	⊢ (𝐼 ∈ ω → (𝐹‘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 𝑥𝑅)}))⟩)

Distinct variable groups:   𝐴,𝑎,𝑙,𝑝,𝑟,𝑥,𝑥_𝐿,𝑥_𝑅   𝐹,𝑙,𝑝   𝐼,𝑎,𝑙,𝑝,𝑟,𝑥,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅   𝐿,𝑎,𝑙,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿   𝑅,𝑎,𝑙,𝑟,𝑥_𝐿,𝑥_𝑅,𝑦_𝑅

Allowed substitution hints:   𝐴(𝑦_𝐿, 𝑦_𝑅)   𝑅(𝑥, 𝑝, 𝑦_𝐿)   𝐹(𝑥, 𝑟, 𝑎, 𝑥_𝐿, 𝑥_𝑅, 𝑦_𝐿, 𝑦_𝑅)   𝐿(𝑥, 𝑟, 𝑝, 𝑦_𝑅)

Proof of Theorem precsexlem3

Step	Hyp	Ref	Expression
1		nnon 7904	. . 3 ⊢ (𝐼 ∈ ω → 𝐼 ∈ On)
2		opex 5436	. . . . 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 5268	. . . 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 5268	. . 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 6905	. . . . 5 ⊢ (𝑝 = (𝐹‘𝐼) → (1st ‘𝑝) = (1st ‘(𝐹‘𝐼)))
7		fveq2 6905	. . . . . 6 ⊢ (𝑝 = (𝐹‘𝐼) → (2nd ‘𝑝) = (2nd ‘(𝐹‘𝐼)))
8	7	csbeq1d 3855	. . . . 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 3860	. . . 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 8464	. . 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 598	. 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 6906	. . . . 5 ⊢ (𝐿‘𝐼) = ((1st ∘ 𝐹)‘𝐼)
14		rdgfnon 8451	. . . . . . 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 6655	. . . . . . 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 234	. . . . . 6 ⊢ 𝐹 Fn On
17		fvco2 7002	. . . . . 6 ⊢ ((𝐹 Fn On ∧ 𝐼 ∈ On) → ((1st ∘ 𝐹)‘𝐼) = (1st ‘(𝐹‘𝐼)))
18	16, 1, 17	sylancr 599	. . . . 5 ⊢ (𝐼 ∈ ω → ((1st ∘ 𝐹)‘𝐼) = (1st ‘(𝐹‘𝐼)))
19	13, 18	eqtrid 2810	. . . 4 ⊢ (𝐼 ∈ ω → (𝐿‘𝐼) = (1st ‘(𝐹‘𝐼)))
20		precsexlem.3	. . . . . . 7 ⊢ 𝑅 = (2nd ∘ 𝐹)
21	20	fveq1i 6906	. . . . . 6 ⊢ (𝑅‘𝐼) = ((2nd ∘ 𝐹)‘𝐼)
22		fvco2 7002	. . . . . . 7 ⊢ ((𝐹 Fn On ∧ 𝐼 ∈ On) → ((2nd ∘ 𝐹)‘𝐼) = (2nd ‘(𝐹‘𝐼)))
23	16, 1, 22	sylancr 599	. . . . . 6 ⊢ (𝐼 ∈ ω → ((2nd ∘ 𝐹)‘𝐼) = (2nd ‘(𝐹‘𝐼)))
24	21, 23	eqtrid 2810	. . . . 5 ⊢ (𝐼 ∈ ω → (𝑅‘𝐼) = (2nd ‘(𝐹‘𝐼)))
25	24	csbeq1d 3855	. . . 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 3860	. . 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 6918	. . . . . 6 ⊢ (𝑅‘𝐼) ∈ V
28		rexeq 3319	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑅‘𝐼) → (∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
29	28	rexbidv 3190	. . . . . . . . . 10 ⊢ (𝑟 = (𝑅‘𝐼) → (∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
30	29	abbidv 2829	. . . . . . . . 9 ⊢ (𝑟 = (𝑅‘𝐼) → {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} = {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})
31	30	uneq2d 4170	. . . . . . . 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 4170	. . . . . . 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 23	. . . . . . . 8 ⊢ (𝑟 = (𝑅‘𝐼) → 𝑟 = (𝑅‘𝐼))
34		rexeq 3319	. . . . . . . . . . 11 ⊢ (𝑟 = (𝑅‘𝐼) → (∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
35	34	rexbidv 3190	. . . . . . . . . 10 ⊢ (𝑟 = (𝑅‘𝐼) → (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
36	35	abbidv 2829	. . . . . . . . 9 ⊢ (𝑟 = (𝑅‘𝐼) → {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} = {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝑅 ∈ (𝑅‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})
37	36	uneq2d 4170	. . . . . . . 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 4171	. . . . . . 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 4851	. . . . . 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 3886	. . . . 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 3859	. . . 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 6918	. . . . 5 ⊢ (𝐿‘𝐼) ∈ V
43		id 23	. . . . . . 7 ⊢ (𝑙 = (𝐿‘𝐼) → 𝑙 = (𝐿‘𝐼))
44		rexeq 3319	. . . . . . . . . 10 ⊢ (𝑙 = (𝐿‘𝐼) → (∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
45	44	rexbidv 3190	. . . . . . . . 9 ⊢ (𝑙 = (𝐿‘𝐼) → (∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
46	45	abbidv 2829	. . . . . . . 8 ⊢ (𝑙 = (𝐿‘𝐼) → {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} = {𝑎 ∣ ∃𝑥𝑅 ∈ (R‘𝐴)∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝑅 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)})
47	46	uneq1d 4169	. . . . . . 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 4171	. . . . . 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 3319	. . . . . . . . . 10 ⊢ (𝑙 = (𝐿‘𝐼) → (∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
50	49	rexbidv 3190	. . . . . . . . 9 ⊢ (𝑙 = (𝐿‘𝐼) → (∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
51	50	abbidv 2829	. . . . . . . 8 ⊢ (𝑙 = (𝐿‘𝐼) → {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} = {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ (L‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ (𝐿‘𝐼)𝑎 = (( 1s +s ((𝑥𝐿 −s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)})
52	51	uneq1d 4169	. . . . . . 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 4170	. . . . . 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 4851	. . . . 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 3886	. . . 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 2786	. . 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 2813	. 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 2798	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 𝑥𝑅)}))⟩)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ∈ wcel 2147  {cab 2741  ∃wrex 3090  {crab 3416  Vcvv 3454  ⦋csb 3851   ∪ cun 4152  ∅c0 4281  {csn 4588  ⟨cop 4838   class class class wbr 5106   ↦ cmpt 5189   ∘ ccom 5659  Oncon0 6377  suc csuc 6379   Fn wfn 6550  ‘cfv 6555  (class class class)co 7440  ωcom 7898  1^st c1st 8020  2^nd c2nd 8021  reccrdg 8442   <s clts 28025   0_s c0s 28218   1_s c1s 28219  Lcleft 28238  Rcright 28239   +_s cadds 28372   −_s csubs 28433   ·_s cmuls 28519   /_su cdivs 28600

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-rep 5235  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7772

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-iun 4956  df-br 5107  df-opab 5171  df-mpt 5190  df-tr 5216  df-id 5550  df-eprel 5555  df-po 5563  df-so 5564  df-fr 5608  df-we 5610  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668  df-pred 6319  df-ord 6380  df-on 6381  df-lim 6382  df-suc 6383  df-iota 6509  df-fun 6557  df-fn 6558  df-f 6559  df-f1 6560  df-fo 6561  df-f1o 6562  df-fv 6563  df-ov 7443  df-om 7899  df-2nd 8023  df-frecs 8324  df-wrecs 8355  df-recs 8404  df-rdg 8443

This theorem is used by:  precsexlem4  28623  precsexlem5  28624