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 ⊢ A ∈ On → N ⁡ A = M ⁡ A ∖ Old ⁡ A
6 5 eleq2d ⊢ A ∈ On → X ∈ N ⁡ A ↔ X ∈ M ⁡ A ∖ Old ⁡ A
7 eldif ⊢ X ∈ M ⁡ A ∖ Old ⁡ A ↔ X ∈ M ⁡ A ∧ ¬ X ∈ Old ⁡ A
8 6 7 bitrdi ⊢ A ∈ On → X ∈ N ⁡ A ↔ X ∈ M ⁡ A ∧ ¬ X ∈ Old ⁡ A
9 8 adantr ⊢ A ∈ On ∧ X ∈ No → X ∈ N ⁡ A ↔ X ∈ M ⁡ A ∧ ¬ X ∈ Old ⁡ A
10 bdayelon ⊢ bday ⁡ X ∈ On
11 10 onordi ⊢ Ord ⁡ bday ⁡ X
12 eloni ⊢ A ∈ On → Ord ⁡ A
13 ordtri4 ⊢ Ord ⁡ bday ⁡ X ∧ Ord ⁡ A → bday ⁡ X = A ↔ bday ⁡ X ⊆ A ∧ ¬ bday ⁡ X ∈ A
14 11 12 13 sylancr ⊢ A ∈ On → bday ⁡ X = A ↔ bday ⁡ X ⊆ A ∧ ¬ bday ⁡ X ∈ A
15 14 adantr ⊢ A ∈ On ∧ X ∈ No → bday ⁡ X = A ↔ bday ⁡ X ⊆ A ∧ ¬ bday ⁡ X ∈ A
16 4 9 15 3bitr4d ⊢ A ∈ On ∧ X ∈ No → X ∈ N ⁡ A ↔ bday ⁡ X = A