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 e. On /\ X e. No ) -> ( X e. ( _N ` A ) <-> ( bday ` X ) = A ) )

Proof

Step Hyp Ref Expression
1 madebday
 |-  ( ( A e. On /\ X e. No ) -> ( X e. ( _M ` A ) <-> ( bday ` X ) C_ A ) )
2 oldbday
 |-  ( ( A e. On /\ X e. No ) -> ( X e. ( _Old ` A ) <-> ( bday ` X ) e. A ) )
3 2 notbid
 |-  ( ( A e. On /\ X e. No ) -> ( -. X e. ( _Old ` A ) <-> -. ( bday ` X ) e. A ) )
4 1 3 anbi12d
 |-  ( ( A e. On /\ X e. No ) -> ( ( X e. ( _M ` A ) /\ -. X e. ( _Old ` A ) ) <-> ( ( bday ` X ) C_ A /\ -. ( bday ` X ) e. A ) ) )
5 newval
 |-  ( _N ` A ) = ( ( _M ` A ) \ ( _Old ` A ) )
6 5 a1i
 |-  ( A e. On -> ( _N ` A ) = ( ( _M ` A ) \ ( _Old ` A ) ) )
7 6 eleq2d
 |-  ( A e. On -> ( X e. ( _N ` A ) <-> X e. ( ( _M ` A ) \ ( _Old ` A ) ) ) )
8 eldif
 |-  ( X e. ( ( _M ` A ) \ ( _Old ` A ) ) <-> ( X e. ( _M ` A ) /\ -. X e. ( _Old ` A ) ) )
9 7 8 bitrdi
 |-  ( A e. On -> ( X e. ( _N ` A ) <-> ( X e. ( _M ` A ) /\ -. X e. ( _Old ` A ) ) ) )
10 9 adantr
 |-  ( ( A e. On /\ X e. No ) -> ( X e. ( _N ` A ) <-> ( X e. ( _M ` A ) /\ -. X e. ( _Old ` A ) ) ) )
11 bdayelon
 |-  ( bday ` X ) e. On
12 11 onordi
 |-  Ord ( bday ` X )
13 eloni
 |-  ( A e. On -> Ord A )
14 ordtri4
 |-  ( ( Ord ( bday ` X ) /\ Ord A ) -> ( ( bday ` X ) = A <-> ( ( bday ` X ) C_ A /\ -. ( bday ` X ) e. A ) ) )
15 12 13 14 sylancr
 |-  ( A e. On -> ( ( bday ` X ) = A <-> ( ( bday ` X ) C_ A /\ -. ( bday ` X ) e. A ) ) )
16 15 adantr
 |-  ( ( A e. On /\ X e. No ) -> ( ( bday ` X ) = A <-> ( ( bday ` X ) C_ A /\ -. ( bday ` X ) e. A ) ) )
17 4 10 16 3bitr4d
 |-  ( ( A e. On /\ X e. No ) -> ( X e. ( _N ` A ) <-> ( bday ` X ) = A ) )