Metamath Proof Explorer

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 
|- ( ph -> A e. No )
0elold.2 
|- ( ph -> A =/= 0s )
Assertion 0elold 
|- ( ph -> 0s e. ( _Old ` ( bday ` A ) ) )

Proof

Step Hyp Ref Expression
1 0elold.1 
 |-  ( ph -> A e. No )
2 0elold.2 
 |-  ( ph -> A =/= 0s )
3 bday0s 
 |-  ( bday ` 0s ) = (/)
4 2 neneqd 
 |-  ( ph -> -. A = 0s )
5 bday0b 
 |-  ( A e. No -> ( ( bday ` A ) = (/) <-> A = 0s ) )
6 1 5 syl 
 |-  ( ph -> ( ( bday ` A ) = (/) <-> A = 0s ) )
7 4 6 mtbird 
 |-  ( ph -> -. ( bday ` A ) = (/) )
8 bdayelon 
 |-  ( bday ` A ) e. On
9 on0eqel 
 |-  ( ( bday ` A ) e. On -> ( ( bday ` A ) = (/) \/ (/) e. ( bday ` A ) ) )
10 8 9 ax-mp 
 |-  ( ( bday ` A ) = (/) \/ (/) e. ( bday ` A ) )
11 orel1 
 |-  ( -. ( bday ` A ) = (/) -> ( ( ( bday ` A ) = (/) \/ (/) e. ( bday ` A ) ) -> (/) e. ( bday ` A ) ) )
12 7 10 11 mpisyl 
 |-  ( ph -> (/) e. ( bday ` A ) )
13 3 12 eqeltrid 
 |-  ( ph -> ( bday ` 0s ) e. ( bday ` A ) )
14 0sno 
 |-  0s e. No
15 oldbday 
 |-  ( ( ( bday ` A ) e. On /\ 0s e. No ) -> ( 0s e. ( _Old ` ( bday ` A ) ) <-> ( bday ` 0s ) e. ( bday ` A ) ) )
16 8 14 15 mp2an 
 |-  ( 0s e. ( _Old ` ( bday ` A ) ) <-> ( bday ` 0s ) e. ( bday ` A ) )
17 13 16 sylibr 
 |-  ( ph -> 0s e. ( _Old ` ( bday ` A ) ) )