Metamath Proof Explorer

Theorem 0elold

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

Ref Expression
Hypotheses 0elold.1 ⊢ φ → A ∈ No
0elold.2 ⊢ φ → A ≠ 0 s
Assertion 0elold ⊢ φ → 0 s ∈ Old ⁡ bday ⁡ A

Proof

Step Hyp Ref Expression
1 0elold.1 ⊢ φ → A ∈ No
2 0elold.2 ⊢ φ → A ≠ 0 s
3 bday0 ⊢ bday ⁡ 0 s = ∅
4 2 neneqd ⊢ φ → ¬ A = 0 s
5 bday0b ⊢ A ∈ No → bday ⁡ A = ∅ ↔ A = 0 s
6 1 5 syl ⊢ φ → bday ⁡ A = ∅ ↔ A = 0 s
7 4 6 mtbird ⊢ φ → ¬ bday ⁡ A = ∅
8 bdayon ⊢ bday ⁡ A ∈ On
9 on0eqel ⊢ bday ⁡ A ∈ On → bday ⁡ A = ∅ ∨ ∅ ∈ bday ⁡ A
10 8 9 ax-mp ⊢ bday ⁡ A = ∅ ∨ ∅ ∈ bday ⁡ A
11 orel1 ⊢ ¬ bday ⁡ A = ∅ → bday ⁡ A = ∅ ∨ ∅ ∈ bday ⁡ A → ∅ ∈ bday ⁡ A
12 7 10 11 mpisyl ⊢ φ → ∅ ∈ bday ⁡ A
13 3 12 eqeltrid ⊢ φ → bday ⁡ 0 s ∈ bday ⁡ A
14 0no ⊢ 0 s ∈ No
15 oldbday ⊢ bday ⁡ A ∈ On ∧ 0 s ∈ No → 0 s ∈ Old ⁡ bday ⁡ A ↔ bday ⁡ 0 s ∈ bday ⁡ A
16 8 14 15 mp2an ⊢ 0 s ∈ Old ⁡ bday ⁡ A ↔ bday ⁡ 0 s ∈ bday ⁡ A
17 13 16 sylibr ⊢ φ → 0 s ∈ Old ⁡ bday ⁡ A