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	$$⊢\phi \to A\in \mathrm{No}$$
	0elold.2	No typesetting found for |- ( ph -> A =/= 0s ) with typecode |-
Assertion	0elold	Could not format assertion : No typesetting found for |- ( ph -> 0s e. ( _Old ` ( bday ` A ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0elold.1	$$⊢\phi \to A\in \mathrm{No}$$
2		0elold.2	Could not format ( ph -> A =/= 0s ) : No typesetting found for |- ( ph -> A =/= 0s ) with typecode |-
3		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
4	2	neneqd	Could not format ( ph -> -. A = 0s ) : No typesetting found for |- ( ph -> -. A = 0s ) with typecode |-
5		bday0b	Could not format ( A e. No -> ( ( bday ` A ) = (/) <-> A = 0s ) ) : No typesetting found for |- ( A e. No -> ( ( bday ` A ) = (/) <-> A = 0s ) ) with typecode |-
6	1 5	syl	Could not format ( ph -> ( ( bday ` A ) = (/) <-> A = 0s ) ) : No typesetting found for |- ( ph -> ( ( bday ` A ) = (/) <-> A = 0s ) ) with typecode |-
7	4 6	mtbird	$$⊢\phi \to \neg \mathrm{bday}\left(A\right)=\varnothing$$
8		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
9		on0eqel	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}\to \left(\mathrm{bday}\left(A\right)=\varnothing \vee \varnothing \in \mathrm{bday}\left(A\right)\right)$$
10	8 9	ax-mp	$$⊢\left(\mathrm{bday}\left(A\right)=\varnothing \vee \varnothing \in \mathrm{bday}\left(A\right)\right)$$
11		orel1	$$⊢\neg \mathrm{bday}\left(A\right)=\varnothing \to \left(\left(\mathrm{bday}\left(A\right)=\varnothing \vee \varnothing \in \mathrm{bday}\left(A\right)\right)\to \varnothing \in \mathrm{bday}\left(A\right)\right)$$
12	7 10 11	mpisyl	$$⊢\phi \to \varnothing \in \mathrm{bday}\left(A\right)$$
13	3 12	eqeltrid	Could not format ( ph -> ( bday ` 0s ) e. ( bday ` A ) ) : No typesetting found for |- ( ph -> ( bday ` 0s ) e. ( bday ` A ) ) with typecode |-
14		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
15		oldbday	Could not format ( ( ( bday ` A ) e. On /\ 0s e. No ) -> ( 0s e. ( _Old ` ( bday ` A ) ) <-> ( bday ` 0s ) e. ( bday ` A ) ) ) : No typesetting found for |- ( ( ( bday ` A ) e. On /\ 0s e. No ) -> ( 0s e. ( _Old ` ( bday ` A ) ) <-> ( bday ` 0s ) e. ( bday ` A ) ) ) with typecode |-
16	8 14 15	mp2an	Could not format ( 0s e. ( _Old ` ( bday ` A ) ) <-> ( bday ` 0s ) e. ( bday ` A ) ) : No typesetting found for |- ( 0s e. ( _Old ` ( bday ` A ) ) <-> ( bday ` 0s ) e. ( bday ` A ) ) with typecode |-
17	13 16	sylibr	Could not format ( ph -> 0s e. ( _Old ` ( bday ` A ) ) ) : No typesetting found for |- ( ph -> 0s e. ( _Old ` ( bday ` A ) ) ) with typecode |-