Metamath Proof Explorer

Theorem leftval

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

Ref Expression
Assertion leftval ⊢ L ⁡ A = x ∈ Old ⁡ bday ⁡ A | x < s A

Proof

Step Hyp Ref Expression
1 2fveq3 ⊢ y = A → Old ⁡ bday ⁡ y = Old ⁡ bday ⁡ A
2 breq2 ⊢ y = A → x < s y ↔ x < s A
3 1 2 rabeqbidv ⊢ y = A → x ∈ Old ⁡ bday ⁡ y | x < s y = x ∈ Old ⁡ bday ⁡ A | x < s A
4 df-left ⊢ L = y ∈ No ⟼ x ∈ Old ⁡ bday ⁡ y | x < s y
5 fvex ⊢ Old ⁡ bday ⁡ A ∈ V
6 5 rabex ⊢ x ∈ Old ⁡ bday ⁡ A | x < s A ∈ V
7 3 4 6 fvmpt ⊢ A ∈ No → L ⁡ A = x ∈ Old ⁡ bday ⁡ A | x < s A
8 4 fvmptndm ⊢ ¬ A ∈ No → L ⁡ A = ∅
9 bdaydm ⊢ dom ⁡ bday = No
10 9 eleq2i ⊢ A ∈ dom ⁡ bday ↔ A ∈ No
11 ndmfv ⊢ ¬ A ∈ dom ⁡ bday → bday ⁡ A = ∅
12 10 11 sylnbir ⊢ ¬ A ∈ No → bday ⁡ A = ∅
13 12 fveq2d ⊢ ¬ A ∈ No → Old ⁡ bday ⁡ A = Old ⁡ ∅
14 old0 ⊢ Old ⁡ ∅ = ∅
15 13 14 eqtrdi ⊢ ¬ A ∈ No → Old ⁡ bday ⁡ A = ∅
16 15 rabeqdv ⊢ ¬ A ∈ No → x ∈ Old ⁡ bday ⁡ A | x < s A = x ∈ ∅ | x < s A
17 rab0 ⊢ x ∈ ∅ | x < s A = ∅
18 16 17 eqtrdi ⊢ ¬ A ∈ No → x ∈ Old ⁡ bday ⁡ A | x < s A = ∅
19 8 18 eqtr4d ⊢ ¬ A ∈ No → L ⁡ A = x ∈ Old ⁡ bday ⁡ A | x < s A
20 7 19 pm2.61i ⊢ L ⁡ A = x ∈ Old ⁡ bday ⁡ A | x < s A