Description: The functionality of the right options function. (Contributed by Scott Fenton, 6-Aug-2024)
Ref | Expression | ||
---|---|---|---|
Assertion | rightf | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | df-right | |
|
2 | bdayelon | |
|
3 | oldf | |
|
4 | 3 | ffvelrni | |
5 | 2 4 | mp1i | |
6 | 5 | elpwid | |
7 | 6 | sselda | |
8 | 7 | a1d | |
9 | 8 | ralrimiva | |
10 | fvex | |
|
11 | 10 | rabex | |
12 | 11 | elpw | |
13 | rabss | |
|
14 | 12 13 | bitri | |
15 | 9 14 | sylibr | |
16 | 1 15 | fmpti | |