Theorem madebdaylemlrcut

Description: Lemma for madebday . If the inductive hypothesis of madebday is satisfied up to the birthday of X , then the conclusion of lrcut holds. (Contributed by Scott Fenton, 19-Aug-2024)

	Ref	Expression
Assertion	madebdaylemlrcut	Could not format assertion : 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 |-

Proof

Step	Hyp	Ref	Expression
1		ssltleft	Could not format ( X e. No -> ( _Left ` X ) < ( _Left ` X ) <
2	1	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 ) < y e. ( _Made ` b ) ) /\ X e. No ) -> ( _Left ` X ) <
3		ssltright	Could not format ( X e. No -> { X } < { X } <
4	3	adantl	Could not format ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> { X } < y e. ( _Made ` b ) ) /\ X e. No ) -> { X } <
5		fveq2	$$⊢X=w\to \mathrm{bday}\left(X\right)=\mathrm{bday}\left(w\right)$$
6		eqimss	$$⊢\mathrm{bday}\left(X\right)=\mathrm{bday}\left(w\right)\to \mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(w\right)$$
7	5 6	syl	$$⊢X=w\to \mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(w\right)$$
8	7	a1i	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( ( _Left ` X ) < ( X = w -> ( bday ` X ) C_ ( bday ` w ) ) ) : No typesetting found for |- ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( ( _Left ` X ) < ( X = w -> ( bday ` X ) C_ ( bday ` w ) ) ) with typecode |-
9		ssltsep	Could not format ( ( _Left ` X ) < A. x e. ( _Left ` X ) A. y e. { w } x A. x e. ( _Left ` X ) A. y e. { w } x
10		vex	$$⊢w\in \mathrm{V}$$
11		breq2	$$⊢y=w\to \left(x{<}_{s}y\leftrightarrow x{<}_{s}w\right)$$
12	10 11	ralsn	$$⊢\forall y\in \left\{w\right\}x{<}_{s}y\leftrightarrow x{<}_{s}w$$
13	12	ralbii	Could not format ( A. x e. ( _Left ` X ) A. y e. { w } x A. x e. ( _Left ` X ) x A. x e. ( _Left ` X ) x
14	9 13	sylib	Could not format ( ( _Left ` X ) < A. x e. ( _Left ` X ) x A. x e. ( _Left ` X ) x
15		ssltsep	Could not format ( { w } < A. y e. { w } A. x e. ( _Right ` X ) y A. y e. { w } A. x e. ( _Right ` X ) y
16		breq1	$$⊢y=w\to \left(y{<}_{s}x\leftrightarrow w{<}_{s}x\right)$$
17	16	ralbidv	Could not format ( y = w -> ( A. x e. ( _Right ` X ) y A. x e. ( _Right ` X ) w ( A. x e. ( _Right ` X ) y A. x e. ( _Right ` X ) w
18	10 17	ralsn	Could not format ( A. y e. { w } A. x e. ( _Right ` X ) y A. x e. ( _Right ` X ) w A. x e. ( _Right ` X ) w
19	15 18	sylib	Could not format ( { w } < A. x e. ( _Right ` X ) w A. x e. ( _Right ` X ) w
20	14 19	anim12i	Could not format ( ( ( _Left ` X ) < ( A. x e. ( _Left ` X ) x ( A. x e. ( _Left ` X ) x
21		leftval	Could not format ( _Left ` X ) = { z e. ( _Old ` ( bday ` X ) ) | z
22	21	a1i	Could not format ( X e. No -> ( _Left ` X ) = { z e. ( _Old ` ( bday ` X ) ) | z ( _Left ` X ) = { z e. ( _Old ` ( bday ` X ) ) | z
23	22	raleqdv	Could not format ( X e. No -> ( A. x e. ( _Left ` X ) x A. x e. { z e. ( _Old ` ( bday ` X ) ) | z ( A. x e. ( _Left ` X ) x A. x e. { z e. ( _Old ` ( bday ` X ) ) | z
24		rightval	Could not format ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
25	24	a1i	Could not format ( X e. No -> ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X ( _Right ` X ) = { z e. ( _Old ` ( bday ` X ) ) | X
26	25	raleqdv	Could not format ( X e. No -> ( A. x e. ( _Right ` X ) w A. x e. { z e. ( _Old ` ( bday ` X ) ) | X ( A. x e. ( _Right ` X ) w A. x e. { z e. ( _Old ` ( bday ` X ) ) | X
27	23 26	anbi12d	Could not format ( X e. No -> ( ( A. x e. ( _Left ` X ) x ( A. x e. { z e. ( _Old ` ( bday ` X ) ) | z ( ( A. x e. ( _Left ` X ) x ( A. x e. { z e. ( _Old ` ( bday ` X ) ) | z
28		breq1	$$⊢z=x\to \left(z{<}_{s}X\leftrightarrow x{<}_{s}X\right)$$
29	28	ralrab	$$⊢\forall x\in \left\{z\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)|z{<}_{s}X\right\}x{<}_{s}w\leftrightarrow \forall x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\left(x{<}_{s}X\to x{<}_{s}w\right)$$
30		breq2	$$⊢z=x\to \left(X{<}_{s}z\leftrightarrow X{<}_{s}x\right)$$
31	30	ralrab	$$⊢\forall x\in \left\{z\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)|X{<}_{s}z\right\}w{<}_{s}x\leftrightarrow \forall x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\left(X{<}_{s}x\to w{<}_{s}x\right)$$
32	29 31	anbi12i	$$⊢\left(\forall x\in \left\{z\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)|z{<}_{s}X\right\}x{<}_{s}w\wedge \forall x\in \left\{z\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)|X{<}_{s}z\right\}w{<}_{s}x\right)\leftrightarrow \left(\forall x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\left(x{<}_{s}X\to x{<}_{s}w\right)\wedge \forall x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\left(X{<}_{s}x\to w{<}_{s}x\right)\right)$$
33	27 32	bitrdi	Could not format ( X e. No -> ( ( A. x e. ( _Left ` X ) x ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( ( A. x e. ( _Left ` X ) x ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w
34	33	ad2antlr	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ w e. No ) -> ( ( A. x e. ( _Left ` X ) x ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w y e. ( _Made ` b ) ) /\ X e. No ) /\ w e. No ) -> ( ( A. x e. ( _Left ` X ) x ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w
35		simplrl	Could not format ( ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w w e. No ) : No typesetting found for |- ( ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w w e. No ) with typecode |-
36		sltirr	$$⊢w\in \mathrm{No}\to \neg w{<}_{s}w$$
37	35 36	syl	Could not format ( ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w -. w y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w -. w
38		bdayelon	$$⊢\mathrm{bday}\left(X\right)\in \mathrm{On}$$
39		bdayelon	$$⊢\mathrm{bday}\left(w\right)\in \mathrm{On}$$
40		ontri1	$$⊢\left(\mathrm{bday}\left(X\right)\in \mathrm{On}\wedge \mathrm{bday}\left(w\right)\in \mathrm{On}\right)\to \left(\mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(w\right)\leftrightarrow \neg \mathrm{bday}\left(w\right)\in \mathrm{bday}\left(X\right)\right)$$
41	38 39 40	mp2an	$$⊢\mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(w\right)\leftrightarrow \neg \mathrm{bday}\left(w\right)\in \mathrm{bday}\left(X\right)$$
42	41	con2bii	$$⊢\mathrm{bday}\left(w\right)\in \mathrm{bday}\left(X\right)\leftrightarrow \neg \mathrm{bday}\left(X\right)\subseteq \mathrm{bday}\left(w\right)$$
43		simplll	Could not format ( ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) : No typesetting found for |- ( ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) ) with typecode |-
44		madebdaylemold	Could not format ( ( ( bday ` X ) e. On /\ A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ w e. No ) -> ( ( bday ` w ) e. ( bday ` X ) -> w e. ( _Old ` ( bday ` X ) ) ) ) : No typesetting found for |- ( ( ( bday ` X ) e. On /\ A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ w e. No ) -> ( ( bday ` w ) e. ( bday ` X ) -> w e. ( _Old ` ( bday ` X ) ) ) ) with typecode |-
45	38 43 35 44	mp3an2i	Could not format ( ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( ( bday ` w ) e. ( bday ` X ) -> w e. ( _Old ` ( 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 ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( ( bday ` w ) e. ( bday ` X ) -> w e. ( _Old ` ( bday ` X ) ) ) ) with typecode |-
46		slttrine	$$⊢\left(X\in \mathrm{No}\wedge w\in \mathrm{No}\right)\to \left(X\ne w\leftrightarrow \left(X{<}_{s}w\vee w{<}_{s}X\right)\right)$$
47	46	ad2ant2lr	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( X =/= w <-> ( X y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( X =/= w <-> ( X
48		simprrr	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w A. x e. ( _Old ` ( bday ` X ) ) ( X w y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w A. x e. ( _Old ` ( bday ` X ) ) ( X w
49		breq2	$$⊢x=w\to \left(X{<}_{s}x\leftrightarrow X{<}_{s}w\right)$$
50		breq2	$$⊢x=w\to \left(w{<}_{s}x\leftrightarrow w{<}_{s}w\right)$$
51	49 50	imbi12d	$$⊢x=w\to \left(\left(X{<}_{s}x\to w{<}_{s}x\right)\leftrightarrow \left(X{<}_{s}w\to w{<}_{s}w\right)\right)$$
52	51	rspccv	$$⊢\forall x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\left(X{<}_{s}x\to w{<}_{s}x\right)\to \left(w\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\to \left(X{<}_{s}w\to w{<}_{s}w\right)\right)$$
53	48 52	syl	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( w e. ( _Old ` ( bday ` X ) ) -> ( X w y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( w e. ( _Old ` ( bday ` X ) ) -> ( X w
54	53	com23	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( X ( w e. ( _Old ` ( bday ` X ) ) -> w y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( X ( w e. ( _Old ` ( bday ` X ) ) -> w
55		simprrl	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w A. x e. ( _Old ` ( bday ` X ) ) ( x x y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w A. x e. ( _Old ` ( bday ` X ) ) ( x x
56		breq1	$$⊢x=w\to \left(x{<}_{s}X\leftrightarrow w{<}_{s}X\right)$$
57		breq1	$$⊢x=w\to \left(x{<}_{s}w\leftrightarrow w{<}_{s}w\right)$$
58	56 57	imbi12d	$$⊢x=w\to \left(\left(x{<}_{s}X\to x{<}_{s}w\right)\leftrightarrow \left(w{<}_{s}X\to w{<}_{s}w\right)\right)$$
59	58	rspccv	$$⊢\forall x\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\left(x{<}_{s}X\to x{<}_{s}w\right)\to \left(w\in \mathrm{Old}\left(\mathrm{bday}\left(X\right)\right)\to \left(w{<}_{s}X\to w{<}_{s}w\right)\right)$$
60	55 59	syl	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( w e. ( _Old ` ( bday ` X ) ) -> ( w w y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( w e. ( _Old ` ( bday ` X ) ) -> ( w w
61	60	com23	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( w ( w e. ( _Old ` ( bday ` X ) ) -> w y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( w ( w e. ( _Old ` ( bday ` X ) ) -> w
62	54 61	jaod	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( ( X ( w e. ( _Old ` ( bday ` X ) ) -> w y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( ( X ( w e. ( _Old ` ( bday ` X ) ) -> w
63	47 62	sylbid	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( X =/= w -> ( w e. ( _Old ` ( bday ` X ) ) -> w y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( X =/= w -> ( w e. ( _Old ` ( bday ` X ) ) -> w
64	63	imp	Could not format ( ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( w e. ( _Old ` ( bday ` X ) ) -> w y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( w e. ( _Old ` ( bday ` X ) ) -> w
65	45 64	syld	Could not format ( ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( ( bday ` w ) e. ( bday ` X ) -> w y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( ( bday ` w ) e. ( bday ` X ) -> w
66	42 65	biimtrrid	Could not format ( ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( -. ( bday ` X ) C_ ( bday ` w ) -> w y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( -. ( bday ` X ) C_ ( bday ` w ) -> w
67	37 66	mt3d	Could not format ( ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( bday ` X ) C_ ( bday ` w ) ) : No typesetting found for |- ( ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( bday ` X ) C_ ( bday ` w ) ) with typecode |-
68	67	ex	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( X =/= w -> ( bday ` X ) C_ ( bday ` w ) ) ) : No typesetting found for |- ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( X =/= w -> ( bday ` X ) C_ ( bday ` w ) ) ) with typecode |-
69	68	expr	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ w e. No ) -> ( ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( X =/= w -> ( bday ` X ) C_ ( bday ` w ) ) ) ) : No typesetting found for |- ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ w e. No ) -> ( ( A. x e. ( _Old ` ( bday ` X ) ) ( x x w ( X =/= w -> ( bday ` X ) C_ ( bday ` w ) ) ) ) with typecode |-
70	34 69	sylbid	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ w e. No ) -> ( ( A. x e. ( _Left ` X ) x ( X =/= w -> ( bday ` X ) C_ ( bday ` w ) ) ) ) : No typesetting found for |- ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ w e. No ) -> ( ( A. x e. ( _Left ` X ) x ( X =/= w -> ( bday ` X ) C_ ( bday ` w ) ) ) ) with typecode |-
71	70	impr	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Left ` X ) x ( X =/= w -> ( bday ` X ) C_ ( bday ` w ) ) ) : No typesetting found for |- ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( A. x e. ( _Left ` X ) x ( X =/= w -> ( bday ` X ) C_ ( bday ` w ) ) ) with typecode |-
72	20 71	sylanr2	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( ( _Left ` X ) < ( X =/= w -> ( bday ` X ) C_ ( bday ` w ) ) ) : No typesetting found for |- ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( ( _Left ` X ) < ( X =/= w -> ( bday ` X ) C_ ( bday ` w ) ) ) with typecode |-
73	8 72	pm2.61dne	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( ( _Left ` X ) < ( bday ` X ) C_ ( bday ` w ) ) : No typesetting found for |- ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ ( w e. No /\ ( ( _Left ` X ) < ( bday ` X ) C_ ( bday ` w ) ) with typecode |-
74	73	expr	Could not format ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ w e. No ) -> ( ( ( _Left ` X ) < ( bday ` X ) C_ ( bday ` w ) ) ) : No typesetting found for |- ( ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) /\ w e. No ) -> ( ( ( _Left ` X ) < ( bday ` X ) C_ ( bday ` w ) ) ) with typecode |-
75	74	ralrimiva	Could not format ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> A. w e. No ( ( ( _Left ` X ) < ( bday ` X ) C_ ( bday ` w ) ) ) : No typesetting found for |- ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> A. w e. No ( ( ( _Left ` X ) < ( bday ` X ) C_ ( bday ` w ) ) ) with typecode |-
76		bdayfn	$$⊢\mathrm{bday}Fn\mathrm{No}$$
77		ssrab2	Could not format { z e. No | ( ( _Left ` X ) <
78		fnssintima	Could not format ( ( bday Fn No /\ { z e. No | ( ( _Left ` X ) < ( ( bday ` X ) C_ |^| ( bday " { z e. No | ( ( _Left ` X ) < A. w e. { z e. No | ( ( _Left ` X ) < ( ( bday ` X ) C_ |^| ( bday " { z e. No | ( ( _Left ` X ) < A. w e. { z e. No | ( ( _Left ` X ) <
79	76 77 78	mp2an	Could not format ( ( bday ` X ) C_ |^| ( bday " { z e. No | ( ( _Left ` X ) < A. w e. { z e. No | ( ( _Left ` X ) < A. w e. { z e. No | ( ( _Left ` X ) <
80		sneq	$$⊢z=w\to \left\{z\right\}=\left\{w\right\}$$
81	80	breq2d	Could not format ( z = w -> ( ( _Left ` X ) < ( _Left ` X ) < ( ( _Left ` X ) < ( _Left ` X ) <
82	80	breq1d	Could not format ( z = w -> ( { z } < { w } < ( { z } < { w } <
83	81 82	anbi12d	Could not format ( z = w -> ( ( ( _Left ` X ) < ( ( _Left ` X ) < ( ( ( _Left ` X ) < ( ( _Left ` X ) <
84	83	ralrab	Could not format ( A. w e. { z e. No | ( ( _Left ` X ) < A. w e. No ( ( ( _Left ` X ) < ( bday ` X ) C_ ( bday ` w ) ) ) : No typesetting found for |- ( A. w e. { z e. No | ( ( _Left ` X ) < A. w e. No ( ( ( _Left ` X ) < ( bday ` X ) C_ ( bday ` w ) ) ) with typecode |-
85	79 84	bitri	Could not format ( ( bday ` X ) C_ |^| ( bday " { z e. No | ( ( _Left ` X ) < A. w e. No ( ( ( _Left ` X ) < ( bday ` X ) C_ ( bday ` w ) ) ) : No typesetting found for |- ( ( bday ` X ) C_ |^| ( bday " { z e. No | ( ( _Left ` X ) < A. w e. No ( ( ( _Left ` X ) < ( bday ` X ) C_ ( bday ` w ) ) ) with typecode |-
86	75 85	sylibr	Could not format ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( bday ` X ) C_ |^| ( bday " { z e. No | ( ( _Left ` X ) < y e. ( _Made ` b ) ) /\ X e. No ) -> ( bday ` X ) C_ |^| ( bday " { z e. No | ( ( _Left ` X ) <
87		sneq	$$⊢z=X\to \left\{z\right\}=\left\{X\right\}$$
88	87	breq2d	Could not format ( z = X -> ( ( _Left ` X ) < ( _Left ` X ) < ( ( _Left ` X ) < ( _Left ` X ) <
89	87	breq1d	Could not format ( z = X -> ( { z } < { X } < ( { z } < { X } <
90	88 89	anbi12d	Could not format ( z = X -> ( ( ( _Left ` X ) < ( ( _Left ` X ) < ( ( ( _Left ` X ) < ( ( _Left ` X ) <
91		simpr	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. No ) : 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. No ) with typecode |-
92	2 4	jca	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 ) < y e. ( _Made ` b ) ) /\ X e. No ) -> ( ( _Left ` X ) <
93	90 91 92	elrabd	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. { z e. No | ( ( _Left ` X ) < y e. ( _Made ` b ) ) /\ X e. No ) -> X e. { z e. No | ( ( _Left ` X ) <
94		fnfvima	Could not format ( ( bday Fn No /\ { z e. No | ( ( _Left ` X ) < ( bday ` X ) e. ( bday " { z e. No | ( ( _Left ` X ) < ( bday ` X ) e. ( bday " { z e. No | ( ( _Left ` X ) <
95	76 77 93 94	mp3an12i	Could not format ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( bday ` X ) e. ( bday " { z e. No | ( ( _Left ` X ) < y e. ( _Made ` b ) ) /\ X e. No ) -> ( bday ` X ) e. ( bday " { z e. No | ( ( _Left ` X ) <
96		intss1	Could not format ( ( bday ` X ) e. ( bday " { z e. No | ( ( _Left ` X ) < |^| ( bday " { z e. No | ( ( _Left ` X ) < |^| ( bday " { z e. No | ( ( _Left ` X ) <
97	95 96	syl	Could not format ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> |^| ( bday " { z e. No | ( ( _Left ` X ) < y e. ( _Made ` b ) ) /\ X e. No ) -> |^| ( bday " { z e. No | ( ( _Left ` X ) <
98	86 97	eqssd	Could not format ( ( A. b e. ( bday ` X ) A. y e. No ( ( bday ` y ) C_ b -> y e. ( _Made ` b ) ) /\ X e. No ) -> ( bday ` X ) = |^| ( bday " { z e. No | ( ( _Left ` X ) < y e. ( _Made ` b ) ) /\ X e. No ) -> ( bday ` X ) = |^| ( bday " { z e. No | ( ( _Left ` X ) <
99		lltropt	Could not format ( _Left ` X ) <
100		eqscut	Could not format ( ( ( _Left ` X ) < ( ( ( _Left ` X ) |s ( _Right ` X ) ) = X <-> ( ( _Left ` X ) < ( ( ( _Left ` X ) |s ( _Right ` X ) ) = X <-> ( ( _Left ` X ) <
101	99 100	mpan	Could not format ( X e. No -> ( ( ( _Left ` X ) |s ( _Right ` X ) ) = X <-> ( ( _Left ` X ) < ( ( ( _Left ` X ) |s ( _Right ` X ) ) = X <-> ( ( _Left ` X ) <
102	101	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 ) ) = X <-> ( ( _Left ` X ) < y e. ( _Made ` b ) ) /\ X e. No ) -> ( ( ( _Left ` X ) |s ( _Right ` X ) ) = X <-> ( ( _Left ` X ) <
103	2 4 98 102	mpbir3and	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 |-