Theorem leftval

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

	Ref	Expression
Assertion	leftval	⊢ ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 }

Proof

Step	Hyp	Ref	Expression
1		2fveq3	⊢ ( 𝑦 = 𝐴 → ( O ‘ ( bday ‘ 𝑦 ) ) = ( O ‘ ( bday ‘ 𝐴 ) ) )
2		breq2	⊢ ( 𝑦 = 𝐴 → ( 𝑥 <s 𝑦 ↔ 𝑥 <s 𝐴 ) )
3	1 2	rabeqbidv	⊢ ( 𝑦 = 𝐴 → { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ∣ 𝑥 <s 𝑦 } = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } )
4		df-left	⊢ L = ( 𝑦 ∈ No ↦ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝑦 ) ) ∣ 𝑥 <s 𝑦 } )
5		fvex	⊢ ( O ‘ ( bday ‘ 𝐴 ) ) ∈ V
6	5	rabex	⊢ { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } ∈ V
7	3 4 6	fvmpt	⊢ ( 𝐴 ∈ No → ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } )
8	4	fvmptndm	⊢ ( ¬ 𝐴 ∈ No → ( L ‘ 𝐴 ) = ∅ )
9		bdaydm	⊢ dom bday = No
10	9	eleq2i	⊢ ( 𝐴 ∈ dom bday ↔ 𝐴 ∈ No )
11		ndmfv	⊢ ( ¬ 𝐴 ∈ dom bday → ( bday ‘ 𝐴 ) = ∅ )
12	10 11	sylnbir	⊢ ( ¬ 𝐴 ∈ No → ( bday ‘ 𝐴 ) = ∅ )
13	12	fveq2d	⊢ ( ¬ 𝐴 ∈ No → ( O ‘ ( bday ‘ 𝐴 ) ) = ( O ‘ ∅ ) )
14		old0	⊢ ( O ‘ ∅ ) = ∅
15	13 14	eqtrdi	⊢ ( ¬ 𝐴 ∈ No → ( O ‘ ( bday ‘ 𝐴 ) ) = ∅ )
16	15	rabeqdv	⊢ ( ¬ 𝐴 ∈ No → { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } = { 𝑥 ∈ ∅ ∣ 𝑥 <s 𝐴 } )
17		rab0	⊢ { 𝑥 ∈ ∅ ∣ 𝑥 <s 𝐴 } = ∅
18	16 17	eqtrdi	⊢ ( ¬ 𝐴 ∈ No → { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } = ∅ )
19	8 18	eqtr4d	⊢ ( ¬ 𝐴 ∈ No → ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 } )
20	7 19	pm2.61i	⊢ ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 }