Theorem 0elold

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

	Ref	Expression
Hypotheses	0elold.1	⊢ ( 𝜑 → 𝐴 ∈ No )
	0elold.2	⊢ ( 𝜑 → 𝐴 ≠ 0s )
Assertion	0elold	⊢ ( 𝜑 → 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		0elold.1	⊢ ( 𝜑 → 𝐴 ∈ No )
2		0elold.2	⊢ ( 𝜑 → 𝐴 ≠ 0s )
3		bday0s	⊢ ( bday ‘ 0s ) = ∅
4	2	neneqd	⊢ ( 𝜑 → ¬ 𝐴 = 0s )
5		bday0b	⊢ ( 𝐴 ∈ No → ( ( bday ‘ 𝐴 ) = ∅ ↔ 𝐴 = 0s ) )
6	1 5	syl	⊢ ( 𝜑 → ( ( bday ‘ 𝐴 ) = ∅ ↔ 𝐴 = 0s ) )
7	4 6	mtbird	⊢ ( 𝜑 → ¬ ( bday ‘ 𝐴 ) = ∅ )
8		bdayelon	⊢ ( bday ‘ 𝐴 ) ∈ On
9		on0eqel	⊢ ( ( bday ‘ 𝐴 ) ∈ On → ( ( bday ‘ 𝐴 ) = ∅ ∨ ∅ ∈ ( bday ‘ 𝐴 ) ) )
10	8 9	ax-mp	⊢ ( ( bday ‘ 𝐴 ) = ∅ ∨ ∅ ∈ ( bday ‘ 𝐴 ) )
11		orel1	⊢ ( ¬ ( bday ‘ 𝐴 ) = ∅ → ( ( ( bday ‘ 𝐴 ) = ∅ ∨ ∅ ∈ ( bday ‘ 𝐴 ) ) → ∅ ∈ ( bday ‘ 𝐴 ) ) )
12	7 10 11	mpisyl	⊢ ( 𝜑 → ∅ ∈ ( bday ‘ 𝐴 ) )
13	3 12	eqeltrid	⊢ ( 𝜑 → ( bday ‘ 0s ) ∈ ( bday ‘ 𝐴 ) )
14		0sno	⊢ 0s ∈ No
15		oldbday	⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ 0s ∈ No ) → ( 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 0s ) ∈ ( bday ‘ 𝐴 ) ) )
16	8 14 15	mp2an	⊢ ( 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) ↔ ( bday ‘ 0s ) ∈ ( bday ‘ 𝐴 ) )
17	13 16	sylibr	⊢ ( 𝜑 → 0s ∈ ( O ‘ ( bday ‘ 𝐴 ) ) )