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

Proof

Step	Hyp	Ref	Expression
1		elold	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( O ‘ 𝐴 ) ↔ ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) ) )
2		onelon	⊢ ( ( 𝐴 ∈ On ∧ 𝑏 ∈ 𝐴 ) → 𝑏 ∈ On )
3	2	adantrr	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑋 ∈ ( M ‘ 𝑏 ) ) ) → 𝑏 ∈ On )
4		simprr	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑋 ∈ ( M ‘ 𝑏 ) ) ) → 𝑋 ∈ ( M ‘ 𝑏 ) )
5		madebdayim	⊢ ( ( 𝑏 ∈ On ∧ 𝑋 ∈ ( M ‘ 𝑏 ) ) → ( bday ‘ 𝑋 ) ⊆ 𝑏 )
6	3 4 5	syl2anc	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑋 ∈ ( M ‘ 𝑏 ) ) ) → ( bday ‘ 𝑋 ) ⊆ 𝑏 )
7		simprl	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑋 ∈ ( M ‘ 𝑏 ) ) ) → 𝑏 ∈ 𝐴 )
8		bdayelon	⊢ ( bday ‘ 𝑋 ) ∈ On
9		ontr2	⊢ ( ( ( bday ‘ 𝑋 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( ( bday ‘ 𝑋 ) ⊆ 𝑏 ∧ 𝑏 ∈ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
10	8 9	mpan	⊢ ( 𝐴 ∈ On → ( ( ( bday ‘ 𝑋 ) ⊆ 𝑏 ∧ 𝑏 ∈ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
11	10	adantr	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑋 ∈ ( M ‘ 𝑏 ) ) ) → ( ( ( bday ‘ 𝑋 ) ⊆ 𝑏 ∧ 𝑏 ∈ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
12	6 7 11	mp2and	⊢ ( ( 𝐴 ∈ On ∧ ( 𝑏 ∈ 𝐴 ∧ 𝑋 ∈ ( M ‘ 𝑏 ) ) ) → ( bday ‘ 𝑋 ) ∈ 𝐴 )
13	12	rexlimdvaa	⊢ ( 𝐴 ∈ On → ( ∃ 𝑏 ∈ 𝐴 𝑋 ∈ ( M ‘ 𝑏 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
14	1 13	sylbid	⊢ ( 𝐴 ∈ On → ( 𝑋 ∈ ( O ‘ 𝐴 ) → ( bday ‘ 𝑋 ) ∈ 𝐴 ) )
15	14	imp	⊢ ( ( 𝐴 ∈ On ∧ 𝑋 ∈ ( O ‘ 𝐴 ) ) → ( bday ‘ 𝑋 ) ∈ 𝐴 )