Metamath Proof Explorer

Theorem oldbdayim

Description: If X is in the old set for A , then the birthday of X is less than A . (Contributed by Scott Fenton, 10-Aug-2024)

Ref Expression
Assertion oldbdayim ⊢ X ∈ Old ⁡ A → bday ⁡ X ∈ A

Proof

Step Hyp Ref Expression
1 elfvdm ⊢ X ∈ Old ⁡ A → A ∈ dom ⁡ Old
2 oldf ⊢ Old : On ⟶ 𝒫 No
3 2 fdmi ⊢ dom ⁡ Old = On
4 1 3 eleqtrdi ⊢ X ∈ Old ⁡ A → A ∈ On
5 elold ⊢ A ∈ On → X ∈ Old ⁡ A ↔ ∃ b ∈ A X ∈ M ⁡ b
6 madebdayim ⊢ X ∈ M ⁡ b → bday ⁡ X ⊆ b
7 6 ad2antll ⊢ A ∈ On ∧ b ∈ A ∧ X ∈ M ⁡ b → bday ⁡ X ⊆ b
8 simprl ⊢ A ∈ On ∧ b ∈ A ∧ X ∈ M ⁡ b → b ∈ A
9 bdayon ⊢ bday ⁡ X ∈ On
10 ontr2 ⊢ bday ⁡ X ∈ On ∧ A ∈ On → bday ⁡ X ⊆ b ∧ b ∈ A → bday ⁡ X ∈ A
11 9 10 mpan ⊢ A ∈ On → bday ⁡ X ⊆ b ∧ b ∈ A → bday ⁡ X ∈ A
12 11 adantr ⊢ A ∈ On ∧ b ∈ A ∧ X ∈ M ⁡ b → bday ⁡ X ⊆ b ∧ b ∈ A → bday ⁡ X ∈ A
13 7 8 12 mp2and ⊢ A ∈ On ∧ b ∈ A ∧ X ∈ M ⁡ b → bday ⁡ X ∈ A
14 13 rexlimdvaa ⊢ A ∈ On → ∃ b ∈ A X ∈ M ⁡ b → bday ⁡ X ∈ A
15 5 14 sylbid ⊢ A ∈ On → X ∈ Old ⁡ A → bday ⁡ X ∈ A
16 4 15 mpcom ⊢ X ∈ Old ⁡ A → bday ⁡ X ∈ A