Theorem precsexlemcbv 28165

Description: Lemma for surreal reciprocals. Change some bound variables. (Contributed by Scott Fenton, 15-Mar-2025.)

Hypothesis

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 }, ∅⟩)

Assertion

Ref	Expression
precsexlemcbv	⊢ 𝐹 = 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 }, ∅⟩)

Distinct variable group:   𝐴,𝑝,𝑞,𝑙,𝑚,𝑟,𝑠,𝑎,𝑏,𝑥_𝐿,𝑥_𝑅,𝑧_𝐿,𝑧_𝑅,𝑦_𝐿,𝑦_𝑅,𝑤,𝑡,𝑥,𝑧

Allowed substitution hints:   𝐹(𝑥,𝑧,𝑤,𝑡,𝑚,𝑠,𝑟,𝑞,𝑝,𝑎,𝑏,𝑙,𝑥_𝐿,𝑥_𝑅,𝑦_𝐿,𝑦_𝑅,𝑧_𝐿,𝑧_𝑅)

Proof of Theorem precsexlemcbv

Step	Hyp	Ref	Expression
1		precsexlem.1	. 2 ⊢ 𝐹 = 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 }, ∅⟩)
2		fveq2 6881	. . . . . 6 ⊢ (𝑝 = 𝑞 → (1st ‘𝑝) = (1st ‘𝑞))
3		fveq2 6881	. . . . . . 7 ⊢ (𝑝 = 𝑞 → (2nd ‘𝑝) = (2nd ‘𝑞))
4	3	csbeq1d 3883	. . . . . 6 ⊢ (𝑝 = 𝑞 → ⦋(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 𝑥𝑅)}))⟩)
5	2, 4	csbeq12dv 3888	. . . . 5 ⊢ (𝑝 = 𝑞 → ⦋(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 𝑥𝑅)}))⟩)
6		rexeq 3305	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑠 → (∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
7	6	rexbidv 3165	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑠 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
8	7	abbidv 2802	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑠 → {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} = {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)})
9	8	uneq2d 4148	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑠 → ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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 𝑥𝐿)}))
10	9	uneq2d 4148	. . . . . . . . . 10 ⊢ (𝑟 = 𝑠 → (𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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 𝑥𝐿)})))
11		id 22	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑠 → 𝑟 = 𝑠)
12		rexeq 3305	. . . . . . . . . . . . . 14 ⊢ (𝑟 = 𝑠 → (∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
13	12	rexbidv 3165	. . . . . . . . . . . . 13 ⊢ (𝑟 = 𝑠 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
14	13	abbidv 2802	. . . . . . . . . . . 12 ⊢ (𝑟 = 𝑠 → {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑟 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} = {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)})
15	14	uneq2d 4148	. . . . . . . . . . 11 ⊢ (𝑟 = 𝑠 → ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( 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 𝑥𝑅)}))
16	11, 15	uneq12d 4149	. . . . . . . . . 10 ⊢ (𝑟 = 𝑠 → (𝑟 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( 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 𝑥𝑅)})))
17	10, 16	opeq12d 4862	. . . . . . . . 9 ⊢ (𝑟 = 𝑠 → ⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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 𝑥𝑅)}))⟩)
18		eqeq1 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ 𝑏 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
19	18	2rexbidv 3210	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑏 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)))
20		oveq1 7417	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝑅 = 𝑧𝑅 → (𝑥𝑅 -s 𝐴) = (𝑧𝑅 -s 𝐴))
21	20	oveq1d 7425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑅 = 𝑧𝑅 → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿) = ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿))
22	21	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑅 = 𝑧𝑅 → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿)))
23		id 22	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑅 = 𝑧𝑅 → 𝑥𝑅 = 𝑧𝑅)
24	22, 23	oveq12d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑅 = 𝑧𝑅 → (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑧𝑅))
25	24	eqeq2d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑅 = 𝑧𝑅 → (𝑏 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑧𝑅)))
26		oveq2 7418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝐿 = 𝑤 → ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿) = ((𝑧𝑅 -s 𝐴) ·s 𝑤))
27	26	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝐿 = 𝑤 → ( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)))
28	27	oveq1d 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝐿 = 𝑤 → (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑧𝑅) = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅))
29	28	eqeq2d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝐿 = 𝑤 → (𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑧𝑅) ↔ 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅)))
30	25, 29	cbvrex2vw 3229	. . . . . . . . . . . . . 14 ⊢ (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑏 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅))
31	19, 30	bitrdi 287	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑏 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅) ↔ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅)))
32	31	cbvabv 2806	. . . . . . . . . . . 12 ⊢ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝑅)} = {𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅)}
33		eqeq1 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ 𝑏 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
34	33	2rexbidv 3210	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑠 𝑏 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)))
35		oveq1 7417	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥𝐿 = 𝑧𝐿 → (𝑥𝐿 -s 𝐴) = (𝑧𝐿 -s 𝐴))
36	35	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝐿 = 𝑧𝐿 → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅) = ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅))
37	36	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝐿 = 𝑧𝐿 → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅)))
38		id 22	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝐿 = 𝑧𝐿 → 𝑥𝐿 = 𝑧𝐿)
39	37, 38	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝐿 = 𝑧𝐿 → (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑧𝐿))
40	39	eqeq2d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝐿 = 𝑧𝐿 → (𝑏 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑧𝐿)))
41		oveq2 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦𝑅 = 𝑡 → ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅) = ((𝑧𝐿 -s 𝐴) ·s 𝑡))
42	41	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑅 = 𝑡 → ( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡)))
43	42	oveq1d 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑅 = 𝑡 → (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑧𝐿) = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿))
44	43	eqeq2d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑅 = 𝑡 → (𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑧𝐿) ↔ 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿)))
45	40, 44	cbvrex2vw 3229	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑠 𝑏 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑧𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿))
46		breq2 5128	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 𝑧 → ( 0s <s 𝑥 ↔ 0s <s 𝑧))
47	46	cbvrabv 3431	. . . . . . . . . . . . . . . 16 ⊢ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥} = {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}
48	47	rexeqi 3308	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿) ↔ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿))
49	45, 48	bitri 275	. . . . . . . . . . . . . 14 ⊢ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑠 𝑏 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿))
50	34, 49	bitrdi 287	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑏 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿) ↔ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿)))
51	50	cbvabv 2806	. . . . . . . . . . . 12 ⊢ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝐿)} = {𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑡)) /su 𝑧𝐿)}
52	32, 51	uneq12i 4146	. . . . . . . . . . 11 ⊢ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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 𝑧𝐿)})
53	52	uneq2i 4145	. . . . . . . . . 10 ⊢ (𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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 𝑧𝐿)}))
54		eqeq1 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ 𝑏 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
55	54	2rexbidv 3210	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑏 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)))
56	35	oveq1d 7425	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥𝐿 = 𝑧𝐿 → ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿) = ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿))
57	56	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝐿 = 𝑧𝐿 → ( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿)))
58	57, 38	oveq12d 7428	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝐿 = 𝑧𝐿 → (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑧𝐿))
59	58	eqeq2d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝐿 = 𝑧𝐿 → (𝑏 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑧𝐿)))
60		oveq2 7418	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑦𝐿 = 𝑤 → ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿) = ((𝑧𝐿 -s 𝐴) ·s 𝑤))
61	60	oveq2d 7426	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝐿 = 𝑤 → ( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿)) = ( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)))
62	61	oveq1d 7425	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝐿 = 𝑤 → (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑧𝐿) = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿))
63	62	eqeq2d 2747	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝐿 = 𝑤 → (𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑧𝐿) ↔ 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿)))
64	59, 63	cbvrex2vw 3229	. . . . . . . . . . . . . . 15 ⊢ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑏 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑧𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿))
65	47	rexeqi 3308	. . . . . . . . . . . . . . 15 ⊢ (∃𝑧𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿) ↔ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿))
66	64, 65	bitri 275	. . . . . . . . . . . . . 14 ⊢ (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑏 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿))
67	55, 66	bitrdi 287	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑏 → (∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿) ↔ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿)))
68	67	cbvabv 2806	. . . . . . . . . . . 12 ⊢ {𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( L ‘𝐴) ∣ 0s <s 𝑥}∃𝑦𝐿 ∈ 𝑙 𝑎 = (( 1s +s ((𝑥𝐿 -s 𝐴) ·s 𝑦𝐿)) /su 𝑥𝐿)} = {𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿)}
69		eqeq1 2740	. . . . . . . . . . . . . . 15 ⊢ (𝑎 = 𝑏 → (𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ 𝑏 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
70	69	2rexbidv 3210	. . . . . . . . . . . . . 14 ⊢ (𝑎 = 𝑏 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑏 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)))
71	20	oveq1d 7425	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥𝑅 = 𝑧𝑅 → ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅) = ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅))
72	71	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥𝑅 = 𝑧𝑅 → ( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅)))
73	72, 23	oveq12d 7428	. . . . . . . . . . . . . . . 16 ⊢ (𝑥𝑅 = 𝑧𝑅 → (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑧𝑅))
74	73	eqeq2d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑥𝑅 = 𝑧𝑅 → (𝑏 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑧𝑅)))
75		oveq2 7418	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑦𝑅 = 𝑡 → ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅) = ((𝑧𝑅 -s 𝐴) ·s 𝑡))
76	75	oveq2d 7426	. . . . . . . . . . . . . . . . 17 ⊢ (𝑦𝑅 = 𝑡 → ( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅)) = ( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑡)))
77	76	oveq1d 7425	. . . . . . . . . . . . . . . 16 ⊢ (𝑦𝑅 = 𝑡 → (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑧𝑅) = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑡)) /su 𝑧𝑅))
78	77	eqeq2d 2747	. . . . . . . . . . . . . . 15 ⊢ (𝑦𝑅 = 𝑡 → (𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑧𝑅) ↔ 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑡)) /su 𝑧𝑅)))
79	74, 78	cbvrex2vw 3229	. . . . . . . . . . . . . 14 ⊢ (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑏 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑡)) /su 𝑧𝑅))
80	70, 79	bitrdi 287	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝑏 → (∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅) ↔ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑡)) /su 𝑧𝑅)))
81	80	cbvabv 2806	. . . . . . . . . . . 12 ⊢ {𝑎 ∣ ∃𝑥𝑅 ∈ ( R ‘𝐴)∃𝑦𝑅 ∈ 𝑠 𝑎 = (( 1s +s ((𝑥𝑅 -s 𝐴) ·s 𝑦𝑅)) /su 𝑥𝑅)} = {𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑡 ∈ 𝑠 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑡)) /su 𝑧𝑅)}
82	68, 81	uneq12i 4146	. . . . . . . . . . 11 ⊢ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( 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 𝑧𝑅)})
83	82	uneq2i 4145	. . . . . . . . . 10 ⊢ (𝑠 ∪ ({𝑎 ∣ ∃𝑥𝐿 ∈ {𝑥 ∈ ( 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 𝑧𝑅)}))
84	53, 83	opeq12i 4859	. . . . . . . . 9 ⊢ ⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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 𝑧𝑅)}))⟩
85	17, 84	eqtrdi 2787	. . . . . . . 8 ⊢ (𝑟 = 𝑠 → ⟨(𝑙 ∪ ({𝑎 ∣ ∃𝑥𝑅 ∈ ( 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 𝑧𝑅)}))⟩)
86	85	cbvcsbv 3891	. . . . . . 7 ⊢ ⦋(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 𝑧𝑅)}))⟩
87	86	csbeq2i 3887	. . . . . 6 ⊢ ⦋(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 𝑧𝑅)}))⟩
88		id 22	. . . . . . . . . 10 ⊢ (𝑙 = 𝑚 → 𝑙 = 𝑚)
89		rexeq 3305	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑚 → (∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅) ↔ ∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅)))
90	89	rexbidv 3165	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑚 → (∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅) ↔ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅)))
91	90	abbidv 2802	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑚 → {𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅)} = {𝑏 ∣ ∃𝑧𝑅 ∈ ( R ‘𝐴)∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝑅 -s 𝐴) ·s 𝑤)) /su 𝑧𝑅)})
92	91	uneq1d 4147	. . . . . . . . . 10 ⊢ (𝑙 = 𝑚 → ({𝑏 ∣ ∃𝑧𝑅 ∈ ( 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 𝑧𝐿)}))
93	88, 92	uneq12d 4149	. . . . . . . . 9 ⊢ (𝑙 = 𝑚 → (𝑙 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( 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 𝑧𝐿)})))
94		rexeq 3305	. . . . . . . . . . . . 13 ⊢ (𝑙 = 𝑚 → (∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿) ↔ ∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿)))
95	94	rexbidv 3165	. . . . . . . . . . . 12 ⊢ (𝑙 = 𝑚 → (∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿) ↔ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿)))
96	95	abbidv 2802	. . . . . . . . . . 11 ⊢ (𝑙 = 𝑚 → {𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑤 ∈ 𝑙 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿)} = {𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( L ‘𝐴) ∣ 0s <s 𝑧}∃𝑤 ∈ 𝑚 𝑏 = (( 1s +s ((𝑧𝐿 -s 𝐴) ·s 𝑤)) /su 𝑧𝐿)})
97	96	uneq1d 4147	. . . . . . . . . 10 ⊢ (𝑙 = 𝑚 → ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( 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 𝑧𝑅)}))
98	97	uneq2d 4148	. . . . . . . . 9 ⊢ (𝑙 = 𝑚 → (𝑠 ∪ ({𝑏 ∣ ∃𝑧𝐿 ∈ {𝑧 ∈ ( 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 𝑧𝑅)})))
99	93, 98	opeq12d 4862	. . . . . . . 8 ⊢ (𝑙 = 𝑚 → ⟨(𝑙 ∪ ({𝑏 ∣ ∃𝑧𝑅 ∈ ( 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 𝑧𝑅)}))⟩)
100	99	csbeq2dv 3886	. . . . . . 7 ⊢ (𝑙 = 𝑚 → ⦋(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 𝑧𝑅)}))⟩)
101	100	cbvcsbv 3891	. . . . . 6 ⊢ ⦋(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 𝑧𝑅)}))⟩
102	87, 101	eqtri 2759	. . . . 5 ⊢ ⦋(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 𝑧𝑅)}))⟩
103	5, 102	eqtrdi 2787	. . . 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 𝑧𝑅)}))⟩)
104	103	cbvmptv 5230	. . 3 ⊢ (𝑝 ∈ 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 𝑥𝑅)}))⟩) = (𝑞 ∈ 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 𝑧𝑅)}))⟩)
105		rdgeq1 8430	. . 3 ⊢ ((𝑝 ∈ 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 𝑥𝑅)}))⟩) = (𝑞 ∈ 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 𝑧𝑅)}))⟩) → 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 }, ∅⟩))
106	104, 105	ax-mp 5	. 2 ⊢ 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 }, ∅⟩)
107	1, 106	eqtri 2759	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 }, ∅⟩)

Syntax hints:   = wceq 1540  {cab 2714  ∃wrex 3061  {crab 3420  Vcvv 3464  ⦋csb 3879   ∪ cun 3929  ∅c0 4313  {csn 4606  ⟨cop 4612   class class class wbr 5124   ↦ cmpt 5206  ‘cfv 6536  (class class class)co 7410  1^st c1st 7991  2^nd c2nd 7992  reccrdg 8428   <s cslt 27609   0_s c0s 27791   1_s c1s 27792   L cleft 27810   R cright 27811   +_s cadds 27923   -_s csubs 27983   ·_s cmuls 28066   /_su cdivs 28147

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2715  df-cleq 2728  df-clel 2810  df-ral 3053  df-rex 3062  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-if 4506  df-sn 4607  df-pr 4609  df-op 4613  df-uni 4889  df-br 5125  df-opab 5187  df-mpt 5207  df-xp 5665  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-pred 6295  df-iota 6489  df-fv 6544  df-ov 7413  df-frecs 8285  df-wrecs 8316  df-recs 8390  df-rdg 8429

This theorem is referenced by:  precsex  28177