Theorem madebdayim

Description: If a surreal is a member of a made set, its birthday is less than or equal to the level. (Contributed by Scott Fenton, 10-Aug-2024)

	Ref	Expression
Assertion	madebdayim	Could not format assertion : No typesetting found for |- ( X e. ( _Made ` A ) -> ( bday ` X ) C_ A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		elfvdm	Could not format ( X e. ( _Made ` A ) -> A e. dom _Made ) : No typesetting found for |- ( X e. ( _Made ` A ) -> A e. dom _Made ) with typecode |-
2		madef	Could not format _Made : On --> ~P No : No typesetting found for |- _Made : On --> ~P No with typecode |-
3	2	fdmi	Could not format dom _Made = On : No typesetting found for |- dom _Made = On with typecode |-
4	1 3	eleqtrdi	Could not format ( X e. ( _Made ` A ) -> A e. On ) : No typesetting found for |- ( X e. ( _Made ` A ) -> A e. On ) with typecode |-
5		fveq2	Could not format ( a = b -> ( _Made ` a ) = ( _Made ` b ) ) : No typesetting found for |- ( a = b -> ( _Made ` a ) = ( _Made ` b ) ) with typecode |-
6		sseq2	$$⊢a=b\to \left(\mathrm{bday}\left(x\right)\subseteq a\leftrightarrow \mathrm{bday}\left(x\right)\subseteq b\right)$$
7	5 6	raleqbidv	Could not format ( a = b -> ( A. x e. ( _Made ` a ) ( bday ` x ) C_ a <-> A. x e. ( _Made ` b ) ( bday ` x ) C_ b ) ) : No typesetting found for |- ( a = b -> ( A. x e. ( _Made ` a ) ( bday ` x ) C_ a <-> A. x e. ( _Made ` b ) ( bday ` x ) C_ b ) ) with typecode |-
8		fveq2	$$⊢x=y\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(y\right)$$
9	8	sseq1d	$$⊢x=y\to \left(\mathrm{bday}\left(x\right)\subseteq b\leftrightarrow \mathrm{bday}\left(y\right)\subseteq b\right)$$
10	9	cbvralvw	Could not format ( A. x e. ( _Made ` b ) ( bday ` x ) C_ b <-> A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) : No typesetting found for |- ( A. x e. ( _Made ` b ) ( bday ` x ) C_ b <-> A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) with typecode |-
11	7 10	bitrdi	Could not format ( a = b -> ( A. x e. ( _Made ` a ) ( bday ` x ) C_ a <-> A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) ) : No typesetting found for |- ( a = b -> ( A. x e. ( _Made ` a ) ( bday ` x ) C_ a <-> A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) ) with typecode |-
12		fveq2	Could not format ( a = A -> ( _Made ` a ) = ( _Made ` A ) ) : No typesetting found for |- ( a = A -> ( _Made ` a ) = ( _Made ` A ) ) with typecode |-
13		sseq2	$$⊢a=A\to \left(\mathrm{bday}\left(x\right)\subseteq a\leftrightarrow \mathrm{bday}\left(x\right)\subseteq A\right)$$
14	12 13	raleqbidv	Could not format ( a = A -> ( A. x e. ( _Made ` a ) ( bday ` x ) C_ a <-> A. x e. ( _Made ` A ) ( bday ` x ) C_ A ) ) : No typesetting found for |- ( a = A -> ( A. x e. ( _Made ` a ) ( bday ` x ) C_ a <-> A. x e. ( _Made ` A ) ( bday ` x ) C_ A ) ) with typecode |-
15		elmade2	Could not format ( a e. On -> ( x e. ( _Made ` a ) <-> E. l e. ~P ( _Old ` a ) E. r e. ~P ( _Old ` a ) ( l < ( x e. ( _Made ` a ) <-> E. l e. ~P ( _Old ` a ) E. r e. ~P ( _Old ` a ) ( l <
16	15	adantr	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( x e. ( _Made ` a ) <-> E. l e. ~P ( _Old ` a ) E. r e. ~P ( _Old ` a ) ( l < ( x e. ( _Made ` a ) <-> E. l e. ~P ( _Old ` a ) E. r e. ~P ( _Old ` a ) ( l <
17		elpwi	$$⊢l\in 𝒫\mathrm{Old}\left(a\right)\to l\subseteq \mathrm{Old}\left(a\right)$$
18		elpwi	$$⊢r\in 𝒫\mathrm{Old}\left(a\right)\to r\subseteq \mathrm{Old}\left(a\right)$$
19	17 18	anim12i	$$⊢\left(l\in 𝒫\mathrm{Old}\left(a\right)\wedge r\in 𝒫\mathrm{Old}\left(a\right)\right)\to \left(l\subseteq \mathrm{Old}\left(a\right)\wedge r\subseteq \mathrm{Old}\left(a\right)\right)$$
20		unss	$$⊢\left(l\subseteq \mathrm{Old}\left(a\right)\wedge r\subseteq \mathrm{Old}\left(a\right)\right)\leftrightarrow l\cup r\subseteq \mathrm{Old}\left(a\right)$$
21	19 20	sylib	$$⊢\left(l\in 𝒫\mathrm{Old}\left(a\right)\wedge r\in 𝒫\mathrm{Old}\left(a\right)\right)\to l\cup r\subseteq \mathrm{Old}\left(a\right)$$
22		simpr	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < l < l <
23		simplll	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < a e. On ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < a e. On ) with typecode |-
24		dfss3	$$⊢l\cup r\subseteq \mathrm{Old}\left(a\right)\leftrightarrow \forall z\in \left(l\cup r\right)z\in \mathrm{Old}\left(a\right)$$
25		fveq2	$$⊢y=z\to \mathrm{bday}\left(y\right)=\mathrm{bday}\left(z\right)$$
26	25	sseq1d	$$⊢y=z\to \left(\mathrm{bday}\left(y\right)\subseteq b\leftrightarrow \mathrm{bday}\left(z\right)\subseteq b\right)$$
27	26	rspccv	Could not format ( A. y e. ( _Made ` b ) ( bday ` y ) C_ b -> ( z e. ( _Made ` b ) -> ( bday ` z ) C_ b ) ) : No typesetting found for |- ( A. y e. ( _Made ` b ) ( bday ` y ) C_ b -> ( z e. ( _Made ` b ) -> ( bday ` z ) C_ b ) ) with typecode |-
28	27	ralimi	Could not format ( A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b -> A. b e. a ( z e. ( _Made ` b ) -> ( bday ` z ) C_ b ) ) : No typesetting found for |- ( A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b -> A. b e. a ( z e. ( _Made ` b ) -> ( bday ` z ) C_ b ) ) with typecode |-
29		rexim	Could not format ( A. b e. a ( z e. ( _Made ` b ) -> ( bday ` z ) C_ b ) -> ( E. b e. a z e. ( _Made ` b ) -> E. b e. a ( bday ` z ) C_ b ) ) : No typesetting found for |- ( A. b e. a ( z e. ( _Made ` b ) -> ( bday ` z ) C_ b ) -> ( E. b e. a z e. ( _Made ` b ) -> E. b e. a ( bday ` z ) C_ b ) ) with typecode |-
30	28 29	syl	Could not format ( A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b -> ( E. b e. a z e. ( _Made ` b ) -> E. b e. a ( bday ` z ) C_ b ) ) : No typesetting found for |- ( A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b -> ( E. b e. a z e. ( _Made ` b ) -> E. b e. a ( bday ` z ) C_ b ) ) with typecode |-
31	30	adantl	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( E. b e. a z e. ( _Made ` b ) -> E. b e. a ( bday ` z ) C_ b ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( E. b e. a z e. ( _Made ` b ) -> E. b e. a ( bday ` z ) C_ b ) ) with typecode |-
32		elold	Could not format ( a e. On -> ( z e. ( _Old ` a ) <-> E. b e. a z e. ( _Made ` b ) ) ) : No typesetting found for |- ( a e. On -> ( z e. ( _Old ` a ) <-> E. b e. a z e. ( _Made ` b ) ) ) with typecode |-
33	32	adantr	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( z e. ( _Old ` a ) <-> E. b e. a z e. ( _Made ` b ) ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( z e. ( _Old ` a ) <-> E. b e. a z e. ( _Made ` b ) ) ) with typecode |-
34		bdayelon	$$⊢\mathrm{bday}\left(z\right)\in \mathrm{On}$$
35		onelssex	$$⊢\left(\mathrm{bday}\left(z\right)\in \mathrm{On}\wedge a\in \mathrm{On}\right)\to \left(\mathrm{bday}\left(z\right)\in a\leftrightarrow \exists b\in a\mathrm{bday}\left(z\right)\subseteq b\right)$$
36	34 35	mpan	$$⊢a\in \mathrm{On}\to \left(\mathrm{bday}\left(z\right)\in a\leftrightarrow \exists b\in a\mathrm{bday}\left(z\right)\subseteq b\right)$$
37	36	adantr	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( ( bday ` z ) e. a <-> E. b e. a ( bday ` z ) C_ b ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( ( bday ` z ) e. a <-> E. b e. a ( bday ` z ) C_ b ) ) with typecode |-
38	31 33 37	3imtr4d	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( z e. ( _Old ` a ) -> ( bday ` z ) e. a ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( z e. ( _Old ` a ) -> ( bday ` z ) e. a ) ) with typecode |-
39	38	ralimdv	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( A. z e. ( l u. r ) z e. ( _Old ` a ) -> A. z e. ( l u. r ) ( bday ` z ) e. a ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( A. z e. ( l u. r ) z e. ( _Old ` a ) -> A. z e. ( l u. r ) ( bday ` z ) e. a ) ) with typecode |-
40	24 39	biimtrid	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( ( l u. r ) C_ ( _Old ` a ) -> A. z e. ( l u. r ) ( bday ` z ) e. a ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( ( l u. r ) C_ ( _Old ` a ) -> A. z e. ( l u. r ) ( bday ` z ) e. a ) ) with typecode |-
41	40	imp	Could not format ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) -> A. z e. ( l u. r ) ( bday ` z ) e. a ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) -> A. z e. ( l u. r ) ( bday ` z ) e. a ) with typecode |-
42	41	adantr	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < A. z e. ( l u. r ) ( bday ` z ) e. a ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < A. z e. ( l u. r ) ( bday ` z ) e. a ) with typecode |-
43		bdayfun	$$⊢\mathrm{Fun}\mathrm{bday}$$
44		oldssno	$$⊢\mathrm{Old}\left(a\right)\subseteq \mathrm{No}$$
45		sstr	$$⊢\left(l\cup r\subseteq \mathrm{Old}\left(a\right)\wedge \mathrm{Old}\left(a\right)\subseteq \mathrm{No}\right)\to l\cup r\subseteq \mathrm{No}$$
46	44 45	mpan2	$$⊢l\cup r\subseteq \mathrm{Old}\left(a\right)\to l\cup r\subseteq \mathrm{No}$$
47		bdaydm	$$⊢\mathrm{dom}\mathrm{bday}=\mathrm{No}$$
48	46 47	sseqtrrdi	$$⊢l\cup r\subseteq \mathrm{Old}\left(a\right)\to l\cup r\subseteq \mathrm{dom}\mathrm{bday}$$
49		funimass4	$$⊢\left(\mathrm{Fun}\mathrm{bday}\wedge l\cup r\subseteq \mathrm{dom}\mathrm{bday}\right)\to \left(\mathrm{bday}\left[l\cup r\right]\subseteq a\leftrightarrow \forall z\in \left(l\cup r\right)\mathrm{bday}\left(z\right)\in a\right)$$
50	43 48 49	sylancr	$$⊢l\cup r\subseteq \mathrm{Old}\left(a\right)\to \left(\mathrm{bday}\left[l\cup r\right]\subseteq a\leftrightarrow \forall z\in \left(l\cup r\right)\mathrm{bday}\left(z\right)\in a\right)$$
51	50	adantl	Could not format ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) -> ( ( bday " ( l u. r ) ) C_ a <-> A. z e. ( l u. r ) ( bday ` z ) e. a ) ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) -> ( ( bday " ( l u. r ) ) C_ a <-> A. z e. ( l u. r ) ( bday ` z ) e. a ) ) with typecode |-
52	51	adantr	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( ( bday " ( l u. r ) ) C_ a <-> A. z e. ( l u. r ) ( bday ` z ) e. a ) ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( ( bday " ( l u. r ) ) C_ a <-> A. z e. ( l u. r ) ( bday ` z ) e. a ) ) with typecode |-
53	42 52	mpbird	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( bday " ( l u. r ) ) C_ a ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( bday " ( l u. r ) ) C_ a ) with typecode |-
54		scutbdaybnd	$$⊢\left(l{\ll }_{s}r\wedge a\in \mathrm{On}\wedge \mathrm{bday}\left[l\cup r\right]\subseteq a\right)\to \mathrm{bday}\left(l{|}_{s}r\right)\subseteq a$$
55	22 23 53 54	syl3anc	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( bday ` ( l |s r ) ) C_ a ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( bday ` ( l |s r ) ) C_ a ) with typecode |-
56		fveq2	$$⊢l{|}_{s}r=x\to \mathrm{bday}\left(l{|}_{s}r\right)=\mathrm{bday}\left(x\right)$$
57	56	sseq1d	$$⊢l{|}_{s}r=x\to \left(\mathrm{bday}\left(l{|}_{s}r\right)\subseteq a\leftrightarrow \mathrm{bday}\left(x\right)\subseteq a\right)$$
58	55 57	syl5ibcom	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( ( l |s r ) = x -> ( bday ` x ) C_ a ) ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) /\ l < ( ( l |s r ) = x -> ( bday ` x ) C_ a ) ) with typecode |-
59	58	expimpd	Could not format ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) -> ( ( l < ( bday ` x ) C_ a ) ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) /\ ( l u. r ) C_ ( _Old ` a ) ) -> ( ( l < ( bday ` x ) C_ a ) ) with typecode |-
60	59	ex	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( ( l u. r ) C_ ( _Old ` a ) -> ( ( l < ( bday ` x ) C_ a ) ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( ( l u. r ) C_ ( _Old ` a ) -> ( ( l < ( bday ` x ) C_ a ) ) ) with typecode |-
61	21 60	syl5	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( ( l e. ~P ( _Old ` a ) /\ r e. ~P ( _Old ` a ) ) -> ( ( l < ( bday ` x ) C_ a ) ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( ( l e. ~P ( _Old ` a ) /\ r e. ~P ( _Old ` a ) ) -> ( ( l < ( bday ` x ) C_ a ) ) ) with typecode |-
62	61	rexlimdvv	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( E. l e. ~P ( _Old ` a ) E. r e. ~P ( _Old ` a ) ( l < ( bday ` x ) C_ a ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( E. l e. ~P ( _Old ` a ) E. r e. ~P ( _Old ` a ) ( l < ( bday ` x ) C_ a ) ) with typecode |-
63	16 62	sylbid	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( x e. ( _Made ` a ) -> ( bday ` x ) C_ a ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> ( x e. ( _Made ` a ) -> ( bday ` x ) C_ a ) ) with typecode |-
64	63	ralrimiv	Could not format ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> A. x e. ( _Made ` a ) ( bday ` x ) C_ a ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b ) -> A. x e. ( _Made ` a ) ( bday ` x ) C_ a ) with typecode |-
65	64	ex	Could not format ( a e. On -> ( A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b -> A. x e. ( _Made ` a ) ( bday ` x ) C_ a ) ) : No typesetting found for |- ( a e. On -> ( A. b e. a A. y e. ( _Made ` b ) ( bday ` y ) C_ b -> A. x e. ( _Made ` a ) ( bday ` x ) C_ a ) ) with typecode |-
66	11 14 65	tfis3	Could not format ( A e. On -> A. x e. ( _Made ` A ) ( bday ` x ) C_ A ) : No typesetting found for |- ( A e. On -> A. x e. ( _Made ` A ) ( bday ` x ) C_ A ) with typecode |-
67		fveq2	$$⊢x=X\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(X\right)$$
68	67	sseq1d	$$⊢x=X\to \left(\mathrm{bday}\left(x\right)\subseteq A\leftrightarrow \mathrm{bday}\left(X\right)\subseteq A\right)$$
69	68	rspccv	Could not format ( A. x e. ( _Made ` A ) ( bday ` x ) C_ A -> ( X e. ( _Made ` A ) -> ( bday ` X ) C_ A ) ) : No typesetting found for |- ( A. x e. ( _Made ` A ) ( bday ` x ) C_ A -> ( X e. ( _Made ` A ) -> ( bday ` X ) C_ A ) ) with typecode |-
70	66 69	syl	Could not format ( A e. On -> ( X e. ( _Made ` A ) -> ( bday ` X ) C_ A ) ) : No typesetting found for |- ( A e. On -> ( X e. ( _Made ` A ) -> ( bday ` X ) C_ A ) ) with typecode |-
71	4 70	mpcom	Could not format ( X e. ( _Made ` A ) -> ( bday ` X ) C_ A ) : No typesetting found for |- ( X e. ( _Made ` A ) -> ( bday ` X ) C_ A ) with typecode |-