Theorem precsexlemcbv

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

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

Proof

Step	Hyp	Ref	Expression
1		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 } , ∅ ⟩ )
2		fveq2	⊢ ( 𝑝 = 𝑞 → ( 1st ‘ 𝑝 ) = ( 1st ‘ 𝑞 ) )
3		fveq2	⊢ ( 𝑝 = 𝑞 → ( 2nd ‘ 𝑝 ) = ( 2nd ‘ 𝑞 ) )
4	3	csbeq1d	⊢ ( 𝑝 = 𝑞 → ⦋ ( 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	⊢ ( 𝑝 = 𝑞 → ⦋ ( 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	⊢ ( 𝑟 = 𝑠 → ( ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
7	6	rexbidv	⊢ ( 𝑟 = 𝑠 → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
8	7	abbidv	⊢ ( 𝑟 = 𝑠 → { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } = { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } )
9	8	uneq2d	⊢ ( 𝑟 = 𝑠 → ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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	⊢ ( 𝑟 = 𝑠 → ( 𝑙 ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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	⊢ ( 𝑟 = 𝑠 → 𝑟 = 𝑠 )
12		rexeq	⊢ ( 𝑟 = 𝑠 → ( ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
13	12	rexbidv	⊢ ( 𝑟 = 𝑠 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
14	13	abbidv	⊢ ( 𝑟 = 𝑠 → { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑟 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } = { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } )
15	14	uneq2d	⊢ ( 𝑟 = 𝑠 → ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( 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	⊢ ( 𝑟 = 𝑠 → ( 𝑟 ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( 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	⊢ ( 𝑟 = 𝑠 → ⟨ ( 𝑙 ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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	⊢ ( 𝑎 = 𝑏 → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
19	18	2rexbidv	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ) )
20		oveq1	⊢ ( 𝑥𝑅 = 𝑧𝑅 → ( 𝑥𝑅 -s 𝐴 ) = ( 𝑧𝑅 -s 𝐴 ) )
21	20	oveq1d	⊢ ( 𝑥𝑅 = 𝑧𝑅 → ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) = ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) )
22	21	oveq2d	⊢ ( 𝑥𝑅 = 𝑧𝑅 → ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) )
23		id	⊢ ( 𝑥𝑅 = 𝑧𝑅 → 𝑥𝑅 = 𝑧𝑅 )
24	22 23	oveq12d	⊢ ( 𝑥𝑅 = 𝑧𝑅 → ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑧𝑅 ) )
25	24	eqeq2d	⊢ ( 𝑥𝑅 = 𝑧𝑅 → ( 𝑏 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑧𝑅 ) ) )
26		oveq2	⊢ ( 𝑦𝐿 = 𝑤 → ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) = ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) )
27	26	oveq2d	⊢ ( 𝑦𝐿 = 𝑤 → ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) )
28	27	oveq1d	⊢ ( 𝑦𝐿 = 𝑤 → ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑧𝑅 ) = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝑅 ) )
29	28	eqeq2d	⊢ ( 𝑦𝐿 = 𝑤 → ( 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑧𝑅 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝑅 ) ) )
30	25 29	cbvrex2vw	⊢ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝑅 ) )
31	19 30	bitrdi	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝑅 ) ) )
32	31	cbvabv	⊢ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝑅 ) } = { 𝑏 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝑅 ) }
33		eqeq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
34	33	2rexbidv	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ) )
35		oveq1	⊢ ( 𝑥𝐿 = 𝑧𝐿 → ( 𝑥𝐿 -s 𝐴 ) = ( 𝑧𝐿 -s 𝐴 ) )
36	35	oveq1d	⊢ ( 𝑥𝐿 = 𝑧𝐿 → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) = ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) )
37	36	oveq2d	⊢ ( 𝑥𝐿 = 𝑧𝐿 → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) )
38		id	⊢ ( 𝑥𝐿 = 𝑧𝐿 → 𝑥𝐿 = 𝑧𝐿 )
39	37 38	oveq12d	⊢ ( 𝑥𝐿 = 𝑧𝐿 → ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑧𝐿 ) )
40	39	eqeq2d	⊢ ( 𝑥𝐿 = 𝑧𝐿 → ( 𝑏 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑧𝐿 ) ) )
41		oveq2	⊢ ( 𝑦𝑅 = 𝑡 → ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) = ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑡 ) )
42	41	oveq2d	⊢ ( 𝑦𝑅 = 𝑡 → ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑡 ) ) )
43	42	oveq1d	⊢ ( 𝑦𝑅 = 𝑡 → ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑧𝐿 ) = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝐿 ) )
44	43	eqeq2d	⊢ ( 𝑦𝑅 = 𝑡 → ( 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑧𝐿 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝐿 ) ) )
45	40 44	cbvrex2vw	⊢ ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑧𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑡 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝐿 ) )
46		breq2	⊢ ( 𝑥 = 𝑧 → ( 0s <s 𝑥 ↔ 0s <s 𝑧 ) )
47	46	cbvrabv	⊢ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } = { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 }
48	47	rexeqi	⊢ ( ∃ 𝑧𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑡 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝐿 ) ↔ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑡 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝐿 ) )
49	45 48	bitri	⊢ ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑡 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝐿 ) )
50	34 49	bitrdi	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑡 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝐿 ) ) )
51	50	cbvabv	⊢ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝐿 ) } = { 𝑏 ∣ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑡 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝐿 ) }
52	32 51	uneq12i	⊢ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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	⊢ ( 𝑙 ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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	⊢ ( 𝑎 = 𝑏 → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
55	54	2rexbidv	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ) )
56	35	oveq1d	⊢ ( 𝑥𝐿 = 𝑧𝐿 → ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) = ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) )
57	56	oveq2d	⊢ ( 𝑥𝐿 = 𝑧𝐿 → ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) )
58	57 38	oveq12d	⊢ ( 𝑥𝐿 = 𝑧𝐿 → ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑧𝐿 ) )
59	58	eqeq2d	⊢ ( 𝑥𝐿 = 𝑧𝐿 → ( 𝑏 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑧𝐿 ) ) )
60		oveq2	⊢ ( 𝑦𝐿 = 𝑤 → ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) = ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) )
61	60	oveq2d	⊢ ( 𝑦𝐿 = 𝑤 → ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) = ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) )
62	61	oveq1d	⊢ ( 𝑦𝐿 = 𝑤 → ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑧𝐿 ) = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) )
63	62	eqeq2d	⊢ ( 𝑦𝐿 = 𝑤 → ( 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑧𝐿 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) ) )
64	59 63	cbvrex2vw	⊢ ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑧𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) )
65	47	rexeqi	⊢ ( ∃ 𝑧𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) ↔ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) )
66	64 65	bitri	⊢ ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) )
67	55 66	bitrdi	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) ↔ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) ) )
68	67	cbvabv	⊢ { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑥 } ∃ 𝑦𝐿 ∈ 𝑙 𝑎 = ( ( 1s +s ( ( 𝑥𝐿 -s 𝐴 ) ·s 𝑦𝐿 ) ) /su 𝑥𝐿 ) } = { 𝑏 ∣ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) }
69		eqeq1	⊢ ( 𝑎 = 𝑏 → ( 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
70	69	2rexbidv	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ) )
71	20	oveq1d	⊢ ( 𝑥𝑅 = 𝑧𝑅 → ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) = ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) )
72	71	oveq2d	⊢ ( 𝑥𝑅 = 𝑧𝑅 → ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) )
73	72 23	oveq12d	⊢ ( 𝑥𝑅 = 𝑧𝑅 → ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑧𝑅 ) )
74	73	eqeq2d	⊢ ( 𝑥𝑅 = 𝑧𝑅 → ( 𝑏 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑧𝑅 ) ) )
75		oveq2	⊢ ( 𝑦𝑅 = 𝑡 → ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) = ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑡 ) )
76	75	oveq2d	⊢ ( 𝑦𝑅 = 𝑡 → ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) = ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑡 ) ) )
77	76	oveq1d	⊢ ( 𝑦𝑅 = 𝑡 → ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑧𝑅 ) = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝑅 ) )
78	77	eqeq2d	⊢ ( 𝑦𝑅 = 𝑡 → ( 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑧𝑅 ) ↔ 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝑅 ) ) )
79	74 78	cbvrex2vw	⊢ ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑡 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝑅 ) )
80	70 79	bitrdi	⊢ ( 𝑎 = 𝑏 → ( ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑡 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝑅 ) ) )
81	80	cbvabv	⊢ { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑦𝑅 ∈ 𝑠 𝑎 = ( ( 1s +s ( ( 𝑥𝑅 -s 𝐴 ) ·s 𝑦𝑅 ) ) /su 𝑥𝑅 ) } = { 𝑏 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑡 ∈ 𝑠 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑡 ) ) /su 𝑧𝑅 ) }
82	68 81	uneq12i	⊢ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( 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	⊢ ( 𝑠 ∪ ( { 𝑎 ∣ ∃ 𝑥𝐿 ∈ { 𝑥 ∈ ( 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	⊢ ⟨ ( 𝑙 ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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	⊢ ( 𝑟 = 𝑠 → ⟨ ( 𝑙 ∪ ( { 𝑎 ∣ ∃ 𝑥𝑅 ∈ ( 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	⊢ ⦋ ( 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	⊢ ⦋ ( 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	⊢ ( 𝑙 = 𝑚 → 𝑙 = 𝑚 )
89		rexeq	⊢ ( 𝑙 = 𝑚 → ( ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝑅 ) ↔ ∃ 𝑤 ∈ 𝑚 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝑅 ) ) )
90	89	rexbidv	⊢ ( 𝑙 = 𝑚 → ( ∃ 𝑧𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝑅 ) ↔ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ 𝑚 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝑅 ) ) )
91	90	abbidv	⊢ ( 𝑙 = 𝑚 → { 𝑏 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝑅 ) } = { 𝑏 ∣ ∃ 𝑧𝑅 ∈ ( R ‘ 𝐴 ) ∃ 𝑤 ∈ 𝑚 𝑏 = ( ( 1s +s ( ( 𝑧𝑅 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝑅 ) } )
92	91	uneq1d	⊢ ( 𝑙 = 𝑚 → ( { 𝑏 ∣ ∃ 𝑧𝑅 ∈ ( 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	⊢ ( 𝑙 = 𝑚 → ( 𝑙 ∪ ( { 𝑏 ∣ ∃ 𝑧𝑅 ∈ ( 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	⊢ ( 𝑙 = 𝑚 → ( ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) ↔ ∃ 𝑤 ∈ 𝑚 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) ) )
95	94	rexbidv	⊢ ( 𝑙 = 𝑚 → ( ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) ↔ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑤 ∈ 𝑚 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) ) )
96	95	abbidv	⊢ ( 𝑙 = 𝑚 → { 𝑏 ∣ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑤 ∈ 𝑙 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) } = { 𝑏 ∣ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( L ‘ 𝐴 ) ∣ 0s <s 𝑧 } ∃ 𝑤 ∈ 𝑚 𝑏 = ( ( 1s +s ( ( 𝑧𝐿 -s 𝐴 ) ·s 𝑤 ) ) /su 𝑧𝐿 ) } )
97	96	uneq1d	⊢ ( 𝑙 = 𝑚 → ( { 𝑏 ∣ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( 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	⊢ ( 𝑙 = 𝑚 → ( 𝑠 ∪ ( { 𝑏 ∣ ∃ 𝑧𝐿 ∈ { 𝑧 ∈ ( 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	⊢ ( 𝑙 = 𝑚 → ⟨ ( 𝑙 ∪ ( { 𝑏 ∣ ∃ 𝑧𝑅 ∈ ( 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	⊢ ( 𝑙 = 𝑚 → ⦋ ( 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	⊢ ⦋ ( 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	⊢ ⦋ ( 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	⊢ ( 𝑝 = 𝑞 → ⦋ ( 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	⊢ ( 𝑝 ∈ 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	⊢ ( ( 𝑝 ∈ 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	⊢ 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	⊢ 𝐹 = 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 } , ∅ ⟩ )