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	⊢ ∅ ∈ On
2		madeval2	⊢ ( ∅ ∈ On → ( M ‘ ∅ ) = { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ ∅ ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } )
3	1 2	ax-mp	⊢ ( M ‘ ∅ ) = { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ ∅ ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) }
4		rabeqsn	⊢ ( { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ ∅ ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } = { 0s } ↔ ∀ 𝑥 ( ( 𝑥 ∈ No ∧ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ ∅ ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) ↔ 𝑥 = 0s ) )
5		0elpw	⊢ ∅ ∈ 𝒫 No
6		nulssgt	⊢ ( ∅ ∈ 𝒫 No → ∅ <<s ∅ )
7	5 6	ax-mp	⊢ ∅ <<s ∅
8		ima0	⊢ ( M “ ∅ ) = ∅
9	8	unieqi	⊢ ∪ ( M “ ∅ ) = ∪ ∅
10		uni0	⊢ ∪ ∅ = ∅
11	9 10	eqtri	⊢ ∪ ( M “ ∅ ) = ∅
12	11	pweqi	⊢ 𝒫 ∪ ( M “ ∅ ) = 𝒫 ∅
13		pw0	⊢ 𝒫 ∅ = { ∅ }
14	12 13	eqtri	⊢ 𝒫 ∪ ( M “ ∅ ) = { ∅ }
15	14	rexeqi	⊢ ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ ∅ ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ ∃ 𝑙 ∈ { ∅ } ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) )
16	14	rexeqi	⊢ ( ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ ∃ 𝑟 ∈ { ∅ } ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) )
17	16	rexbii	⊢ ( ∃ 𝑙 ∈ { ∅ } ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ ∃ 𝑙 ∈ { ∅ } ∃ 𝑟 ∈ { ∅ } ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) )
18		0ex	⊢ ∅ ∈ V
19		breq2	⊢ ( 𝑟 = ∅ → ( 𝑙 <<s 𝑟 ↔ 𝑙 <<s ∅ ) )
20		oveq2	⊢ ( 𝑟 = ∅ → ( 𝑙 |s 𝑟 ) = ( 𝑙 |s ∅ ) )
21	20	eqeq1d	⊢ ( 𝑟 = ∅ → ( ( 𝑙 |s 𝑟 ) = 𝑥 ↔ ( 𝑙 |s ∅ ) = 𝑥 ) )
22	19 21	anbi12d	⊢ ( 𝑟 = ∅ → ( ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ ( 𝑙 <<s ∅ ∧ ( 𝑙 |s ∅ ) = 𝑥 ) ) )
23	18 22	rexsn	⊢ ( ∃ 𝑟 ∈ { ∅ } ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ ( 𝑙 <<s ∅ ∧ ( 𝑙 |s ∅ ) = 𝑥 ) )
24	23	rexbii	⊢ ( ∃ 𝑙 ∈ { ∅ } ∃ 𝑟 ∈ { ∅ } ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ ∃ 𝑙 ∈ { ∅ } ( 𝑙 <<s ∅ ∧ ( 𝑙 |s ∅ ) = 𝑥 ) )
25		breq1	⊢ ( 𝑙 = ∅ → ( 𝑙 <<s ∅ ↔ ∅ <<s ∅ ) )
26		oveq1	⊢ ( 𝑙 = ∅ → ( 𝑙 |s ∅ ) = ( ∅ |s ∅ ) )
27	26	eqeq1d	⊢ ( 𝑙 = ∅ → ( ( 𝑙 |s ∅ ) = 𝑥 ↔ ( ∅ |s ∅ ) = 𝑥 ) )
28	25 27	anbi12d	⊢ ( 𝑙 = ∅ → ( ( 𝑙 <<s ∅ ∧ ( 𝑙 |s ∅ ) = 𝑥 ) ↔ ( ∅ <<s ∅ ∧ ( ∅ |s ∅ ) = 𝑥 ) ) )
29	18 28	rexsn	⊢ ( ∃ 𝑙 ∈ { ∅ } ( 𝑙 <<s ∅ ∧ ( 𝑙 |s ∅ ) = 𝑥 ) ↔ ( ∅ <<s ∅ ∧ ( ∅ |s ∅ ) = 𝑥 ) )
30	24 29	bitri	⊢ ( ∃ 𝑙 ∈ { ∅ } ∃ 𝑟 ∈ { ∅ } ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ ( ∅ <<s ∅ ∧ ( ∅ |s ∅ ) = 𝑥 ) )
31	15 17 30	3bitri	⊢ ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ ∅ ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ ( ∅ <<s ∅ ∧ ( ∅ |s ∅ ) = 𝑥 ) )
32	7 31	mpbiran	⊢ ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ ∅ ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ ( ∅ |s ∅ ) = 𝑥 )
33		df-0s	⊢ 0s = ( ∅ |s ∅ )
34	33	eqeq1i	⊢ ( 0s = 𝑥 ↔ ( ∅ |s ∅ ) = 𝑥 )
35		eqcom	⊢ ( 0s = 𝑥 ↔ 𝑥 = 0s )
36	32 34 35	3bitr2i	⊢ ( ∃ 𝑙 ∈ 𝒫 ∪ ( M “ ∅ ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ↔ 𝑥 = 0s )
37	36	anbi2i	⊢ ( ( 𝑥 ∈ No ∧ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ ∅ ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) ↔ ( 𝑥 ∈ No ∧ 𝑥 = 0s ) )
38		0sno	⊢ 0s ∈ No
39		eleq1	⊢ ( 𝑥 = 0s → ( 𝑥 ∈ No ↔ 0s ∈ No ) )
40	38 39	mpbiri	⊢ ( 𝑥 = 0s → 𝑥 ∈ No )
41	40	pm4.71ri	⊢ ( 𝑥 = 0s ↔ ( 𝑥 ∈ No ∧ 𝑥 = 0s ) )
42	37 41	bitr4i	⊢ ( ( 𝑥 ∈ No ∧ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ ∅ ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) ) ↔ 𝑥 = 0s )
43	4 42	mpgbir	⊢ { 𝑥 ∈ No ∣ ∃ 𝑙 ∈ 𝒫 ∪ ( M “ ∅ ) ∃ 𝑟 ∈ 𝒫 ∪ ( M “ ∅ ) ( 𝑙 <<s 𝑟 ∧ ( 𝑙 |s 𝑟 ) = 𝑥 ) } = { 0s }
44	3 43	eqtri	⊢ ( M ‘ ∅ ) = { 0s }