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 𝒫 No

Proof

Step Hyp Ref Expression
1 df-right R = x No y Old bday x | x < s y
2 bdayelon bday x On
3 oldf Old : On 𝒫 No
4 3 ffvelrni 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 x < s y y No
9 8 ralrimiva x No y Old bday x x < s y y No
10 fvex Old bday x V
11 10 rabex y Old bday x | x < s y V
12 11 elpw y Old bday x | x < s y 𝒫 No y Old bday x | x < s y No
13 rabss y Old bday x | x < s y No y Old bday x x < s y y No
14 12 13 bitri y Old bday x | x < s y 𝒫 No y Old bday x x < s y y No
15 9 14 sylibr x No y Old bday x | x < s y 𝒫 No
16 1 15 fmpti R : No 𝒫 No