Metamath Proof Explorer

Theorem newbday

Description: A surreal is an element of a new set iff its birthday is equal to that ordinal. Remark in Conway p. 29. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion newbday ⊢ A ∈ On ∧ X ∈ No → X ∈ N ⁡ A ↔ bday ⁡ X = A

Proof

Step Hyp Ref Expression
1 madebday ⊢ A ∈ On ∧ X ∈ No → X ∈ M ⁡ A ↔ bday ⁡ X ⊆ A
2 oldbday ⊢ A ∈ On ∧ X ∈ No → X ∈ Old ⁡ A ↔ bday ⁡ X ∈ A
3 2 notbid ⊢ A ∈ On ∧ X ∈ No → ¬ X ∈ Old ⁡ A ↔ ¬ bday ⁡ X ∈ A
4 1 3 anbi12d ⊢ A ∈ On ∧ X ∈ No → X ∈ M ⁡ A ∧ ¬ X ∈ Old ⁡ A ↔ bday ⁡ X ⊆ A ∧ ¬ bday ⁡ X ∈ A
5 newval ⊢ N ⁡ A = M ⁡ A ∖ Old ⁡ A
6 5 a1i ⊢ A ∈ On → N ⁡ A = M ⁡ A ∖ Old ⁡ A
7 6 eleq2d ⊢ A ∈ On → X ∈ N ⁡ A ↔ X ∈ M ⁡ A ∖ Old ⁡ A
8 eldif ⊢ X ∈ M ⁡ A ∖ Old ⁡ A ↔ X ∈ M ⁡ A ∧ ¬ X ∈ Old ⁡ A
9 7 8 bitrdi ⊢ A ∈ On → X ∈ N ⁡ A ↔ X ∈ M ⁡ A ∧ ¬ X ∈ Old ⁡ A
10 9 adantr ⊢ A ∈ On ∧ X ∈ No → X ∈ N ⁡ A ↔ X ∈ M ⁡ A ∧ ¬ X ∈ Old ⁡ A
11 bdayon ⊢ bday ⁡ X ∈ On
12 11 onordi ⊢ Ord ⁡ bday ⁡ X
13 eloni ⊢ A ∈ On → Ord ⁡ A
14 ordtri4 ⊢ Ord ⁡ bday ⁡ X ∧ Ord ⁡ A → bday ⁡ X = A ↔ bday ⁡ X ⊆ A ∧ ¬ bday ⁡ X ∈ A
15 12 13 14 sylancr ⊢ A ∈ On → bday ⁡ X = A ↔ bday ⁡ X ⊆ A ∧ ¬ bday ⁡ X ∈ A
16 15 adantr ⊢ A ∈ On ∧ X ∈ No → bday ⁡ X = A ↔ bday ⁡ X ⊆ A ∧ ¬ bday ⁡ X ∈ A
17 4 10 16 3bitr4d ⊢ A ∈ On ∧ X ∈ No → X ∈ N ⁡ A ↔ bday ⁡ X = A