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 e. On /\ X e. ( _Old ` A ) ) -> ( bday ` X ) e. A )

Proof

Step	Hyp	Ref	Expression
1		elold	|- ( A e. On -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _M ` b ) ) )
2		onelon	|- ( ( A e. On /\ b e. A ) -> b e. On )
3	2	adantrr	|- ( ( A e. On /\ ( b e. A /\ X e. ( _M ` b ) ) ) -> b e. On )
4		simprr	|- ( ( A e. On /\ ( b e. A /\ X e. ( _M ` b ) ) ) -> X e. ( _M ` b ) )
5		madebdayim	|- ( ( b e. On /\ X e. ( _M ` b ) ) -> ( bday ` X ) C_ b )
6	3 4 5	syl2anc	|- ( ( A e. On /\ ( b e. A /\ X e. ( _M ` b ) ) ) -> ( bday ` X ) C_ b )
7		simprl	|- ( ( A e. On /\ ( b e. A /\ X e. ( _M ` b ) ) ) -> b e. A )
8		bdayelon	|- ( bday ` X ) e. On
9		ontr2	|- ( ( ( bday ` X ) e. On /\ A e. On ) -> ( ( ( bday ` X ) C_ b /\ b e. A ) -> ( bday ` X ) e. A ) )
10	8 9	mpan	|- ( A e. On -> ( ( ( bday ` X ) C_ b /\ b e. A ) -> ( bday ` X ) e. A ) )
11	10	adantr	|- ( ( A e. On /\ ( b e. A /\ X e. ( _M ` b ) ) ) -> ( ( ( bday ` X ) C_ b /\ b e. A ) -> ( bday ` X ) e. A ) )
12	6 7 11	mp2and	|- ( ( A e. On /\ ( b e. A /\ X e. ( _M ` b ) ) ) -> ( bday ` X ) e. A )
13	12	rexlimdvaa	|- ( A e. On -> ( E. b e. A X e. ( _M ` b ) -> ( bday ` X ) e. A ) )
14	1 13	sylbid	|- ( A e. On -> ( X e. ( _Old ` A ) -> ( bday ` X ) e. A ) )
15	14	imp	|- ( ( A e. On /\ X e. ( _Old ` A ) ) -> ( bday ` X ) e. A )