Metamath Proof Explorer

Theorem made0

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

Ref Expression
Assertion made0 ⊢ M ⁡ ∅ = 0 s

Proof

Step Hyp Ref Expression
1 0elon ⊢ ∅ ∈ On
2 madeval2 ⊢ ∅ ∈ On → M ⁡ ∅ = x ∈ No | ∃ l ∈ 𝒫 ⋃ M ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x
3 1 2 ax-mp ⊢ M ⁡ ∅ = x ∈ No | ∃ l ∈ 𝒫 ⋃ M ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x
4 rabeqsn ⊢ x ∈ No | ∃ l ∈ 𝒫 ⋃ M ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x = 0 s ↔ ∀ x x ∈ No ∧ ∃ l ∈ 𝒫 ⋃ M ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x ↔ x = 0 s
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 ⊢ ∃ l ∈ 𝒫 ⋃ M ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x ↔ ∃ l ∈ ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x
16 14 rexeqi ⊢ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x ↔ ∃ r ∈ ∅ l ≪ s r ∧ l | s r = x
17 16 rexbii ⊢ ∃ l ∈ ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x ↔ ∃ l ∈ ∅ ∃ r ∈ ∅ l ≪ s r ∧ l | s r = x
18 0ex ⊢ ∅ ∈ V
19 breq2 ⊢ r = ∅ → l ≪ s r ↔ l ≪ s ∅
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 ≪ s r ∧ l | s r = x ↔ l ≪ s ∅ ∧ l | s ∅ = x
23 18 22 rexsn ⊢ ∃ r ∈ ∅ l ≪ s r ∧ l | s r = x ↔ l ≪ s ∅ ∧ l | s ∅ = x
24 23 rexbii ⊢ ∃ l ∈ ∅ ∃ r ∈ ∅ l ≪ s r ∧ l | s r = x ↔ ∃ l ∈ ∅ l ≪ s ∅ ∧ l | s ∅ = x
25 breq1 ⊢ l = ∅ → l ≪ s ∅ ↔ ∅ ≪ s ∅
26 oveq1 ⊢ l = ∅ → l | s ∅ = ∅ | s ∅
27 26 eqeq1d ⊢ l = ∅ → l | s ∅ = x ↔ ∅ | s ∅ = x
28 25 27 anbi12d ⊢ l = ∅ → l ≪ s ∅ ∧ l | s ∅ = x ↔ ∅ ≪ s ∅ ∧ ∅ | s ∅ = x
29 18 28 rexsn ⊢ ∃ l ∈ ∅ l ≪ s ∅ ∧ l | s ∅ = x ↔ ∅ ≪ s ∅ ∧ ∅ | s ∅ = x
30 24 29 bitri ⊢ ∃ l ∈ ∅ ∃ r ∈ ∅ l ≪ s r ∧ l | s r = x ↔ ∅ ≪ s ∅ ∧ ∅ | s ∅ = x
31 15 17 30 3bitri ⊢ ∃ l ∈ 𝒫 ⋃ M ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x ↔ ∅ ≪ s ∅ ∧ ∅ | s ∅ = x
32 7 31 mpbiran ⊢ ∃ l ∈ 𝒫 ⋃ M ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x ↔ ∅ | s ∅ = x
33 df-0s ⊢ 0 s = ∅ | s ∅
34 33 eqeq1i ⊢ 0 s = x ↔ ∅ | s ∅ = x
35 eqcom ⊢ 0 s = x ↔ x = 0 s
36 32 34 35 3bitr2i ⊢ ∃ l ∈ 𝒫 ⋃ M ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x ↔ x = 0 s
37 36 anbi2i ⊢ x ∈ No ∧ ∃ l ∈ 𝒫 ⋃ M ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x ↔ x ∈ No ∧ x = 0 s
38 0sno ⊢ 0 s ∈ No
39 eleq1 ⊢ x = 0 s → x ∈ No ↔ 0 s ∈ No
40 38 39 mpbiri ⊢ x = 0 s → x ∈ No
41 40 pm4.71ri ⊢ x = 0 s ↔ x ∈ No ∧ x = 0 s
42 37 41 bitr4i ⊢ x ∈ No ∧ ∃ l ∈ 𝒫 ⋃ M ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x ↔ x = 0 s
43 4 42 mpgbir ⊢ x ∈ No | ∃ l ∈ 𝒫 ⋃ M ∅ ∃ r ∈ 𝒫 ⋃ M ∅ l ≪ s r ∧ l | s r = x = 0 s
44 3 43 eqtri ⊢ M ⁡ ∅ = 0 s