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	⊢ ( 𝑋 ∈ ( O ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		elfvdm	⊢ ( 𝑋 ∈ ( O ‘ 𝐴 ) → 𝐴 ∈ dom O )
2		oldf	⊢ O : On ⟶ 𝒫 No
3	2	fdmi	⊢ dom O = On
4	1 3	eleqtrdi	⊢ ( 𝑋 ∈ ( O ‘ 𝐴 ) → 𝐴 ∈ On )
5		elold	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ) )
6		madebdayim	⊢ ( 𝑋 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑋 ) ⊆ 𝑏 )
7	6	ad2antll	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑋 ∈ ( M ‘ 𝑏 ) ) ) → ( bday ‘ 𝑋 ) ⊆ 𝑏 )
8		simprl	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑋 ∈ ( M ‘ 𝑏 ) ) ) → 𝑏 ∈ 𝐴 )
9		bdayelon	⊢ ( bday ‘ 𝑋 ) ∈ On
10		ontr2	⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( ( bday ‘ 𝑋 ) ⊆ 𝑏 ∧ 𝑏 ∈ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
11	9 10	mpan	⊢ ( 𝐴 ∈ On → ( ( ( bday ‘ 𝑋 ) ⊆ 𝑏 ∧ 𝑏 ∈ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
12	11	adantr	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑋 ∈ ( M ‘ 𝑏 ) ) ) → ( ( ( bday ‘ 𝑋 ) ⊆ 𝑏 ∧ 𝑏 ∈ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
13	7 8 12	mp2and	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑋 ∈ ( M ‘ 𝑏 ) ) ) → ( bday ‘ 𝑋 ) ∈ 𝐴 )
14	13	rexlimdvaa	⊢ ( 𝐴 ∈ On → ( ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
15	5 14	sylbid	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( O ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
16	4 15	mpcom	⊢ ( 𝑋 ∈ ( O ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 )