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 ⊢ A ∈ On ∧ X ∈ Old ⁡ A → bday ⁡ X ∈ A

Proof

Step Hyp Ref Expression
1 elold ⊢ A ∈ On → X ∈ Old ⁡ A ↔ ∃ b ∈ A X ∈ M ⁡ b
2 onelon ⊢ A ∈ On ∧ b ∈ A → b ∈ On
3 2 adantrr ⊢ A ∈ On ∧ b ∈ A ∧ X ∈ M ⁡ b → b ∈ On
4 simprr ⊢ A ∈ On ∧ b ∈ A ∧ X ∈ M ⁡ b → X ∈ M ⁡ b
5 madebdayim ⊢ b ∈ On ∧ X ∈ M ⁡ b → bday ⁡ X ⊆ b
6 3 4 5 syl2anc ⊢ A ∈ On ∧ b ∈ A ∧ X ∈ M ⁡ b → bday ⁡ X ⊆ b
7 simprl ⊢ A ∈ On ∧ b ∈ A ∧ X ∈ M ⁡ b → b ∈ A
8 bdayelon ⊢ bday ⁡ X ∈ On
9 ontr2 ⊢ bday ⁡ X ∈ On ∧ A ∈ On → bday ⁡ X ⊆ b ∧ b ∈ A → bday ⁡ X ∈ A
10 8 9 mpan ⊢ A ∈ On → bday ⁡ X ⊆ b ∧ b ∈ A → bday ⁡ X ∈ A
11 10 adantr ⊢ A ∈ On ∧ b ∈ A ∧ X ∈ M ⁡ b → bday ⁡ X ⊆ b ∧ b ∈ A → bday ⁡ X ∈ A
12 6 7 11 mp2and ⊢ A ∈ On ∧ b ∈ A ∧ X ∈ M ⁡ b → bday ⁡ X ∈ A
13 12 rexlimdvaa ⊢ A ∈ On → ∃ b ∈ A X ∈ M ⁡ b → bday ⁡ X ∈ A
14 1 13 sylbid ⊢ A ∈ On → X ∈ Old ⁡ A → bday ⁡ X ∈ A
15 14 imp ⊢ A ∈ On ∧ X ∈ Old ⁡ A → bday ⁡ X ∈ A