Theorem made0

Description: The only surreal made on day (/) is 0s . (Contributed by Scott Fenton, 7-Aug-2024)

	Ref	Expression
Assertion	made0	|- ( _M ` (/) ) = { 0s }

Proof

Step	Hyp	Ref	Expression
1		0elon	|- (/) e. On
2		madeval2	|- ( (/) e. On -> ( _M ` (/) ) = { x e. No | E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l <
3	1 2	ax-mp	|- ( _M ` (/) ) = { x e. No | E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l <
4		rabeqsn	|- ( { x e. No | E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < A. x ( ( x e. No /\ E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < x = 0s ) )
5		0elpw	|- (/) e. ~P No
6		nulssgt	|- ( (/) e. ~P No -> (/) <
7	5 6	ax-mp	|- (/) <
8		ima0	|- ( _M " (/) ) = (/)
9	8	unieqi	|- U. ( _M " (/) ) = U. (/)
10		uni0	|- U. (/) = (/)
11	9 10	eqtri	|- U. ( _M " (/) ) = (/)
12	11	pweqi	|- ~P U. ( _M " (/) ) = ~P (/)
13		pw0	|- ~P (/) = { (/) }
14	12 13	eqtri	|- ~P U. ( _M " (/) ) = { (/) }
15	14	rexeqi	|- ( E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < E. l e. { (/) } E. r e. ~P U. ( _M " (/) ) ( l <
16	14	rexeqi	|- ( E. r e. ~P U. ( _M " (/) ) ( l < E. r e. { (/) } ( l <
17	16	rexbii	|- ( E. l e. { (/) } E. r e. ~P U. ( _M " (/) ) ( l < E. l e. { (/) } E. r e. { (/) } ( l <
18		0ex	|- (/) e. _V
19		breq2	|- ( r = (/) -> ( l < l <
20		oveq2	|- ( r = (/) -> ( l |s r ) = ( l |s (/) ) )
21	20	eqeq1d	|- ( r = (/) -> ( ( l |s r ) = x <-> ( l |s (/) ) = x ) )
22	19 21	anbi12d	|- ( r = (/) -> ( ( l < ( l <
23	18 22	rexsn	|- ( E. r e. { (/) } ( l < ( l <
24	23	rexbii	|- ( E. l e. { (/) } E. r e. { (/) } ( l < E. l e. { (/) } ( l <
25		breq1	|- ( l = (/) -> ( l < (/) <
26		oveq1	|- ( l = (/) -> ( l |s (/) ) = ( (/) |s (/) ) )
27	26	eqeq1d	|- ( l = (/) -> ( ( l |s (/) ) = x <-> ( (/) |s (/) ) = x ) )
28	25 27	anbi12d	|- ( l = (/) -> ( ( l < ( (/) <
29	18 28	rexsn	|- ( E. l e. { (/) } ( l < ( (/) <
30	24 29	bitri	|- ( E. l e. { (/) } E. r e. { (/) } ( l < ( (/) <
31	15 17 30	3bitri	|- ( E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < ( (/) <
32	7 31	mpbiran	|- ( E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < ( (/) |s (/) ) = x )
33		df-0s	|- 0s = ( (/) |s (/) )
34	33	eqeq1i	|- ( 0s = x <-> ( (/) |s (/) ) = x )
35		eqcom	|- ( 0s = x <-> x = 0s )
36	32 34 35	3bitr2i	|- ( E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < x = 0s )
37	36	anbi2i	|- ( ( x e. No /\ E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < ( x e. No /\ x = 0s ) )
38		0sno	|- 0s e. No
39		eleq1	|- ( x = 0s -> ( x e. No <-> 0s e. No ) )
40	38 39	mpbiri	|- ( x = 0s -> x e. No )
41	40	pm4.71ri	|- ( x = 0s <-> ( x e. No /\ x = 0s ) )
42	37 41	bitr4i	|- ( ( x e. No /\ E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < x = 0s )
43	4 42	mpgbir	|- { x e. No | E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l <
44	3 43	eqtri	|- ( _M ` (/) ) = { 0s }