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 bdayon ⊢ bday ⁡ x ∈ On
3 oldf ⊢ Old : On ⟶ 𝒫 No
4 3 ffvelcdmi ⊢ 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