Metamath Proof Explorer

Theorem leftf

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

Ref Expression
Assertion leftf 
|- _L : No --> ~P No

Proof

Step Hyp Ref Expression
1 df-left 
 |-  _L = ( x e. No |-> { y e. ( _Old ` ( bday ` x ) ) | y
2 bdayelon 
 |-  ( bday ` x ) e. On
3 oldf 
 |-  _Old : On --> ~P No
4 3 ffvelrni 
 |-  ( ( bday ` x ) e. On -> ( _Old ` ( bday ` x ) ) e. ~P No )
5 2 4 mp1i 
 |-  ( x e. No -> ( _Old ` ( bday ` x ) ) e. ~P No )
6 5 elpwid 
 |-  ( x e. No -> ( _Old ` ( bday ` x ) ) C_ No )
7 6 sselda 
 |-  ( ( x e. No /\ y e. ( _Old ` ( bday ` x ) ) ) -> y e. No )
8 7 a1d 
 |-  ( ( x e. No /\ y e. ( _Old ` ( bday ` x ) ) ) -> ( y  y e. No ) )
9 8 ralrimiva 
 |-  ( x e. No -> A. y e. ( _Old ` ( bday ` x ) ) ( y  y e. No ) )
10 fvex 
 |-  ( _Old ` ( bday ` x ) ) e. _V
11 10 rabex 
 |-  { y e. ( _Old ` ( bday ` x ) ) | y
12 11 elpw 
 |-  ( { y e. ( _Old ` ( bday ` x ) ) | y  { y e. ( _Old ` ( bday ` x ) ) | y
13 rabss 
 |-  ( { y e. ( _Old ` ( bday ` x ) ) | y  A. y e. ( _Old ` ( bday ` x ) ) ( y  y e. No ) )
14 12 13 bitri 
 |-  ( { y e. ( _Old ` ( bday ` x ) ) | y  A. y e. ( _Old ` ( bday ` x ) ) ( y  y e. No ) )
15 9 14 sylibr 
 |-  ( x e. No -> { y e. ( _Old ` ( bday ` x ) ) | y
16 1 15 fmpti 
 |-  _L : No --> ~P No