Theorem leftval

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

	Ref	Expression
Assertion	leftval	|- ( _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
8	4	fvmptndm	|- ( -. A e. No -> ( _L ` 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 ) ) | x
17		rab0	|- { x e. (/) | x
18	16 17	eqtrdi	|- ( -. A e. No -> { x e. ( _Old ` ( bday ` A ) ) | x
19	8 18	eqtr4d	|- ( -. A e. No -> ( _L ` A ) = { x e. ( _Old ` ( bday ` A ) ) | x
20	7 19	pm2.61i	|- ( _L ` A ) = { x e. ( _Old ` ( bday ` A ) ) | x