Metamath Proof Explorer

Theorem rightf

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

Ref Expression
Assertion rightf 
|- _R : No --> ~P No

Proof

Step Hyp Ref Expression
1 df-right 
 |-  _R = ( x e. No |-> { y e. ( _Old ` ( bday ` x ) ) | x
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 ) ) ) -> ( x  y e. No ) )
9 8 ralrimiva 
 |-  ( x e. No -> A. y e. ( _Old ` ( bday ` x ) ) ( x  y e. No ) )
10 fvex 
 |-  ( _Old ` ( bday ` x ) ) e. _V
11 10 rabex 
 |-  { y e. ( _Old ` ( bday ` x ) ) | x
12 11 elpw 
 |-  ( { y e. ( _Old ` ( bday ` x ) ) | x  { y e. ( _Old ` ( bday ` x ) ) | x
13 rabss 
 |-  ( { y e. ( _Old ` ( bday ` x ) ) | x  A. y e. ( _Old ` ( bday ` x ) ) ( x  y e. No ) )
14 12 13 bitri 
 |-  ( { y e. ( _Old ` ( bday ` x ) ) | x  A. y e. ( _Old ` ( bday ` x ) ) ( x  y e. No ) )
15 9 14 sylibr 
 |-  ( x e. No -> { y e. ( _Old ` ( bday ` x ) ) | x
16 1 15 fmpti 
 |-  _R : No --> ~P No