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 = ( 𝑥 ∈ 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	⊢ L : No ⟶ 𝒫 No