Theorem madebday

Description: A surreal is part of the set made by ordinal A iff its birthday is less than or equal to A . Remark in Conway p. 29. (Contributed by Scott Fenton, 19-Aug-2024)

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

Proof

Step	Hyp	Ref	Expression
1		madebdayim	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 |-
2		sseq2	$$⊢a=b\to \left(\mathrm{bday}\left(x\right)\subseteq a\leftrightarrow \mathrm{bday}\left(x\right)\subseteq b\right)$$
3		fveq2	Could not format ( a = b -> ( _Made ` a ) = ( _Made ` b ) ) : No typesetting found for |- ( a = b -> ( _Made ` a ) = ( _Made ` b ) ) with typecode |-
4	3	eleq2d	Could not format ( a = b -> ( x e. ( _Made ` a ) <-> x e. ( _Made ` b ) ) ) : No typesetting found for |- ( a = b -> ( x e. ( _Made ` a ) <-> x e. ( _Made ` b ) ) ) with typecode |-
5	2 4	imbi12d	Could not format ( a = b -> ( ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> ( ( bday ` x ) C_ b -> x e. ( _Made ` b ) ) ) ) : No typesetting found for |- ( a = b -> ( ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> ( ( bday ` x ) C_ b -> x e. ( _Made ` b ) ) ) ) with typecode |-
6	5	ralbidv	Could not format ( a = b -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> A. x e. No ( ( bday ` x ) C_ b -> x e. ( _Made ` b ) ) ) ) : No typesetting found for |- ( a = b -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> A. x e. No ( ( bday ` x ) C_ b -> x e. ( _Made ` b ) ) ) ) with typecode |-
7		fveq2	$$⊢x=y\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(y\right)$$
8	7	sseq1d	$$⊢x=y\to \left(\mathrm{bday}\left(x\right)\subseteq b\leftrightarrow \mathrm{bday}\left(y\right)\subseteq b\right)$$
9		eleq1	Could not format ( x = y -> ( x e. ( _Made ` b ) <-> y e. ( _Made ` b ) ) ) : No typesetting found for |- ( x = y -> ( x e. ( _Made ` b ) <-> y e. ( _Made ` b ) ) ) with typecode |-
10	8 9	imbi12d	Could not format ( x = y -> ( ( ( bday ` x ) C_ b -> x e. ( _Made ` b ) ) <-> ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) ) : No typesetting found for |- ( x = y -> ( ( ( bday ` x ) C_ b -> x e. ( _Made ` b ) ) <-> ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) ) with typecode |-
11	10	cbvralvw	Could not format ( A. x e. No ( ( bday ` x ) C_ b -> x e. ( _Made ` b ) ) <-> A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) : No typesetting found for |- ( A. x e. No ( ( bday ` x ) C_ b -> x e. ( _Made ` b ) ) <-> A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) with typecode |-
12	6 11	bitrdi	Could not format ( a = b -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) ) : No typesetting found for |- ( a = b -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) ) 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		fveq2	Could not format ( a = A -> ( _Made ` a ) = ( _Made ` A ) ) : No typesetting found for |- ( a = A -> ( _Made ` a ) = ( _Made ` A ) ) with typecode |-
15	14	eleq2d	Could not format ( a = A -> ( x e. ( _Made ` a ) <-> x e. ( _Made ` A ) ) ) : No typesetting found for |- ( a = A -> ( x e. ( _Made ` a ) <-> x e. ( _Made ` A ) ) ) with typecode |-
16	13 15	imbi12d	Could not format ( a = A -> ( ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) ) ) : No typesetting found for |- ( a = A -> ( ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) ) ) with typecode |-
17	16	ralbidv	Could not format ( a = A -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> A. x e. No ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) ) ) : No typesetting found for |- ( a = A -> ( A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) <-> A. x e. No ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) ) ) with typecode |-
18		bdayelon	$$⊢\mathrm{bday}\left(x\right)\in \mathrm{On}$$
19		onsseleq	$$⊢\left(\mathrm{bday}\left(x\right)\in \mathrm{On}\wedge a\in \mathrm{On}\right)\to \left(\mathrm{bday}\left(x\right)\subseteq a\leftrightarrow \left(\mathrm{bday}\left(x\right)\in a\vee \mathrm{bday}\left(x\right)=a\right)\right)$$
20	18 19	mpan	$$⊢a\in \mathrm{On}\to \left(\mathrm{bday}\left(x\right)\subseteq a\leftrightarrow \left(\mathrm{bday}\left(x\right)\in a\vee \mathrm{bday}\left(x\right)=a\right)\right)$$
21	20	ad2antrr	Could not format ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) C_ a <-> ( ( bday ` x ) e. a \/ ( bday ` x ) = a ) ) ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) C_ a <-> ( ( bday ` x ) e. a \/ ( bday ` x ) = a ) ) ) with typecode |-
22		simpll	Could not format ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> a e. On ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> a e. On ) with typecode |-
23		onelss	$$⊢a\in \mathrm{On}\to \left(\mathrm{bday}\left(x\right)\in a\to \mathrm{bday}\left(x\right)\subseteq a\right)$$
24	23	ad2antrr	Could not format ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) e. a -> ( bday ` x ) C_ a ) ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) e. a -> ( bday ` x ) C_ a ) ) with typecode |-
25	24	imp	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( bday ` x ) C_ a ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( bday ` x ) C_ a ) with typecode |-
26		madess	Could not format ( ( a e. On /\ ( bday ` x ) C_ a ) -> ( _Made ` ( bday ` x ) ) C_ ( _Made ` a ) ) : No typesetting found for |- ( ( a e. On /\ ( bday ` x ) C_ a ) -> ( _Made ` ( bday ` x ) ) C_ ( _Made ` a ) ) with typecode |-
27	22 25 26	syl2an2r	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( _Made ` ( bday ` x ) ) C_ ( _Made ` a ) ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( _Made ` ( bday ` x ) ) C_ ( _Made ` a ) ) with typecode |-
28		ssid	$$⊢\mathrm{bday}\left(x\right)\subseteq \mathrm{bday}\left(x\right)$$
29		simpr	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( bday ` x ) e. a ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( bday ` x ) e. a ) with typecode |-
30		simplr	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> x e. No ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> x e. No ) with typecode |-
31	29 30	jca	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( ( bday ` x ) e. a /\ x e. No ) ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( ( bday ` x ) e. a /\ x e. No ) ) with typecode |-
32		simpllr	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) with typecode |-
33		sseq2	$$⊢b=\mathrm{bday}\left(x\right)\to \left(\mathrm{bday}\left(y\right)\subseteq b\leftrightarrow \mathrm{bday}\left(y\right)\subseteq \mathrm{bday}\left(x\right)\right)$$
34		fveq2	Could not format ( b = ( bday ` x ) -> ( _Made ` b ) = ( _Made ` ( bday ` x ) ) ) : No typesetting found for |- ( b = ( bday ` x ) -> ( _Made ` b ) = ( _Made ` ( bday ` x ) ) ) with typecode |-
35	34	eleq2d	Could not format ( b = ( bday ` x ) -> ( y e. ( _Made ` b ) <-> y e. ( _Made ` ( bday ` x ) ) ) ) : No typesetting found for |- ( b = ( bday ` x ) -> ( y e. ( _Made ` b ) <-> y e. ( _Made ` ( bday ` x ) ) ) ) with typecode |-
36	33 35	imbi12d	Could not format ( b = ( bday ` x ) -> ( ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) <-> ( ( bday ` y ) C_ ( bday ` x ) -> y e. ( _Made ` ( bday ` x ) ) ) ) ) : No typesetting found for |- ( b = ( bday ` x ) -> ( ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) <-> ( ( bday ` y ) C_ ( bday ` x ) -> y e. ( _Made ` ( bday ` x ) ) ) ) ) with typecode |-
37		fveq2	$$⊢y=x\to \mathrm{bday}\left(y\right)=\mathrm{bday}\left(x\right)$$
38	37	sseq1d	$$⊢y=x\to \left(\mathrm{bday}\left(y\right)\subseteq \mathrm{bday}\left(x\right)\leftrightarrow \mathrm{bday}\left(x\right)\subseteq \mathrm{bday}\left(x\right)\right)$$
39		eleq1	Could not format ( y = x -> ( y e. ( _Made ` ( bday ` x ) ) <-> x e. ( _Made ` ( bday ` x ) ) ) ) : No typesetting found for |- ( y = x -> ( y e. ( _Made ` ( bday ` x ) ) <-> x e. ( _Made ` ( bday ` x ) ) ) ) with typecode |-
40	38 39	imbi12d	Could not format ( y = x -> ( ( ( bday ` y ) C_ ( bday ` x ) -> y e. ( _Made ` ( bday ` x ) ) ) <-> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _Made ` ( bday ` x ) ) ) ) ) : No typesetting found for |- ( y = x -> ( ( ( bday ` y ) C_ ( bday ` x ) -> y e. ( _Made ` ( bday ` x ) ) ) <-> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _Made ` ( bday ` x ) ) ) ) ) with typecode |-
41	36 40	rspc2v	Could not format ( ( ( bday ` x ) e. a /\ x e. No ) -> ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) -> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _Made ` ( bday ` x ) ) ) ) ) : No typesetting found for |- ( ( ( bday ` x ) e. a /\ x e. No ) -> ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) -> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _Made ` ( bday ` x ) ) ) ) ) with typecode |-
42	31 32 41	sylc	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _Made ` ( bday ` x ) ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> ( ( bday ` x ) C_ ( bday ` x ) -> x e. ( _Made ` ( bday ` x ) ) ) ) with typecode |-
43	28 42	mpi	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> x e. ( _Made ` ( bday ` x ) ) ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> x e. ( _Made ` ( bday ` x ) ) ) with typecode |-
44	27 43	sseldd	Could not format ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> x e. ( _Made ` a ) ) : No typesetting found for |- ( ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) /\ ( bday ` x ) e. a ) -> x e. ( _Made ` a ) ) with typecode |-
45	44	ex	Could not format ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) e. a -> x e. ( _Made ` a ) ) ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) e. a -> x e. ( _Made ` a ) ) ) with typecode |-
46		madebdaylemlrcut	Could not format ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) : No typesetting found for |- ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) = x ) with typecode |-
47	18	a1i	$$⊢x\in \mathrm{No}\to \mathrm{bday}\left(x\right)\in \mathrm{On}$$
48		lltropt	Could not format ( _Left ` x ) <
49	48	a1i	Could not format ( x e. No -> ( _Left ` x ) < ( _Left ` x ) <
50		leftssold	Could not format ( _Left ` x ) C_ ( _Old ` ( bday ` x ) ) : No typesetting found for |- ( _Left ` x ) C_ ( _Old ` ( bday ` x ) ) with typecode |-
51	50	a1i	Could not format ( x e. No -> ( _Left ` x ) C_ ( _Old ` ( bday ` x ) ) ) : No typesetting found for |- ( x e. No -> ( _Left ` x ) C_ ( _Old ` ( bday ` x ) ) ) with typecode |-
52		rightssold	Could not format ( _Right ` x ) C_ ( _Old ` ( bday ` x ) ) : No typesetting found for |- ( _Right ` x ) C_ ( _Old ` ( bday ` x ) ) with typecode |-
53	52	a1i	Could not format ( x e. No -> ( _Right ` x ) C_ ( _Old ` ( bday ` x ) ) ) : No typesetting found for |- ( x e. No -> ( _Right ` x ) C_ ( _Old ` ( bday ` x ) ) ) with typecode |-
54		madecut	Could not format ( ( ( ( bday ` x ) e. On /\ ( _Left ` x ) < ( ( _Left ` x ) |s ( _Right ` x ) ) e. ( _Made ` ( bday ` x ) ) ) : No typesetting found for |- ( ( ( ( bday ` x ) e. On /\ ( _Left ` x ) < ( ( _Left ` x ) |s ( _Right ` x ) ) e. ( _Made ` ( bday ` x ) ) ) with typecode |-
55	47 49 51 53 54	syl22anc	Could not format ( x e. No -> ( ( _Left ` x ) |s ( _Right ` x ) ) e. ( _Made ` ( bday ` x ) ) ) : No typesetting found for |- ( x e. No -> ( ( _Left ` x ) |s ( _Right ` x ) ) e. ( _Made ` ( bday ` x ) ) ) with typecode |-
56	55	adantl	Could not format ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) e. ( _Made ` ( bday ` x ) ) ) : No typesetting found for |- ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> ( ( _Left ` x ) |s ( _Right ` x ) ) e. ( _Made ` ( bday ` x ) ) ) with typecode |-
57	46 56	eqeltrrd	Could not format ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` ( bday ` x ) ) ) : No typesetting found for |- ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` ( bday ` x ) ) ) with typecode |-
58		raleq	Could not format ( ( bday ` x ) = a -> ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) <-> A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) ) : No typesetting found for |- ( ( bday ` x ) = a -> ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) <-> A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) ) with typecode |-
59	58	anbi1d	Could not format ( ( bday ` x ) = a -> ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) <-> ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) ) ) : No typesetting found for |- ( ( bday ` x ) = a -> ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) <-> ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) ) ) with typecode |-
60		fveq2	Could not format ( ( bday ` x ) = a -> ( _Made ` ( bday ` x ) ) = ( _Made ` a ) ) : No typesetting found for |- ( ( bday ` x ) = a -> ( _Made ` ( bday ` x ) ) = ( _Made ` a ) ) with typecode |-
61	60	eleq2d	Could not format ( ( bday ` x ) = a -> ( x e. ( _Made ` ( bday ` x ) ) <-> x e. ( _Made ` a ) ) ) : No typesetting found for |- ( ( bday ` x ) = a -> ( x e. ( _Made ` ( bday ` x ) ) <-> x e. ( _Made ` a ) ) ) with typecode |-
62	59 61	imbi12d	Could not format ( ( bday ` x ) = a -> ( ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` ( bday ` x ) ) ) <-> ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` a ) ) ) ) : No typesetting found for |- ( ( bday ` x ) = a -> ( ( ( A. b e. ( bday ` x ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` ( bday ` x ) ) ) <-> ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` a ) ) ) ) with typecode |-
63	57 62	mpbii	Could not format ( ( bday ` x ) = a -> ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` a ) ) ) : No typesetting found for |- ( ( bday ` x ) = a -> ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> x e. ( _Made ` a ) ) ) with typecode |-
64	63	com12	Could not format ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> ( ( bday ` x ) = a -> x e. ( _Made ` a ) ) ) : No typesetting found for |- ( ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ x e. No ) -> ( ( bday ` x ) = a -> x e. ( _Made ` a ) ) ) with typecode |-
65	64	adantll	Could not format ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) = a -> x e. ( _Made ` a ) ) ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) = a -> x e. ( _Made ` a ) ) ) with typecode |-
66	45 65	jaod	Could not format ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( ( bday ` x ) e. a \/ ( bday ` x ) = a ) -> x e. ( _Made ` a ) ) ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( ( bday ` x ) e. a \/ ( bday ` x ) = a ) -> x e. ( _Made ` a ) ) ) with typecode |-
67	21 66	sylbid	Could not format ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) ) : No typesetting found for |- ( ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) /\ x e. No ) -> ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) ) with typecode |-
68	67	ralrimiva	Could not format ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) -> A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) ) : No typesetting found for |- ( ( a e. On /\ A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) -> A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) ) with typecode |-
69	68	ex	Could not format ( a e. On -> ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) -> A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) ) ) : No typesetting found for |- ( a e. On -> ( A. b e. a A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) -> A. x e. No ( ( bday ` x ) C_ a -> x e. ( _Made ` a ) ) ) ) with typecode |-
70	12 17 69	tfis3	Could not format ( A e. On -> A. x e. No ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) ) : No typesetting found for |- ( A e. On -> A. x e. No ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) ) with typecode |-
71		fveq2	$$⊢x=X\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(X\right)$$
72	71	sseq1d	$$⊢x=X\to \left(\mathrm{bday}\left(x\right)\subseteq A\leftrightarrow \mathrm{bday}\left(X\right)\subseteq A\right)$$
73		eleq1	Could not format ( x = X -> ( x e. ( _Made ` A ) <-> X e. ( _Made ` A ) ) ) : No typesetting found for |- ( x = X -> ( x e. ( _Made ` A ) <-> X e. ( _Made ` A ) ) ) with typecode |-
74	72 73	imbi12d	Could not format ( x = X -> ( ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) <-> ( ( bday ` X ) C_ A -> X e. ( _Made ` A ) ) ) ) : No typesetting found for |- ( x = X -> ( ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) <-> ( ( bday ` X ) C_ A -> X e. ( _Made ` A ) ) ) ) with typecode |-
75	74	rspccva	Could not format ( ( A. x e. No ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) /\ X e. No ) -> ( ( bday ` X ) C_ A -> X e. ( _Made ` A ) ) ) : No typesetting found for |- ( ( A. x e. No ( ( bday ` x ) C_ A -> x e. ( _Made ` A ) ) /\ X e. No ) -> ( ( bday ` X ) C_ A -> X e. ( _Made ` A ) ) ) with typecode |-
76	70 75	sylan	Could not format ( ( A e. On /\ X e. No ) -> ( ( bday ` X ) C_ A -> X e. ( _Made ` A ) ) ) : No typesetting found for |- ( ( A e. On /\ X e. No ) -> ( ( bday ` X ) C_ A -> X e. ( _Made ` A ) ) ) with typecode |-
77	1 76	impbid2	Could not format ( ( A e. On /\ X e. No ) -> ( X e. ( _Made ` A ) <-> ( bday ` X ) C_ A ) ) : No typesetting found for |- ( ( A e. On /\ X e. No ) -> ( X e. ( _Made ` A ) <-> ( bday ` X ) C_ A ) ) with typecode |-