Theorem leftval

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

	Ref	Expression
Assertion	leftval	|- ( A e. No -> ( _L ` A ) = { x e. ( _Old ` ( bday ` A ) ) | x

Proof

Step	Hyp	Ref	Expression
1		2fveq3	|- ( y = A -> ( _Old ` ( bday ` y ) ) = ( _Old ` ( bday ` A ) ) )
2		breq2	|- ( y = A -> ( x x
3	1 2	rabeqbidv	|- ( y = A -> { x e. ( _Old ` ( bday ` y ) ) | x
4		df-left	|- _L = ( y e. No |-> { x e. ( _Old ` ( bday ` y ) ) | x
5		fvex	|- ( _Old ` ( bday ` A ) ) e. _V
6	5	rabex	|- { x e. ( _Old ` ( bday ` A ) ) | x
7	3 4 6	fvmpt	|- ( A e. No -> ( _L ` A ) = { x e. ( _Old ` ( bday ` A ) ) | x