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\in \mathrm{Old}\left(A\right)\to \mathrm{bday}\left(X\right)\in A$$

Proof

Step	Hyp	Ref	Expression
1		elfvdm	$$⊢X\in \mathrm{Old}\left(A\right)\to A\in \mathrm{dom}\mathrm{Old}$$
2		oldf	$$⊢\mathrm{Old}:\mathrm{On}⟶𝒫\mathrm{No}$$
3	2	fdmi	$$⊢\mathrm{dom}\mathrm{Old}=\mathrm{On}$$
4	1 3	eleqtrdi	$$⊢X\in \mathrm{Old}\left(A\right)\to A\in \mathrm{On}$$
5		elold	Could not format ( A e. On -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _Made ` b ) ) ) : No typesetting found for |- ( A e. On -> ( X e. ( _Old ` A ) <-> E. b e. A X e. ( _Made ` b ) ) ) with typecode |-
6		madebdayim	Could not format ( X e. ( _Made ` b ) -> ( bday ` X ) C_ b ) : No typesetting found for |- ( X e. ( _Made ` b ) -> ( bday ` X ) C_ b ) with typecode |-
7	6	ad2antll	Could not format ( ( A e. On /\ ( b e. A /\ X e. ( _Made ` b ) ) ) -> ( bday ` X ) C_ b ) : No typesetting found for |- ( ( A e. On /\ ( b e. A /\ X e. ( _Made ` b ) ) ) -> ( bday ` X ) C_ b ) with typecode |-
8		simprl	Could not format ( ( A e. On /\ ( b e. A /\ X e. ( _Made ` b ) ) ) -> b e. A ) : No typesetting found for |- ( ( A e. On /\ ( b e. A /\ X e. ( _Made ` b ) ) ) -> b e. A ) with typecode |-
9		bdayelon	$$⊢\mathrm{bday}\left(X\right)\in \mathrm{On}$$
10		ontr2	$$⊢\left(\mathrm{bday}\left(X\right)\in \mathrm{On}\wedge A\in \mathrm{On}\right)\to \left(\left(\mathrm{bday}\left(X\right)\subseteq b\wedge b\in A\right)\to \mathrm{bday}\left(X\right)\in A\right)$$
11	9 10	mpan	$$⊢A\in \mathrm{On}\to \left(\left(\mathrm{bday}\left(X\right)\subseteq b\wedge b\in A\right)\to \mathrm{bday}\left(X\right)\in A\right)$$
12	11	adantr	Could not format ( ( A e. On /\ ( b e. A /\ X e. ( _Made ` b ) ) ) -> ( ( ( bday ` X ) C_ b /\ b e. A ) -> ( bday ` X ) e. A ) ) : No typesetting found for |- ( ( A e. On /\ ( b e. A /\ X e. ( _Made ` b ) ) ) -> ( ( ( bday ` X ) C_ b /\ b e. A ) -> ( bday ` X ) e. A ) ) with typecode |-
13	7 8 12	mp2and	Could not format ( ( A e. On /\ ( b e. A /\ X e. ( _Made ` b ) ) ) -> ( bday ` X ) e. A ) : No typesetting found for |- ( ( A e. On /\ ( b e. A /\ X e. ( _Made ` b ) ) ) -> ( bday ` X ) e. A ) with typecode |-
14	13	rexlimdvaa	Could not format ( A e. On -> ( E. b e. A X e. ( _Made ` b ) -> ( bday ` X ) e. A ) ) : No typesetting found for |- ( A e. On -> ( E. b e. A X e. ( _Made ` b ) -> ( bday ` X ) e. A ) ) with typecode |-
15	5 14	sylbid	$$⊢A\in \mathrm{On}\to \left(X\in \mathrm{Old}\left(A\right)\to \mathrm{bday}\left(X\right)\in A\right)$$
16	4 15	mpcom	$$⊢X\in \mathrm{Old}\left(A\right)\to \mathrm{bday}\left(X\right)\in A$$