Theorem rightval

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

	Ref	Expression
Assertion	rightval	|- ( _R ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A

Proof

Step	Hyp	Ref	Expression
1		2fveq3	|- ( y = A -> ( _Old ` ( bday ` y ) ) = ( _Old ` ( bday ` A ) ) )
2		breq1	|- ( y = A -> ( y A
3	1 2	rabeqbidv	|- ( y = A -> { x e. ( _Old ` ( bday ` y ) ) | y
4		df-right	|- _R = ( y e. No |-> { x e. ( _Old ` ( bday ` y ) ) | y
5		fvex	|- ( _Old ` ( bday ` A ) ) e. _V
6	5	rabex	|- { x e. ( _Old ` ( bday ` A ) ) | A
7	3 4 6	fvmpt	|- ( A e. No -> ( _R ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A
8	4	fvmptndm	|- ( -. A e. No -> ( _R ` A ) = (/) )
9		bdaydm	|- dom bday = No
10	9	eleq2i	|- ( A e. dom bday <-> A e. No )
11		ndmfv	|- ( -. A e. dom bday -> ( bday ` A ) = (/) )
12	10 11	sylnbir	|- ( -. A e. No -> ( bday ` A ) = (/) )
13	12	fveq2d	|- ( -. A e. No -> ( _Old ` ( bday ` A ) ) = ( _Old ` (/) ) )
14		old0	|- ( _Old ` (/) ) = (/)
15	13 14	eqtrdi	|- ( -. A e. No -> ( _Old ` ( bday ` A ) ) = (/) )
16	15	rabeqdv	|- ( -. A e. No -> { x e. ( _Old ` ( bday ` A ) ) | A
17		rab0	|- { x e. (/) | A
18	16 17	eqtrdi	|- ( -. A e. No -> { x e. ( _Old ` ( bday ` A ) ) | A
19	8 18	eqtr4d	|- ( -. A e. No -> ( _R ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A
20	7 19	pm2.61i	|- ( _R ` A ) = { x e. ( _Old ` ( bday ` A ) ) | A