Metamath Proof Explorer

Theorem leftf

Description: The functionality of the left options function. (Contributed by Scott Fenton, 6-Aug-2024)

Ref Expression
Assertion leftf ⊢ L : No ⟶ 𝒫 No

Proof

Step Hyp Ref Expression
1 df-left ⊢ L = x ∈ No ⟼ y ∈ Old ⁡ bday ⁡ x | y < s x
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 → y < s x → y ∈ No
9 8 ralrimiva ⊢ x ∈ No → ∀ y ∈ Old ⁡ bday ⁡ x y < s x → y ∈ No
10 fvex ⊢ Old ⁡ bday ⁡ x ∈ V
11 10 rabex ⊢ y ∈ Old ⁡ bday ⁡ x | y < s x ∈ V
12 11 elpw ⊢ y ∈ Old ⁡ bday ⁡ x | y < s x ∈ 𝒫 No ↔ y ∈ Old ⁡ bday ⁡ x | y < s x ⊆ No
13 rabss ⊢ y ∈ Old ⁡ bday ⁡ x | y < s x ⊆ No ↔ ∀ y ∈ Old ⁡ bday ⁡ x y < s x → y ∈ No
14 12 13 bitri ⊢ y ∈ Old ⁡ bday ⁡ x | y < s x ∈ 𝒫 No ↔ ∀ y ∈ Old ⁡ bday ⁡ x y < s x → y ∈ No
15 9 14 sylibr ⊢ x ∈ No → y ∈ Old ⁡ bday ⁡ x | y < s x ∈ 𝒫 No
16 1 15 fmpti ⊢ L : No ⟶ 𝒫 No