Theorem made0

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

	Ref	Expression
Assertion	made0	Could not format assertion : No typesetting found for |- ( _M ` (/) ) = { 0s } with typecode |-

Proof

Step	Hyp	Ref	Expression
1		0elon	$$⊢\varnothing \in \mathrm{On}$$
2		madeval2	$$⊢\varnothing \in \mathrm{On}\to M\left(\varnothing \right)=\left\{x\in \mathrm{No}|\exists l\in 𝒫\bigcup M\left[\varnothing \right]\exists r\in 𝒫\bigcup M\left[\varnothing \right]\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\right\}$$
3	1 2	ax-mp	$$⊢M\left(\varnothing \right)=\left\{x\in \mathrm{No}|\exists l\in 𝒫\bigcup M\left[\varnothing \right]\exists r\in 𝒫\bigcup M\left[\varnothing \right]\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\right\}$$
4		rabeqsn	Could not format ( { 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 ) ) : No typesetting found for |- ( { 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 ) ) with typecode |-
5		0elpw	$$⊢\varnothing \in 𝒫\mathrm{No}$$
6		nulssgt	$$⊢\varnothing \in 𝒫\mathrm{No}\to \varnothing {\ll }_s\varnothing$$
7	5 6	ax-mp	$$⊢\varnothing {\ll }_s\varnothing$$
8		ima0	$$⊢M\left[\varnothing \right]=\varnothing$$
9	8	unieqi	$$⊢\bigcup M\left[\varnothing \right]=\bigcup \varnothing$$
10		uni0	$$⊢\bigcup \varnothing =\varnothing$$
11	9 10	eqtri	$$⊢\bigcup M\left[\varnothing \right]=\varnothing$$
12	11	pweqi	$$⊢𝒫\bigcup M\left[\varnothing \right]=𝒫\varnothing$$
13		pw0	$$⊢𝒫\varnothing =\left\{\varnothing \right\}$$
14	12 13	eqtri	$$⊢𝒫\bigcup M\left[\varnothing \right]=\left\{\varnothing \right\}$$
15	14	rexeqi	$$⊢\exists l\in 𝒫\bigcup M\left[\varnothing \right]\exists r\in 𝒫\bigcup M\left[\varnothing \right]\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\leftrightarrow \exists l\in \left\{\varnothing \right\}\exists r\in 𝒫\bigcup M\left[\varnothing \right]\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)$$
16	14	rexeqi	$$⊢\exists r\in 𝒫\bigcup M\left[\varnothing \right]\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\leftrightarrow \exists r\in \left\{\varnothing \right\}\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)$$
17	16	rexbii	$$⊢\exists l\in \left\{\varnothing \right\}\exists r\in 𝒫\bigcup M\left[\varnothing \right]\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\leftrightarrow \exists l\in \left\{\varnothing \right\}\exists r\in \left\{\varnothing \right\}\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)$$
18		0ex	$$⊢\varnothing \in \mathrm{V}$$
19		breq2	$$⊢r=\varnothing \to \left(l{\ll }_{s}r\leftrightarrow l{\ll }_s\varnothing \right)$$
20		oveq2	$$⊢r=\varnothing \to l{|}_{s}r=l{|}_s\varnothing$$
21	20	eqeq1d	$$⊢r=\varnothing \to \left(l{|}_{s}r=x\leftrightarrow l{|}_s\varnothing =x\right)$$
22	19 21	anbi12d	$$⊢r=\varnothing \to \left(\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\leftrightarrow \left(l{\ll }_s\varnothing \wedge l{|}_s\varnothing =x\right)\right)$$
23	18 22	rexsn	$$⊢\exists r\in \left\{\varnothing \right\}\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\leftrightarrow \left(l{\ll }_s\varnothing \wedge l{|}_s\varnothing =x\right)$$
24	23	rexbii	$$⊢\exists l\in \left\{\varnothing \right\}\exists r\in \left\{\varnothing \right\}\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\leftrightarrow \exists l\in \left\{\varnothing \right\}\left(l{\ll }_s\varnothing \wedge l{|}_s\varnothing =x\right)$$
25		breq1	$$⊢l=\varnothing \to \left(l{\ll }_s\varnothing \leftrightarrow \varnothing {\ll }_s\varnothing \right)$$
26		oveq1	$$⊢l=\varnothing \to l{|}_s\varnothing =\varnothing {|}_s\varnothing$$
27	26	eqeq1d	$$⊢l=\varnothing \to \left(l{|}_s\varnothing =x\leftrightarrow \varnothing {|}_s\varnothing =x\right)$$
28	25 27	anbi12d	$$⊢l=\varnothing \to \left(\left(l{\ll }_s\varnothing \wedge l{|}_s\varnothing =x\right)\leftrightarrow \left(\varnothing {\ll }_s\varnothing \wedge \varnothing {|}_s\varnothing =x\right)\right)$$
29	18 28	rexsn	$$⊢\exists l\in \left\{\varnothing \right\}\left(l{\ll }_s\varnothing \wedge l{|}_s\varnothing =x\right)\leftrightarrow \left(\varnothing {\ll }_s\varnothing \wedge \varnothing {|}_s\varnothing =x\right)$$
30	24 29	bitri	$$⊢\exists l\in \left\{\varnothing \right\}\exists r\in \left\{\varnothing \right\}\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\leftrightarrow \left(\varnothing {\ll }_s\varnothing \wedge \varnothing {|}_s\varnothing =x\right)$$
31	15 17 30	3bitri	$$⊢\exists l\in 𝒫\bigcup M\left[\varnothing \right]\exists r\in 𝒫\bigcup M\left[\varnothing \right]\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\leftrightarrow \left(\varnothing {\ll }_s\varnothing \wedge \varnothing {|}_s\varnothing =x\right)$$
32	7 31	mpbiran	$$⊢\exists l\in 𝒫\bigcup M\left[\varnothing \right]\exists r\in 𝒫\bigcup M\left[\varnothing \right]\left(l{\ll }_{s}r\wedge l{|}_{s}r=x\right)\leftrightarrow \varnothing {|}_s\varnothing =x$$
33		df-0s	Could not format 0s = ( (/) |s (/) ) : No typesetting found for |- 0s = ( (/) |s (/) ) with typecode |-
34	33	eqeq1i	Could not format ( 0s = x <-> ( (/) |s (/) ) = x ) : No typesetting found for |- ( 0s = x <-> ( (/) |s (/) ) = x ) with typecode |-
35		eqcom	Could not format ( 0s = x <-> x = 0s ) : No typesetting found for |- ( 0s = x <-> x = 0s ) with typecode |-
36	32 34 35	3bitr2i	Could not format ( E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < x = 0s ) : No typesetting found for |- ( E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < x = 0s ) with typecode |-
37	36	anbi2i	Could not format ( ( x e. No /\ E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < ( x e. No /\ x = 0s ) ) : No typesetting found for |- ( ( x e. No /\ E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < ( x e. No /\ x = 0s ) ) with typecode |-
38		0sno	Could not format 0s e. No : No typesetting found for |- 0s e. No with typecode |-
39		eleq1	Could not format ( x = 0s -> ( x e. No <-> 0s e. No ) ) : No typesetting found for |- ( x = 0s -> ( x e. No <-> 0s e. No ) ) with typecode |-
40	38 39	mpbiri	Could not format ( x = 0s -> x e. No ) : No typesetting found for |- ( x = 0s -> x e. No ) with typecode |-
41	40	pm4.71ri	Could not format ( x = 0s <-> ( x e. No /\ x = 0s ) ) : No typesetting found for |- ( x = 0s <-> ( x e. No /\ x = 0s ) ) with typecode |-
42	37 41	bitr4i	Could not format ( ( x e. No /\ E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < x = 0s ) : No typesetting found for |- ( ( x e. No /\ E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l < x = 0s ) with typecode |-
43	4 42	mpgbir	Could not format { x e. No | E. l e. ~P U. ( _M " (/) ) E. r e. ~P U. ( _M " (/) ) ( l <
44	3 43	eqtri	Could not format ( _M ` (/) ) = { 0s } : No typesetting found for |- ( _M ` (/) ) = { 0s } with typecode |-