Metamath Proof Explorer


Theorem leftval

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

Ref Expression
Assertion leftval ( 𝐴 No → ( 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 𝐴 } )