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=xNoyOldbdayx|x<sy
2 bdayelon bdayxOn
3 oldf Old:On𝒫No
4 3 ffvelrni bdayxOnOldbdayx𝒫No
5 2 4 mp1i xNoOldbdayx𝒫No
6 5 elpwid xNoOldbdayxNo
7 6 sselda xNoyOldbdayxyNo
8 7 a1d xNoyOldbdayxx<syyNo
9 8 ralrimiva xNoyOldbdayxx<syyNo
10 fvex OldbdayxV
11 10 rabex yOldbdayx|x<syV
12 11 elpw yOldbdayx|x<sy𝒫NoyOldbdayx|x<syNo
13 rabss yOldbdayx|x<syNoyOldbdayxx<syyNo
14 12 13 bitri yOldbdayx|x<sy𝒫NoyOldbdayxx<syyNo
15 9 14 sylibr xNoyOldbdayx|x<sy𝒫No
16 1 15 fmpti R:No𝒫No