Theorem bday1s

Description: The birthday of surreal one is ordinal one. (Contributed by Scott Fenton, 8-Aug-2024)

	Ref	Expression
Assertion	bday1s	Could not format assertion : No typesetting found for |- ( bday ` 1s ) = 1o with typecode |-

Proof

Step	Hyp	Ref	Expression
1		df-1s	Could not format 1s = ( { 0s } |s (/) ) : No typesetting found for |- 1s = ( { 0s } |s (/) ) with typecode |-
2	1	fveq2i	Could not format ( bday ` 1s ) = ( bday ` ( { 0s } |s (/) ) ) : No typesetting found for |- ( bday ` 1s ) = ( bday ` ( { 0s } |s (/) ) ) with typecode |-
3		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
4		snelpwi	Could not format ( 0s e. No -> { 0s } e. ~P No ) : No typesetting found for |- ( 0s e. No -> { 0s } e. ~P No ) with typecode |-
5	3 4	ax-mp	Could not format { 0s } e. ~P No : No typesetting found for |- { 0s } e. ~P No with typecode |-
6		nulssgt	Could not format ( { 0s } e. ~P No -> { 0s } < { 0s } <
7	5 6	ax-mp	Could not format { 0s } <
8		scutbdaybnd2	Could not format ( { 0s } < ( bday ` ( { 0s } |s (/) ) ) C_ suc U. ( bday " ( { 0s } u. (/) ) ) ) : No typesetting found for |- ( { 0s } < ( bday ` ( { 0s } |s (/) ) ) C_ suc U. ( bday " ( { 0s } u. (/) ) ) ) with typecode |-
9	7 8	ax-mp	Could not format ( bday ` ( { 0s } |s (/) ) ) C_ suc U. ( bday " ( { 0s } u. (/) ) ) : No typesetting found for |- ( bday ` ( { 0s } |s (/) ) ) C_ suc U. ( bday " ( { 0s } u. (/) ) ) with typecode |-
10		un0	Could not format ( { 0s } u. (/) ) = { 0s } : No typesetting found for |- ( { 0s } u. (/) ) = { 0s } with typecode |-
11	10	imaeq2i	Could not format ( bday " ( { 0s } u. (/) ) ) = ( bday " { 0s } ) : No typesetting found for |- ( bday " ( { 0s } u. (/) ) ) = ( bday " { 0s } ) with typecode |-
12		bdayfn	$$⊢\mathrm{bday}Fn\mathrm{No}$$
13		fnsnfv	Could not format ( ( bday Fn No /\ 0s e. No ) -> { ( bday ` 0s ) } = ( bday " { 0s } ) ) : No typesetting found for |- ( ( bday Fn No /\ 0s e. No ) -> { ( bday ` 0s ) } = ( bday " { 0s } ) ) with typecode |-
14	12 3 13	mp2an	Could not format { ( bday ` 0s ) } = ( bday " { 0s } ) : No typesetting found for |- { ( bday ` 0s ) } = ( bday " { 0s } ) with typecode |-
15		bday0s	Could not format ( bday ` 0s ) = (/) : No typesetting found for |- ( bday ` 0s ) = (/) with typecode |-
16	15	sneqi	Could not format { ( bday ` 0s ) } = { (/) } : No typesetting found for |- { ( bday ` 0s ) } = { (/) } with typecode |-
17	11 14 16	3eqtr2i	Could not format ( bday " ( { 0s } u. (/) ) ) = { (/) } : No typesetting found for |- ( bday " ( { 0s } u. (/) ) ) = { (/) } with typecode |-
18	17	unieqi	Could not format U. ( bday " ( { 0s } u. (/) ) ) = U. { (/) } : No typesetting found for |- U. ( bday " ( { 0s } u. (/) ) ) = U. { (/) } with typecode |-
19		0ex	$$⊢\varnothing \in \mathrm{V}$$
20	19	unisn	$$⊢\bigcup \left\{\varnothing \right\}=\varnothing$$
21	18 20	eqtri	Could not format U. ( bday " ( { 0s } u. (/) ) ) = (/) : No typesetting found for |- U. ( bday " ( { 0s } u. (/) ) ) = (/) with typecode |-
22		suceq	Could not format ( U. ( bday " ( { 0s } u. (/) ) ) = (/) -> suc U. ( bday " ( { 0s } u. (/) ) ) = suc (/) ) : No typesetting found for |- ( U. ( bday " ( { 0s } u. (/) ) ) = (/) -> suc U. ( bday " ( { 0s } u. (/) ) ) = suc (/) ) with typecode |-
23	21 22	ax-mp	Could not format suc U. ( bday " ( { 0s } u. (/) ) ) = suc (/) : No typesetting found for |- suc U. ( bday " ( { 0s } u. (/) ) ) = suc (/) with typecode |-
24		df-1o	$$⊢1_{𝑜}=\mathrm{suc}\varnothing$$
25	23 24	eqtr4i	Could not format suc U. ( bday " ( { 0s } u. (/) ) ) = 1o : No typesetting found for |- suc U. ( bday " ( { 0s } u. (/) ) ) = 1o with typecode |-
26	9 25	sseqtri	Could not format ( bday ` ( { 0s } |s (/) ) ) C_ 1o : No typesetting found for |- ( bday ` ( { 0s } |s (/) ) ) C_ 1o with typecode |-
27		ssrab2	Could not format { x e. No | ( { 0s } <
28		fnssintima	Could not format ( ( bday Fn No /\ { x e. No | ( { 0s } < ( 1o C_ |^| ( bday " { x e. No | ( { 0s } < A. y e. { x e. No | ( { 0s } < ( 1o C_ |^| ( bday " { x e. No | ( { 0s } < A. y e. { x e. No | ( { 0s } <
29	12 27 28	mp2an	Could not format ( 1o C_ |^| ( bday " { x e. No | ( { 0s } < A. y e. { x e. No | ( { 0s } < A. y e. { x e. No | ( { 0s } <
30		sneq	$$⊢x=y\to \left\{x\right\}=\left\{y\right\}$$
31	30	breq2d	Could not format ( x = y -> ( { 0s } < { 0s } < ( { 0s } < { 0s } <
32	30	breq1d	$$⊢x=y\to \left(\left\{x\right\}{\ll }_s\varnothing \leftrightarrow \left\{y\right\}{\ll }_s\varnothing \right)$$
33	31 32	anbi12d	Could not format ( x = y -> ( ( { 0s } < ( { 0s } < ( ( { 0s } < ( { 0s } <
34	33	elrab	Could not format ( y e. { x e. No | ( { 0s } < ( y e. No /\ ( { 0s } < ( y e. No /\ ( { 0s } <
35		sltirr	Could not format ( 0s e. No -> -. 0s -. 0s
36	3 35	ax-mp	Could not format -. 0s
37		breq2	Could not format ( y = 0s -> ( 0s 0s ( 0s 0s
38	36 37	mtbiri	Could not format ( y = 0s -> -. 0s -. 0s
39	38	necon2ai	Could not format ( 0s y =/= 0s ) : No typesetting found for |- ( 0s y =/= 0s ) with typecode |-
40		bday0b	Could not format ( y e. No -> ( ( bday ` y ) = (/) <-> y = 0s ) ) : No typesetting found for |- ( y e. No -> ( ( bday ` y ) = (/) <-> y = 0s ) ) with typecode |-
41	40	necon3bid	Could not format ( y e. No -> ( ( bday ` y ) =/= (/) <-> y =/= 0s ) ) : No typesetting found for |- ( y e. No -> ( ( bday ` y ) =/= (/) <-> y =/= 0s ) ) with typecode |-
42	39 41	syl5ibr	Could not format ( y e. No -> ( 0s ( bday ` y ) =/= (/) ) ) : No typesetting found for |- ( y e. No -> ( 0s ( bday ` y ) =/= (/) ) ) with typecode |-
43		bdayelon	$$⊢\mathrm{bday}\left(y\right)\in \mathrm{On}$$
44	43	onordi	$$⊢\mathrm{Ord}\mathrm{bday}\left(y\right)$$
45		ordge1n0	$$⊢\mathrm{Ord}\mathrm{bday}\left(y\right)\to \left(1_{𝑜}\subseteq \mathrm{bday}\left(y\right)\leftrightarrow \mathrm{bday}\left(y\right)\ne \varnothing \right)$$
46	44 45	ax-mp	$$⊢1_{𝑜}\subseteq \mathrm{bday}\left(y\right)\leftrightarrow \mathrm{bday}\left(y\right)\ne \varnothing$$
47	42 46	syl6ibr	Could not format ( y e. No -> ( 0s 1o C_ ( bday ` y ) ) ) : No typesetting found for |- ( y e. No -> ( 0s 1o C_ ( bday ` y ) ) ) with typecode |-
48		ssltsep	Could not format ( { 0s } < A. x e. { 0s } A. z e. { y } x A. x e. { 0s } A. z e. { y } x
49		vex	$$⊢y\in \mathrm{V}$$
50		breq2	$$⊢z=y\to \left(x{<}_{s}z\leftrightarrow x{<}_{s}y\right)$$
51	49 50	ralsn	$$⊢\forall z\in \left\{y\right\}x{<}_{s}z\leftrightarrow x{<}_{s}y$$
52	51	ralbii	Could not format ( A. x e. { 0s } A. z e. { y } x A. x e. { 0s } x A. x e. { 0s } x
53	3	elexi	Could not format 0s e. _V : No typesetting found for |- 0s e. _V with typecode |-
54		breq1	Could not format ( x = 0s -> ( x 0s ( x 0s
55	53 54	ralsn	Could not format ( A. x e. { 0s } x 0s 0s
56	52 55	bitri	Could not format ( A. x e. { 0s } A. z e. { y } x 0s 0s
57	48 56	sylib	Could not format ( { 0s } < 0s 0s
58	47 57	impel	Could not format ( ( y e. No /\ { 0s } < 1o C_ ( bday ` y ) ) : No typesetting found for |- ( ( y e. No /\ { 0s } < 1o C_ ( bday ` y ) ) with typecode |-
59	58	adantrr	Could not format ( ( y e. No /\ ( { 0s } < 1o C_ ( bday ` y ) ) : No typesetting found for |- ( ( y e. No /\ ( { 0s } < 1o C_ ( bday ` y ) ) with typecode |-
60	34 59	sylbi	Could not format ( y e. { x e. No | ( { 0s } < 1o C_ ( bday ` y ) ) : No typesetting found for |- ( y e. { x e. No | ( { 0s } < 1o C_ ( bday ` y ) ) with typecode |-
61	29 60	mprgbir	Could not format 1o C_ |^| ( bday " { x e. No | ( { 0s } <
62		scutbday	Could not format ( { 0s } < ( bday ` ( { 0s } |s (/) ) ) = |^| ( bday " { x e. No | ( { 0s } < ( bday ` ( { 0s } |s (/) ) ) = |^| ( bday " { x e. No | ( { 0s } <
63	7 62	ax-mp	Could not format ( bday ` ( { 0s } |s (/) ) ) = |^| ( bday " { x e. No | ( { 0s } <
64	61 63	sseqtrri	Could not format 1o C_ ( bday ` ( { 0s } |s (/) ) ) : No typesetting found for |- 1o C_ ( bday ` ( { 0s } |s (/) ) ) with typecode |-
65	26 64	eqssi	Could not format ( bday ` ( { 0s } |s (/) ) ) = 1o : No typesetting found for |- ( bday ` ( { 0s } |s (/) ) ) = 1o with typecode |-
66	2 65	eqtri	Could not format ( bday ` 1s ) = 1o : No typesetting found for |- ( bday ` 1s ) = 1o with typecode |-