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. ( _New ` A ) <-> ( bday ` X ) = A ) )

Proof

Step	Hyp	Ref	Expression
1		madebday	|- ( ( A e. On /\ X e. No ) -> ( X e. ( _Made ` 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. ( _Made ` A ) /\ -. X e. ( _Old ` A ) ) <-> ( ( bday ` X ) C_ A /\ -. ( bday ` X ) e. A ) ) )
5		newval	|- ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) )
6	5	a1i	|- ( A e. On -> ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) )
7	6	eleq2d	|- ( A e. On -> ( X e. ( _New ` A ) <-> X e. ( ( _Made ` A ) \ ( _Old ` A ) ) ) )
8		eldif	|- ( X e. ( ( _Made ` A ) \ ( _Old ` A ) ) <-> ( X e. ( _Made ` A ) /\ -. X e. ( _Old ` A ) ) )
9	7 8	bitrdi	|- ( A e. On -> ( X e. ( _New ` A ) <-> ( X e. ( _Made ` A ) /\ -. X e. ( _Old ` A ) ) ) )
10	9	adantr	|- ( ( A e. On /\ X e. No ) -> ( X e. ( _New ` A ) <-> ( X e. ( _Made ` 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. ( _New ` A ) <-> ( bday ` X ) = A ) )