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

Proof

Step	Hyp	Ref	Expression
1		elfvdm	|- ( X e. ( _Old ` A ) -> A e. dom _Old )
2		oldf	|- _Old : On --> ~P No
3	2	fdmi	|- dom _Old = On
4	1 3	eleqtrdi	|- ( X e. ( _Old ` A ) -> A e. On )
5		elold	|- ( A e. On -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _M ` b ) ) )
6		madebdayim	|- ( X e. ( _M ` b ) -> ( bday ` X ) C_ b )
7	6	ad2antll	|- ( ( A e. On /\ ( b e. A /\ X e. ( _M ` b ) ) ) -> ( bday ` X ) C_ b )
8		simprl	|- ( ( A e. On /\ ( b e. A /\ X e. ( _M ` b ) ) ) -> b e. A )
9		bdayelon	|- ( bday ` X ) e. On
10		ontr2	|- ( ( ( bday ` X ) e. On /\ A e. On ) -> ( ( ( bday ` X ) C_ b /\ b e. A ) -> ( bday ` X ) e. A ) )
11	9 10	mpan	|- ( A e. On -> ( ( ( bday ` X ) C_ b /\ b e. A ) -> ( bday ` X ) e. A ) )
12	11	adantr	|- ( ( A e. On /\ ( b e. A /\ X e. ( _M ` b ) ) ) -> ( ( ( bday ` X ) C_ b /\ b e. A ) -> ( bday ` X ) e. A ) )
13	7 8 12	mp2and	|- ( ( A e. On /\ ( b e. A /\ X e. ( _M ` b ) ) ) -> ( bday ` X ) e. A )
14	13	rexlimdvaa	|- ( A e. On -> ( E. b e. A X e. ( _M ` b ) -> ( bday ` X ) e. A ) )
15	5 14	sylbid	|- ( A e. On -> ( X e. ( _Old ` A ) -> ( bday ` X ) e. A ) )
16	4 15	mpcom	|- ( X e. ( _Old ` A ) -> ( bday ` X ) e. A )