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	Could not format assertion : No typesetting found for |- ( ( A e. On /\ X e. No ) -> ( X e. ( _New ` A ) <-> ( bday ` X ) = A ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		madebday	Could not format ( ( A e. On /\ X e. No ) -> ( X e. ( _Made ` A ) <-> ( bday ` X ) C_ A ) ) : No typesetting found for |- ( ( A e. On /\ X e. No ) -> ( X e. ( _Made ` A ) <-> ( bday ` X ) C_ A ) ) with typecode |-
2		oldbday	$$⊢\left(A\in \mathrm{On}\wedge X\in \mathrm{No}\right)\to \left(X\in \mathrm{Old}\left(A\right)\leftrightarrow \mathrm{bday}\left(X\right)\in A\right)$$
3	2	notbid	$$⊢\left(A\in \mathrm{On}\wedge X\in \mathrm{No}\right)\to \left(\neg X\in \mathrm{Old}\left(A\right)\leftrightarrow \neg \mathrm{bday}\left(X\right)\in A\right)$$
4	1 3	anbi12d	Could not format ( ( A e. On /\ X e. No ) -> ( ( X e. ( _Made ` A ) /\ -. X e. ( _Old ` A ) ) <-> ( ( bday ` X ) C_ A /\ -. ( bday ` X ) e. A ) ) ) : No typesetting found for |- ( ( A e. On /\ X e. No ) -> ( ( X e. ( _Made ` A ) /\ -. X e. ( _Old ` A ) ) <-> ( ( bday ` X ) C_ A /\ -. ( bday ` X ) e. A ) ) ) with typecode |-
5		newval	Could not format ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) : No typesetting found for |- ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) with typecode |-
6	5	a1i	Could not format ( A e. On -> ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) ) : No typesetting found for |- ( A e. On -> ( _New ` A ) = ( ( _Made ` A ) \ ( _Old ` A ) ) ) with typecode |-
7	6	eleq2d	Could not format ( A e. On -> ( X e. ( _New ` A ) <-> X e. ( ( _Made ` A ) \ ( _Old ` A ) ) ) ) : No typesetting found for |- ( A e. On -> ( X e. ( _New ` A ) <-> X e. ( ( _Made ` A ) \ ( _Old ` A ) ) ) ) with typecode |-
8		eldif	Could not format ( X e. ( ( _Made ` A ) \ ( _Old ` A ) ) <-> ( X e. ( _Made ` A ) /\ -. X e. ( _Old ` A ) ) ) : No typesetting found for |- ( X e. ( ( _Made ` A ) \ ( _Old ` A ) ) <-> ( X e. ( _Made ` A ) /\ -. X e. ( _Old ` A ) ) ) with typecode |-
9	7 8	bitrdi	Could not format ( A e. On -> ( X e. ( _New ` A ) <-> ( X e. ( _Made ` A ) /\ -. X e. ( _Old ` A ) ) ) ) : No typesetting found for |- ( A e. On -> ( X e. ( _New ` A ) <-> ( X e. ( _Made ` A ) /\ -. X e. ( _Old ` A ) ) ) ) with typecode |-
10	9	adantr	Could not format ( ( A e. On /\ X e. No ) -> ( X e. ( _New ` A ) <-> ( X e. ( _Made ` A ) /\ -. X e. ( _Old ` A ) ) ) ) : No typesetting found for |- ( ( A e. On /\ X e. No ) -> ( X e. ( _New ` A ) <-> ( X e. ( _Made ` A ) /\ -. X e. ( _Old ` A ) ) ) ) with typecode |-
11		bdayelon	$$⊢\mathrm{bday}\left(X\right)\in \mathrm{On}$$
12	11	onordi	$$⊢\mathrm{Ord}\mathrm{bday}\left(X\right)$$
13		eloni	$$⊢A\in \mathrm{On}\to \mathrm{Ord}A$$
14		ordtri4	$$⊢\left(\mathrm{Ord}\mathrm{bday}\left(X\right)\wedge \mathrm{Ord}A\right)\to \left(\mathrm{bday}\left(X\right)=A\leftrightarrow \left(\mathrm{bday}\left(X\right)\subseteq A\wedge \neg \mathrm{bday}\left(X\right)\in A\right)\right)$$
15	12 13 14	sylancr	$$⊢A\in \mathrm{On}\to \left(\mathrm{bday}\left(X\right)=A\leftrightarrow \left(\mathrm{bday}\left(X\right)\subseteq A\wedge \neg \mathrm{bday}\left(X\right)\in A\right)\right)$$
16	15	adantr	$$⊢\left(A\in \mathrm{On}\wedge X\in \mathrm{No}\right)\to \left(\mathrm{bday}\left(X\right)=A\leftrightarrow \left(\mathrm{bday}\left(X\right)\subseteq A\wedge \neg \mathrm{bday}\left(X\right)\in A\right)\right)$$
17	4 10 16	3bitr4d	Could not format ( ( A e. On /\ X e. No ) -> ( X e. ( _New ` A ) <-> ( bday ` X ) = A ) ) : No typesetting found for |- ( ( A e. On /\ X e. No ) -> ( X e. ( _New ` A ) <-> ( bday ` X ) = A ) ) with typecode |-