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 = ( 𝑥 No ↦ { 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ∣ 𝑥 <s 𝑦 } )
2 bdayelon ( bday 𝑥 ) ∈ On
3 oldf O : On ⟶ 𝒫 No
4 3 ffvelrni ( ( bday 𝑥 ) ∈ On → ( O ‘ ( bday 𝑥 ) ) ∈ 𝒫 No )
5 2 4 mp1i ( 𝑥 No → ( O ‘ ( bday 𝑥 ) ) ∈ 𝒫 No )
6 5 elpwid ( 𝑥 No → ( O ‘ ( bday 𝑥 ) ) ⊆ No )
7 6 sselda ( ( 𝑥 No 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ) → 𝑦 No )
8 7 a1d ( ( 𝑥 No 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ) → ( 𝑥 <s 𝑦𝑦 No ) )
9 8 ralrimiva ( 𝑥 No → ∀ 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ( 𝑥 <s 𝑦𝑦 No ) )
10 fvex ( O ‘ ( bday 𝑥 ) ) ∈ V
11 10 rabex { 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ∈ V
12 11 elpw ( { 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ∈ 𝒫 No ↔ { 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ⊆ No )
13 rabss ( { 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ⊆ No ↔ ∀ 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ( 𝑥 <s 𝑦𝑦 No ) )
14 12 13 bitri ( { 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ∈ 𝒫 No ↔ ∀ 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ( 𝑥 <s 𝑦𝑦 No ) )
15 9 14 sylibr ( 𝑥 No → { 𝑦 ∈ ( O ‘ ( bday 𝑥 ) ) ∣ 𝑥 <s 𝑦 } ∈ 𝒫 No )
16 1 15 fmpti R : No ⟶ 𝒫 No