Metamath Proof Explorer

Theorem leftf

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

Ref Expression
Assertion leftf Could not format assertion : No typesetting found for |- _Left : No --> ~P No with typecode |-

Proof

Step Hyp Ref Expression
1 df-left Could not format _Left = ( x e. No |-> { y e. ( _Old ` ( bday ` x ) ) | y { y e. ( _Old ` ( bday ` x ) ) | y
2 bdayelon ⊢bday⁡x∈On
3 oldf ⊢Old:On⟶𝒫No
4 3 ffvelcdmi ⊢bday⁡x∈On→Old⁡bday⁡x∈𝒫No
5 2 4 mp1i ⊢x∈No→Old⁡bday⁡x∈𝒫No
6 5 elpwid ⊢x∈No→Old⁡bday⁡x⊆No
7 6 sselda ⊢x∈No∧y∈Old⁡bday⁡x→y∈No
8 7 a1d ⊢x∈No∧y∈Old⁡bday⁡x→y<sx→y∈No
9 8 ralrimiva ⊢x∈No→∀y∈Old⁡bday⁡xy<sx→y∈No
10 fvex ⊢Old⁡bday⁡x∈V
11 10 rabex ⊢y∈Old⁡bday⁡x|y<sx∈V
12 11 elpw ⊢y∈Old⁡bday⁡x|y<sx∈𝒫No↔y∈Old⁡bday⁡x|y<sx⊆No
13 rabss ⊢y∈Old⁡bday⁡x|y<sx⊆No↔∀y∈Old⁡bday⁡xy<sx→y∈No
14 12 13 bitri ⊢y∈Old⁡bday⁡x|y<sx∈𝒫No↔∀y∈Old⁡bday⁡xy<sx→y∈No
15 9 14 sylibr ⊢x∈No→y∈Old⁡bday⁡x|y<sx∈𝒫No
16 1 15 fmpti Could not format _Left : No --> ~P No : No typesetting found for |- _Left : No --> ~P No with typecode |-