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 ⊢ A ∈ On ∧ X ∈ Old ⁡ A → bday ⁡ X ∈ A
2 1 ex ⊢ A ∈ On → X ∈ Old ⁡ A → bday ⁡ X ∈ A
3 2 adantr ⊢ A ∈ On ∧ X ∈ No → X ∈ Old ⁡ A → bday ⁡ X ∈ A
4 simpl ⊢ A ∈ On ∧ X ∈ No → A ∈ On
5 onelon ⊢ A ∈ On ∧ b ∈ A → b ∈ On
6 madebday ⊢ b ∈ On ∧ y ∈ No → y ∈ M ⁡ b ↔ bday ⁡ y ⊆ b
7 6 biimprd ⊢ b ∈ On ∧ y ∈ No → bday ⁡ y ⊆ b → y ∈ M ⁡ b
8 5 7 sylan ⊢ A ∈ On ∧ b ∈ A ∧ y ∈ No → bday ⁡ y ⊆ b → y ∈ M ⁡ b
9 8 anasss ⊢ A ∈ On ∧ b ∈ A ∧ y ∈ No → bday ⁡ y ⊆ b → y ∈ M ⁡ b
10 9 ralrimivva ⊢ A ∈ On → ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b
11 10 adantr ⊢ A ∈ On ∧ X ∈ No → ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b
12 simpr ⊢ A ∈ On ∧ X ∈ No → X ∈ No
13 madebdaylemold ⊢ A ∈ On ∧ ∀ b ∈ A ∀ y ∈ No bday ⁡ y ⊆ b → y ∈ M ⁡ b ∧ X ∈ No → bday ⁡ X ∈ A → X ∈ Old ⁡ A
14 4 11 12 13 syl3anc ⊢ A ∈ On ∧ X ∈ No → bday ⁡ X ∈ A → X ∈ Old ⁡ A
15 3 14 impbid ⊢ A ∈ On ∧ X ∈ No → X ∈ Old ⁡ A ↔ bday ⁡ X ∈ A