Theorem rightval

Description: The value of the right options function. (Contributed by Scott Fenton, 6-Aug-2024)

	Ref	Expression
Assertion	rightval	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } )

Proof

Step	Hyp	Ref	Expression
1		2fveq3	⊢ ( 𝑦 = 𝐴 → ( O ‘ ( bday ‘ 𝑦 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) )
2		breq1	⊢ ( 𝑦 = 𝐴 → ( 𝑦 <s 𝑥 ↔ 𝐴 <s 𝑥 ) )
3	1 2	rabeqbidv	⊢ ( 𝑦 = 𝐴 → { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ∣ 𝑦 <s 𝑥 } = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } )
4		df-right	⊢ R = ( 𝑦 ∈ No ↦ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ∣ 𝑦 <s 𝑥 } )
5		fvex	⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ∈ V
6	5	rabex	⊢ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } ∈ V
7	3 4 6	fvmpt	⊢ ( 𝐴 ∈ No → ( R ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝐴 <s 𝑥 } )