Metamath Proof Explorer

Theorem oldbday

Description: A surreal is part of the set older than ordinal A iff its birthday is less than A . Remark in Conway p. 29. (Contributed by Scott Fenton, 19-Aug-2024)

Ref Expression
Assertion oldbday ⊢ A ∈ On ∧ X ∈ No → X ∈ Old ⁡ A ↔ bday ⁡ X ∈ A

Proof

Step Hyp Ref Expression
1 oldbdayim ⊢ X ∈ Old ⁡ A → bday ⁡ X ∈ A
2 simpl ⊢ A ∈ On ∧ X ∈ No → A ∈ On
3 onelon ⊢ A ∈ On ∧ b ∈ A → b ∈ On
4 madebday ⊢ b ∈ On ∧ y ∈ No → y ∈ M ⁡ b ↔ bday ⁡ y ⊆ b
5 4 biimprd ⊢ b ∈ On ∧ y ∈ No → bday ⁡ y ⊆ b → y ∈ M ⁡ b
6 3 5 sylan ⊢ A ∈ On ∧ b ∈ A ∧ y ∈ No → bday ⁡ y ⊆ b → y ∈ M ⁡ b
7 6 anasss ⊢ A ∈ On ∧ b ∈ A ∧ y ∈ No → bday ⁡ y ⊆ b → y ∈ M ⁡ b
8 7 ralrimivva ⊢ A ∈ On → ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b
9 8 adantr ⊢ A ∈ On ∧ X ∈ No → ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b
10 simpr ⊢ A ∈ On ∧ X ∈ No → X ∈ No
11 madebdaylemold ⊢ A ∈ On ∧ ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → bday ⁡ X ∈ A → X ∈ Old ⁡ A
12 2 9 10 11 syl3anc ⊢ A ∈ On ∧ X ∈ No → bday ⁡ X ∈ A → X ∈ Old ⁡ A
13 1 12 impbid2 ⊢ A ∈ On ∧ X ∈ No → X ∈ Old ⁡ A ↔ bday ⁡ X ∈ A