Theorem 0elleft

Description: Zero is in the left set of any positive number. (Contributed by Scott Fenton, 13-Mar-2025)

	Ref	Expression
Hypotheses	0elleft.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	0elleft.2	⊢ ( 𝜑 → 0s <s 𝐴 )
Assertion	0elleft	⊢ ( 𝜑 → 0s ∈ ( L ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		0elleft.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		0elleft.2	⊢ ( 𝜑 → 0s <s 𝐴 )
3	2	sgt0ne0d	⊢ ( 𝜑 → 𝐴 ≠ 0s )
4	1 3	0elold	⊢ ( 𝜑 → 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )
5		breq1	⊢ ( 𝑥 = 0s → ( 𝑥 <s 𝐴 ↔ 0s <s 𝐴 ) )
6		leftval	⊢ ( L ‘ 𝐴 ) = { 𝑥 ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∣ 𝑥 <s 𝐴 }
7	5 6	elrab2	⊢ ( 0s ∈ ( L ‘ 𝐴 ) ↔ ( 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ∧ 0s <s 𝐴 ) )
8	4 2 7	sylanbrc	⊢ ( 𝜑 → 0s ∈ ( L ‘ 𝐴 ) )