Metamath Proof Explorer

Theorem bday0b

Description: The only surreal with birthday (/) is 0s . (Contributed by Scott Fenton, 8-Aug-2024)

Ref Expression
Assertion bday0b ⊢ X ∈ No → bday ⁡ X = ∅ ↔ X = 0 s

Proof

Step Hyp Ref Expression
1 df-0s ⊢ 0 s = ∅ | s ∅
2 snelpwi ⊢ X ∈ No → X ∈ 𝒫 No
3 nulsslt ⊢ X ∈ 𝒫 No → ∅ ≪ s X
4 2 3 syl ⊢ X ∈ No → ∅ ≪ s X
5 4 adantr ⊢ X ∈ No ∧ bday ⁡ X = ∅ → ∅ ≪ s X
6 nulssgt ⊢ X ∈ 𝒫 No → X ≪ s ∅
7 2 6 syl ⊢ X ∈ No → X ≪ s ∅
8 7 adantr ⊢ X ∈ No ∧ bday ⁡ X = ∅ → X ≪ s ∅
9 id ⊢ bday ⁡ X = ∅ → bday ⁡ X = ∅
10 0ss ⊢ ∅ ⊆ bday ⁡ x
11 9 10 eqsstrdi ⊢ bday ⁡ X = ∅ → bday ⁡ X ⊆ bday ⁡ x
12 11 a1d ⊢ bday ⁡ X = ∅ → ∅ ≪ s x ∧ x ≪ s ∅ → bday ⁡ X ⊆ bday ⁡ x
13 12 adantl ⊢ X ∈ No ∧ bday ⁡ X = ∅ → ∅ ≪ s x ∧ x ≪ s ∅ → bday ⁡ X ⊆ bday ⁡ x
14 13 ralrimivw ⊢ X ∈ No ∧ bday ⁡ X = ∅ → ∀ x ∈ No ∅ ≪ s x ∧ x ≪ s ∅ → bday ⁡ X ⊆ bday ⁡ x
15 0elpw ⊢ ∅ ∈ 𝒫 No
16 nulssgt ⊢ ∅ ∈ 𝒫 No → ∅ ≪ s ∅
17 15 16 ax-mp ⊢ ∅ ≪ s ∅
18 eqscut2 ⊢ ∅ ≪ s ∅ ∧ X ∈ No → ∅ | s ∅ = X ↔ ∅ ≪ s X ∧ X ≪ s ∅ ∧ ∀ x ∈ No ∅ ≪ s x ∧ x ≪ s ∅ → bday ⁡ X ⊆ bday ⁡ x
19 17 18 mpan ⊢ X ∈ No → ∅ | s ∅ = X ↔ ∅ ≪ s X ∧ X ≪ s ∅ ∧ ∀ x ∈ No ∅ ≪ s x ∧ x ≪ s ∅ → bday ⁡ X ⊆ bday ⁡ x
20 19 adantr ⊢ X ∈ No ∧ bday ⁡ X = ∅ → ∅ | s ∅ = X ↔ ∅ ≪ s X ∧ X ≪ s ∅ ∧ ∀ x ∈ No ∅ ≪ s x ∧ x ≪ s ∅ → bday ⁡ X ⊆ bday ⁡ x
21 5 8 14 20 mpbir3and ⊢ X ∈ No ∧ bday ⁡ X = ∅ → ∅ | s ∅ = X
22 1 21 eqtr2id ⊢ X ∈ No ∧ bday ⁡ X = ∅ → X = 0 s
23 22 ex ⊢ X ∈ No → bday ⁡ X = ∅ → X = 0 s
24 fveq2 ⊢ X = 0 s → bday ⁡ X = bday ⁡ 0 s
25 bday0s ⊢ bday ⁡ 0 s = ∅
26 24 25 eqtrdi ⊢ X = 0 s → bday ⁡ X = ∅
27 23 26 impbid1 ⊢ X ∈ No → bday ⁡ X = ∅ ↔ X = 0 s