Theorem addsonbday

Description: The birthday of the sum of two ordinals is the natural sum of their birthdays. (Contributed by Scott Fenton, 22-Feb-2026)

	Ref	Expression
Assertion	addsonbday	$$⊢\left(A\in {On}_s\wedge B\in {On}_s\right)\to \mathrm{bday}\left(A{+}_{s}B\right)=\mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		onsno	$$⊢A\in {On}_s\to A\in \mathrm{No}$$
2		onsno	$$⊢B\in {On}_s\to B\in \mathrm{No}$$
3		addsbday	$$⊢\left(A\in \mathrm{No}\wedge B\in \mathrm{No}\right)\to \mathrm{bday}\left(A{+}_{s}B\right)\subseteq \mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)$$
4	1 2 3	syl2an	$$⊢\left(A\in {On}_s\wedge B\in {On}_s\right)\to \mathrm{bday}\left(A{+}_{s}B\right)\subseteq \mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)$$
5		fveq2	Could not format ( x = xO -> ( bday ` x ) = ( bday ` xO ) ) : No typesetting found for |- ( x = xO -> ( bday ` x ) = ( bday ` xO ) ) with typecode |-
6	5	oveq1d	Could not format ( x = xO -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) ) : No typesetting found for |- ( x = xO -> ( ( bday ` x ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` y ) ) ) with typecode |-
7		fvoveq1	Could not format ( x = xO -> ( bday ` ( x +s y ) ) = ( bday ` ( xO +s y ) ) ) : No typesetting found for |- ( x = xO -> ( bday ` ( x +s y ) ) = ( bday ` ( xO +s y ) ) ) with typecode |-
8	6 7	sseq12d	Could not format ( x = xO -> ( ( ( bday ` x ) +no ( bday ` y ) ) C_ ( bday ` ( x +s y ) ) <-> ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) ) : No typesetting found for |- ( x = xO -> ( ( ( bday ` x ) +no ( bday ` y ) ) C_ ( bday ` ( x +s y ) ) <-> ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) ) with typecode |-
9		fveq2	Could not format ( y = yO -> ( bday ` y ) = ( bday ` yO ) ) : No typesetting found for |- ( y = yO -> ( bday ` y ) = ( bday ` yO ) ) with typecode |-
10	9	oveq2d	Could not format ( y = yO -> ( ( bday ` xO ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) ) : No typesetting found for |- ( y = yO -> ( ( bday ` xO ) +no ( bday ` y ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) ) with typecode |-
11		oveq2	Could not format ( y = yO -> ( xO +s y ) = ( xO +s yO ) ) : No typesetting found for |- ( y = yO -> ( xO +s y ) = ( xO +s yO ) ) with typecode |-
12	11	fveq2d	Could not format ( y = yO -> ( bday ` ( xO +s y ) ) = ( bday ` ( xO +s yO ) ) ) : No typesetting found for |- ( y = yO -> ( bday ` ( xO +s y ) ) = ( bday ` ( xO +s yO ) ) ) with typecode |-
13	10 12	sseq12d	Could not format ( y = yO -> ( ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) <-> ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) ) : No typesetting found for |- ( y = yO -> ( ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) <-> ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) ) with typecode |-
14	5	oveq1d	Could not format ( x = xO -> ( ( bday ` x ) +no ( bday ` yO ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) ) : No typesetting found for |- ( x = xO -> ( ( bday ` x ) +no ( bday ` yO ) ) = ( ( bday ` xO ) +no ( bday ` yO ) ) ) with typecode |-
15		fvoveq1	Could not format ( x = xO -> ( bday ` ( x +s yO ) ) = ( bday ` ( xO +s yO ) ) ) : No typesetting found for |- ( x = xO -> ( bday ` ( x +s yO ) ) = ( bday ` ( xO +s yO ) ) ) with typecode |-
16	14 15	sseq12d	Could not format ( x = xO -> ( ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) <-> ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) ) : No typesetting found for |- ( x = xO -> ( ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) <-> ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) ) with typecode |-
17		fveq2	$$⊢x=A\to \mathrm{bday}\left(x\right)=\mathrm{bday}\left(A\right)$$
18	17	oveq1d	$$⊢x=A\to \mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)=\mathrm{bday}\left(A\right)+\mathrm{bday}\left(y\right)$$
19		fvoveq1	$$⊢x=A\to \mathrm{bday}\left(x{+}_{s}y\right)=\mathrm{bday}\left(A{+}_{s}y\right)$$
20	18 19	sseq12d	$$⊢x=A\to \left(\mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)\subseteq \mathrm{bday}\left(x{+}_{s}y\right)\leftrightarrow \mathrm{bday}\left(A\right)+\mathrm{bday}\left(y\right)\subseteq \mathrm{bday}\left(A{+}_{s}y\right)\right)$$
21		fveq2	$$⊢y=B\to \mathrm{bday}\left(y\right)=\mathrm{bday}\left(B\right)$$
22	21	oveq2d	$$⊢y=B\to \mathrm{bday}\left(A\right)+\mathrm{bday}\left(y\right)=\mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)$$
23		oveq2	$$⊢y=B\to A{+}_{s}y=A{+}_{s}B$$
24	23	fveq2d	$$⊢y=B\to \mathrm{bday}\left(A{+}_{s}y\right)=\mathrm{bday}\left(A{+}_{s}B\right)$$
25	22 24	sseq12d	$$⊢y=B\to \left(\mathrm{bday}\left(A\right)+\mathrm{bday}\left(y\right)\subseteq \mathrm{bday}\left(A{+}_{s}y\right)\leftrightarrow \mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)\subseteq \mathrm{bday}\left(A{+}_{s}B\right)\right)$$
26		bdayelon	$$⊢\mathrm{bday}\left(x\right)\in \mathrm{On}$$
27		bdayelon	$$⊢\mathrm{bday}\left(y\right)\in \mathrm{On}$$
28		naddov2	$$⊢\left(\mathrm{bday}\left(x\right)\in \mathrm{On}\wedge \mathrm{bday}\left(y\right)\in \mathrm{On}\right)\to \mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)=\bigcap \left\{a\in \mathrm{On}|\left(\forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in a\wedge \forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in a\right)\right\}$$
29	26 27 28	mp2an	$$⊢\mathrm{bday}\left(x\right)+\mathrm{bday}\left(y\right)=\bigcap \left\{a\in \mathrm{On}|\left(\forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in a\wedge \forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in a\right)\right\}$$
30	27	oneli	$$⊢q\in \mathrm{bday}\left(y\right)\to q\in \mathrm{On}$$
31		breq1	Could not format ( yO = ( `' ( bday |` On_s ) ` q ) -> ( yO ( `' ( bday |` On_s ) ` q ) ( yO ( `' ( bday |` On_s ) ` q )
32		fveq2	Could not format ( yO = ( `' ( bday |` On_s ) ` q ) -> ( bday ` yO ) = ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) : No typesetting found for |- ( yO = ( `' ( bday |` On_s ) ` q ) -> ( bday ` yO ) = ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) with typecode |-
33	32	oveq2d	Could not format ( yO = ( `' ( bday |` On_s ) ` q ) -> ( ( bday ` x ) +no ( bday ` yO ) ) = ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) ) : No typesetting found for |- ( yO = ( `' ( bday |` On_s ) ` q ) -> ( ( bday ` x ) +no ( bday ` yO ) ) = ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) ) with typecode |-
34		oveq2	Could not format ( yO = ( `' ( bday |` On_s ) ` q ) -> ( x +s yO ) = ( x +s ( `' ( bday |` On_s ) ` q ) ) ) : No typesetting found for |- ( yO = ( `' ( bday |` On_s ) ` q ) -> ( x +s yO ) = ( x +s ( `' ( bday |` On_s ) ` q ) ) ) with typecode |-
35	34	fveq2d	Could not format ( yO = ( `' ( bday |` On_s ) ` q ) -> ( bday ` ( x +s yO ) ) = ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) : No typesetting found for |- ( yO = ( `' ( bday |` On_s ) ` q ) -> ( bday ` ( x +s yO ) ) = ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) with typecode |-
36	33 35	sseq12d	Could not format ( yO = ( `' ( bday |` On_s ) ` q ) -> ( ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) <-> ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) ) : No typesetting found for |- ( yO = ( `' ( bday |` On_s ) ` q ) -> ( ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) <-> ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) ) with typecode |-
37	31 36	imbi12d	Could not format ( yO = ( `' ( bday |` On_s ) ` q ) -> ( ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) <-> ( ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) ) ) : No typesetting found for |- ( yO = ( `' ( bday |` On_s ) ` q ) -> ( ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) <-> ( ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) ) ) with typecode |-
38		simplr3	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) with typecode |-
39		onsiso	$$⊢\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right){Isom}_{{<}_s,\mathrm{E}}\left({On}_s,\mathrm{On}\right)$$
40		isof1o	$$⊢\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right){Isom}_{{<}_s,\mathrm{E}}\left({On}_s,\mathrm{On}\right)\to \left({\mathrm{bday}\upharpoonright }_{{On}_s}\right):{On}_s\underset{1-1\; onto}{⟶}\mathrm{On}$$
41	39 40	ax-mp	$$⊢\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right):{On}_s\underset{1-1\; onto}{⟶}\mathrm{On}$$
42		f1ocnvdm	$$⊢\left(\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right):{On}_s\underset{1-1\; onto}{⟶}\mathrm{On}\wedge q\in \mathrm{On}\right)\to {\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\in {On}_s$$
43	41 42	mpan	$$⊢q\in \mathrm{On}\to {\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\in {On}_s$$
44	43	adantl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( `' ( bday |` On_s ) ` q ) e. On_s ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( `' ( bday |` On_s ) ` q ) e. On_s ) with typecode |-
45	37 38 44	rspcdva	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) ) with typecode |-
46	45	impr	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( q e. On /\ ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( q e. On /\ ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) C_ ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) ) with typecode |-
47		onsno	$$⊢{\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\in {On}_s\to {\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\in \mathrm{No}$$
48	44 47	syl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( `' ( bday |` On_s ) ` q ) e. No ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( `' ( bday |` On_s ) ` q ) e. No ) with typecode |-
49		simpllr	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> y e. On_s ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> y e. On_s ) with typecode |-
50		onsno	$$⊢y\in {On}_s\to y\in \mathrm{No}$$
51	49 50	syl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> y e. No ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> y e. No ) with typecode |-
52		simplll	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> x e. On_s ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> x e. On_s ) with typecode |-
53		onsno	$$⊢x\in {On}_s\to x\in \mathrm{No}$$
54	52 53	syl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> x e. No ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> x e. No ) with typecode |-
55	48 51 54	sltadd2d	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( x +s ( `' ( bday |` On_s ) ` q ) ) ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( x +s ( `' ( bday |` On_s ) ` q ) )
56		onaddscl	$$⊢\left(x\in {On}_s\wedge {\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\in {On}_s\right)\to x{+}_s{\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\in {On}_s$$
57	52 44 56	syl2anc	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( x +s ( `' ( bday |` On_s ) ` q ) ) e. On_s ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( x +s ( `' ( bday |` On_s ) ` q ) ) e. On_s ) with typecode |-
58		onaddscl	$$⊢\left(x\in {On}_s\wedge y\in {On}_s\right)\to x{+}_{s}y\in {On}_s$$
59	58	ad2antrr	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( x +s y ) e. On_s ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( x +s y ) e. On_s ) with typecode |-
60		onslt	$$⊢\left(x{+}_s{\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\in {On}_s\wedge x{+}_{s}y\in {On}_s\right)\to \left(\left(x{+}_s{\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right){<}_s\left(x{+}_{s}y\right)\leftrightarrow \mathrm{bday}\left(x{+}_s{\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)$$
61	57 59 60	syl2anc	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( x +s ( `' ( bday |` On_s ) ` q ) ) ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( x +s ( `' ( bday |` On_s ) ` q ) ) ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
62	55 61	bitrd	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
63	62	biimpd	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
64	63	impr	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( q e. On /\ ( `' ( bday |` On_s ) ` q ) ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( q e. On /\ ( `' ( bday |` On_s ) ` q ) ( bday ` ( x +s ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) with typecode |-
65		bdayelon	$$⊢\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{On}$$
66		naddcl	$$⊢\left(\mathrm{bday}\left(x\right)\in \mathrm{On}\wedge \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{On}\right)\to \mathrm{bday}\left(x\right)+\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{On}$$
67	26 65 66	mp2an	$$⊢\mathrm{bday}\left(x\right)+\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{On}$$
68	67	onordi	$$⊢\mathrm{Ord}\left(\mathrm{bday}\left(x\right)+\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\right)$$
69		bdayelon	$$⊢\mathrm{bday}\left(x{+}_{s}y\right)\in \mathrm{On}$$
70	69	onordi	$$⊢\mathrm{Ord}\mathrm{bday}\left(x{+}_{s}y\right)$$
71		ordtr2	$$⊢\left(\mathrm{Ord}\left(\mathrm{bday}\left(x\right)+\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\right)\wedge \mathrm{Ord}\mathrm{bday}\left(x{+}_{s}y\right)\right)\to \left(\left(\mathrm{bday}\left(x\right)+\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\subseteq \mathrm{bday}\left(x{+}_s{\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\wedge \mathrm{bday}\left(x{+}_s{\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)\to \mathrm{bday}\left(x\right)+\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)$$
72	68 70 71	mp2an	$$⊢\left(\mathrm{bday}\left(x\right)+\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\subseteq \mathrm{bday}\left(x{+}_s{\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\wedge \mathrm{bday}\left(x{+}_s{\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)\to \mathrm{bday}\left(x\right)+\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{bday}\left(x{+}_{s}y\right)$$
73	46 64 72	syl2anc	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( q e. On /\ ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( q e. On /\ ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) with typecode |-
74	73	expr	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
75	43	fvresd	$$⊢q\in \mathrm{On}\to \left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)=\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)$$
76	75	adantl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) = ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) = ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) with typecode |-
77	76	oveq2d	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) = ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) = ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) ) with typecode |-
78	77	eleq1d	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) <-> ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) <-> ( ( bday ` x ) +no ( bday ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
79	74 78	sylibrd	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
80		onslt	$$⊢\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\in {On}_s\wedge y\in {On}_s\right)\to \left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right){<}_{s}y\leftrightarrow \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{bday}\left(y\right)\right)$$
81	44 49 80	syl2anc	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( bday ` ( `' ( bday |` On_s ) ` q ) ) e. ( bday ` y ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) ( bday ` ( `' ( bday |` On_s ) ` q ) ) e. ( bday ` y ) ) ) with typecode |-
82		f1ocnvfv2	$$⊢\left(\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right):{On}_s\underset{1-1\; onto}{⟶}\mathrm{On}\wedge q\in \mathrm{On}\right)\to \left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)=q$$
83	41 82	mpan	$$⊢q\in \mathrm{On}\to \left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)=q$$
84	75 83	eqtr3d	$$⊢q\in \mathrm{On}\to \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)=q$$
85	84	eleq1d	$$⊢q\in \mathrm{On}\to \left(\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{bday}\left(y\right)\leftrightarrow q\in \mathrm{bday}\left(y\right)\right)$$
86	85	adantl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( bday ` ( `' ( bday |` On_s ) ` q ) ) e. ( bday ` y ) <-> q e. ( bday ` y ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( bday ` ( `' ( bday |` On_s ) ` q ) ) e. ( bday ` y ) <-> q e. ( bday ` y ) ) ) with typecode |-
87	81 86	bitrd	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) q e. ( bday ` y ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( `' ( bday |` On_s ) ` q ) q e. ( bday ` y ) ) ) with typecode |-
88	83	oveq2d	$$⊢q\in \mathrm{On}\to \mathrm{bday}\left(x\right)+\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)=\mathrm{bday}\left(x\right)+q$$
89	88	eleq1d	$$⊢q\in \mathrm{On}\to \left(\mathrm{bday}\left(x\right)+\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(q\right)\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\leftrightarrow \mathrm{bday}\left(x\right)+q\in \mathrm{bday}\left(x{+}_{s}y\right)\right)$$
90	89	adantl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) <-> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( ( ( bday ` x ) +no ( ( bday |` On_s ) ` ( `' ( bday |` On_s ) ` q ) ) ) e. ( bday ` ( x +s y ) ) <-> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
91	79 87 90	3imtr3d	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ q e. On ) -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
92	91	ex	Could not format ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( q e. On -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) ) : No typesetting found for |- ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( q e. On -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) ) with typecode |-
93	30 92	syl5	Could not format ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( q e. ( bday ` y ) -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) ) : No typesetting found for |- ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( q e. ( bday ` y ) -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) ) with typecode |-
94	93	pm2.43d	Could not format ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( q e. ( bday ` y ) -> ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
95	94	ralrimiv	Could not format ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) : No typesetting found for |- ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. ( bday ` ( x +s y ) ) ) with typecode |-
96	26	oneli	$$⊢p\in \mathrm{bday}\left(x\right)\to p\in \mathrm{On}$$
97		breq1	Could not format ( xO = ( `' ( bday |` On_s ) ` p ) -> ( xO ( `' ( bday |` On_s ) ` p ) ( xO ( `' ( bday |` On_s ) ` p )
98		fveq2	Could not format ( xO = ( `' ( bday |` On_s ) ` p ) -> ( bday ` xO ) = ( bday ` ( `' ( bday |` On_s ) ` p ) ) ) : No typesetting found for |- ( xO = ( `' ( bday |` On_s ) ` p ) -> ( bday ` xO ) = ( bday ` ( `' ( bday |` On_s ) ` p ) ) ) with typecode |-
99	98	oveq1d	Could not format ( xO = ( `' ( bday |` On_s ) ` p ) -> ( ( bday ` xO ) +no ( bday ` y ) ) = ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) ) : No typesetting found for |- ( xO = ( `' ( bday |` On_s ) ` p ) -> ( ( bday ` xO ) +no ( bday ` y ) ) = ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) ) with typecode |-
100		fvoveq1	Could not format ( xO = ( `' ( bday |` On_s ) ` p ) -> ( bday ` ( xO +s y ) ) = ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) : No typesetting found for |- ( xO = ( `' ( bday |` On_s ) ` p ) -> ( bday ` ( xO +s y ) ) = ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) with typecode |-
101	99 100	sseq12d	Could not format ( xO = ( `' ( bday |` On_s ) ` p ) -> ( ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) <-> ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) ) : No typesetting found for |- ( xO = ( `' ( bday |` On_s ) ` p ) -> ( ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) <-> ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) ) with typecode |-
102	97 101	imbi12d	Could not format ( xO = ( `' ( bday |` On_s ) ` p ) -> ( ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) <-> ( ( `' ( bday |` On_s ) ` p ) ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) ) ) : No typesetting found for |- ( xO = ( `' ( bday |` On_s ) ` p ) -> ( ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) <-> ( ( `' ( bday |` On_s ) ` p ) ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) ) ) with typecode |-
103		simplr2	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) ) with typecode |-
104		f1ocnvdm	$$⊢\left(\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right):{On}_s\underset{1-1\; onto}{⟶}\mathrm{On}\wedge p\in \mathrm{On}\right)\to {\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\in {On}_s$$
105	41 104	mpan	$$⊢p\in \mathrm{On}\to {\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\in {On}_s$$
106	105	adantl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( `' ( bday |` On_s ) ` p ) e. On_s ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( `' ( bday |` On_s ) ` p ) e. On_s ) with typecode |-
107	102 103 106	rspcdva	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) ) with typecode |-
108	107	impr	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( p e. On /\ ( `' ( bday |` On_s ) ` p ) ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( p e. On /\ ( `' ( bday |` On_s ) ` p ) ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) C_ ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) ) with typecode |-
109		onsno	$$⊢{\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\in {On}_s\to {\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\in \mathrm{No}$$
110	106 109	syl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( `' ( bday |` On_s ) ` p ) e. No ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( `' ( bday |` On_s ) ` p ) e. No ) with typecode |-
111		simplll	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> x e. On_s ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> x e. On_s ) with typecode |-
112	111 53	syl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> x e. No ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> x e. No ) with typecode |-
113		simpllr	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> y e. On_s ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> y e. On_s ) with typecode |-
114	113 50	syl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> y e. No ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> y e. No ) with typecode |-
115	110 112 114	sltadd1d	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) ( ( `' ( bday |` On_s ) ` p ) +s y ) ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) ( ( `' ( bday |` On_s ) ` p ) +s y )
116		onaddscl	$$⊢\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\in {On}_s\wedge y\in {On}_s\right)\to {\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){+}_{s}y\in {On}_s$$
117	106 113 116	syl2anc	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) +s y ) e. On_s ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) +s y ) e. On_s ) with typecode |-
118	58	ad2antrr	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( x +s y ) e. On_s ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( x +s y ) e. On_s ) with typecode |-
119		onslt	$$⊢\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){+}_{s}y\in {On}_s\wedge x{+}_{s}y\in {On}_s\right)\to \left(\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){+}_{s}y\right){<}_s\left(x{+}_{s}y\right)\leftrightarrow \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){+}_{s}y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)$$
120	117 118 119	syl2anc	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( ( `' ( bday |` On_s ) ` p ) +s y ) ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( ( `' ( bday |` On_s ) ` p ) +s y ) ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
121	115 120	bitrd	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
122	121	biimpd	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
123	122	impr	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( p e. On /\ ( `' ( bday |` On_s ) ` p ) ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( p e. On /\ ( `' ( bday |` On_s ) ` p ) ( bday ` ( ( `' ( bday |` On_s ) ` p ) +s y ) ) e. ( bday ` ( x +s y ) ) ) with typecode |-
124		bdayelon	$$⊢\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)\in \mathrm{On}$$
125		naddcl	$$⊢\left(\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)\in \mathrm{On}\wedge \mathrm{bday}\left(y\right)\in \mathrm{On}\right)\to \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)+\mathrm{bday}\left(y\right)\in \mathrm{On}$$
126	124 27 125	mp2an	$$⊢\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)+\mathrm{bday}\left(y\right)\in \mathrm{On}$$
127	126	onordi	$$⊢\mathrm{Ord}\left(\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)+\mathrm{bday}\left(y\right)\right)$$
128		ordtr2	$$⊢\left(\mathrm{Ord}\left(\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)+\mathrm{bday}\left(y\right)\right)\wedge \mathrm{Ord}\mathrm{bday}\left(x{+}_{s}y\right)\right)\to \left(\left(\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)+\mathrm{bday}\left(y\right)\subseteq \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){+}_{s}y\right)\wedge \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){+}_{s}y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)\to \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)+\mathrm{bday}\left(y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)$$
129	127 70 128	mp2an	$$⊢\left(\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)+\mathrm{bday}\left(y\right)\subseteq \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){+}_{s}y\right)\wedge \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){+}_{s}y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)\to \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)+\mathrm{bday}\left(y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)$$
130	108 123 129	syl2anc	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( p e. On /\ ( `' ( bday |` On_s ) ` p ) ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ ( p e. On /\ ( `' ( bday |` On_s ) ` p ) ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) with typecode |-
131	130	expr	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
132		onslt	$$⊢\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\in {On}_s\wedge x\in {On}_s\right)\to \left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){<}_{s}x\leftrightarrow \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)\in \mathrm{bday}\left(x\right)\right)$$
133	105 132	sylan	$$⊢\left(p\in \mathrm{On}\wedge x\in {On}_s\right)\to \left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){<}_{s}x\leftrightarrow \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)\in \mathrm{bday}\left(x\right)\right)$$
134	133	ancoms	$$⊢\left(x\in {On}_s\wedge p\in \mathrm{On}\right)\to \left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){<}_{s}x\leftrightarrow \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)\in \mathrm{bday}\left(x\right)\right)$$
135	105	fvresd	$$⊢p\in \mathrm{On}\to \left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)=\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)$$
136		f1ocnvfv2	$$⊢\left(\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right):{On}_s\underset{1-1\; onto}{⟶}\mathrm{On}\wedge p\in \mathrm{On}\right)\to \left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)=p$$
137	41 136	mpan	$$⊢p\in \mathrm{On}\to \left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)=p$$
138	135 137	eqtr3d	$$⊢p\in \mathrm{On}\to \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)=p$$
139	138	eleq1d	$$⊢p\in \mathrm{On}\to \left(\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)\in \mathrm{bday}\left(x\right)\leftrightarrow p\in \mathrm{bday}\left(x\right)\right)$$
140	139	adantl	$$⊢\left(x\in {On}_s\wedge p\in \mathrm{On}\right)\to \left(\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)\in \mathrm{bday}\left(x\right)\leftrightarrow p\in \mathrm{bday}\left(x\right)\right)$$
141	134 140	bitrd	$$⊢\left(x\in {On}_s\wedge p\in \mathrm{On}\right)\to \left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right){<}_{s}x\leftrightarrow p\in \mathrm{bday}\left(x\right)\right)$$
142	141	ad4ant14	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) p e. ( bday ` x ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( `' ( bday |` On_s ) ` p ) p e. ( bday ` x ) ) ) with typecode |-
143	138	oveq1d	$$⊢p\in \mathrm{On}\to \mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)+\mathrm{bday}\left(y\right)=p+\mathrm{bday}\left(y\right)$$
144	143	eleq1d	$$⊢p\in \mathrm{On}\to \left(\mathrm{bday}\left({\left({\mathrm{bday}\upharpoonright }_{{On}_s}\right)}^{-1}\left(p\right)\right)+\mathrm{bday}\left(y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\leftrightarrow p+\mathrm{bday}\left(y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)$$
145	144	adantl	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) <-> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( ( ( bday ` ( `' ( bday |` On_s ) ` p ) ) +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) <-> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
146	131 142 145	3imtr3d	Could not format ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) /\ p e. On ) -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
147	146	ex	Could not format ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( p e. On -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) ) : No typesetting found for |- ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( p e. On -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) ) with typecode |-
148	96 147	syl5	Could not format ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( p e. ( bday ` x ) -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) ) : No typesetting found for |- ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( p e. ( bday ` x ) -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) ) with typecode |-
149	148	pm2.43d	Could not format ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( p e. ( bday ` x ) -> ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) ) with typecode |-
150	149	ralrimiv	Could not format ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) : No typesetting found for |- ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. ( bday ` ( x +s y ) ) ) with typecode |-
151		eleq2	$$⊢a=\mathrm{bday}\left(x{+}_{s}y\right)\to \left(\mathrm{bday}\left(x\right)+q\in a\leftrightarrow \mathrm{bday}\left(x\right)+q\in \mathrm{bday}\left(x{+}_{s}y\right)\right)$$
152	151	ralbidv	$$⊢a=\mathrm{bday}\left(x{+}_{s}y\right)\to \left(\forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in a\leftrightarrow \forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in \mathrm{bday}\left(x{+}_{s}y\right)\right)$$
153		eleq2	$$⊢a=\mathrm{bday}\left(x{+}_{s}y\right)\to \left(p+\mathrm{bday}\left(y\right)\in a\leftrightarrow p+\mathrm{bday}\left(y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)$$
154	153	ralbidv	$$⊢a=\mathrm{bday}\left(x{+}_{s}y\right)\to \left(\forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in a\leftrightarrow \forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)$$
155	152 154	anbi12d	$$⊢a=\mathrm{bday}\left(x{+}_{s}y\right)\to \left(\left(\forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in a\wedge \forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in a\right)\leftrightarrow \left(\forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in \mathrm{bday}\left(x{+}_{s}y\right)\wedge \forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)\right)$$
156	155	elrab3	$$⊢\mathrm{bday}\left(x{+}_{s}y\right)\in \mathrm{On}\to \left(\mathrm{bday}\left(x{+}_{s}y\right)\in \left\{a\in \mathrm{On}|\left(\forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in a\wedge \forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in a\right)\right\}\leftrightarrow \left(\forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in \mathrm{bday}\left(x{+}_{s}y\right)\wedge \forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)\right)$$
157	69 156	ax-mp	$$⊢\mathrm{bday}\left(x{+}_{s}y\right)\in \left\{a\in \mathrm{On}|\left(\forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in a\wedge \forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in a\right)\right\}\leftrightarrow \left(\forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in \mathrm{bday}\left(x{+}_{s}y\right)\wedge \forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in \mathrm{bday}\left(x{+}_{s}y\right)\right)$$
158	95 150 157	sylanbrc	Could not format ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( bday ` ( x +s y ) ) e. { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) } ) : No typesetting found for |- ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( bday ` ( x +s y ) ) e. { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) } ) with typecode |-
159		intss1	$$⊢\mathrm{bday}\left(x{+}_{s}y\right)\in \left\{a\in \mathrm{On}|\left(\forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in a\wedge \forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in a\right)\right\}\to \bigcap \left\{a\in \mathrm{On}|\left(\forall q\in \mathrm{bday}\left(y\right)\mathrm{bday}\left(x\right)+q\in a\wedge \forall p\in \mathrm{bday}\left(x\right)p+\mathrm{bday}\left(y\right)\in a\right)\right\}\subseteq \mathrm{bday}\left(x{+}_{s}y\right)$$
160	158 159	syl	Could not format ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> |^| { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) } C_ ( bday ` ( x +s y ) ) ) : No typesetting found for |- ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> |^| { a e. On | ( A. q e. ( bday ` y ) ( ( bday ` x ) +no q ) e. a /\ A. p e. ( bday ` x ) ( p +no ( bday ` y ) ) e. a ) } C_ ( bday ` ( x +s y ) ) ) with typecode |-
161	29 160	eqsstrid	Could not format ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( ( bday ` x ) +no ( bday ` y ) ) C_ ( bday ` ( x +s y ) ) ) : No typesetting found for |- ( ( ( x e. On_s /\ y e. On_s ) /\ ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) ) -> ( ( bday ` x ) +no ( bday ` y ) ) C_ ( bday ` ( x +s y ) ) ) with typecode |-
162	161	ex	Could not format ( ( x e. On_s /\ y e. On_s ) -> ( ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) -> ( ( bday ` x ) +no ( bday ` y ) ) C_ ( bday ` ( x +s y ) ) ) ) : No typesetting found for |- ( ( x e. On_s /\ y e. On_s ) -> ( ( A. xO e. On_s A. yO e. On_s ( ( xO ( ( bday ` xO ) +no ( bday ` yO ) ) C_ ( bday ` ( xO +s yO ) ) ) /\ A. xO e. On_s ( xO ( ( bday ` xO ) +no ( bday ` y ) ) C_ ( bday ` ( xO +s y ) ) ) /\ A. yO e. On_s ( yO ( ( bday ` x ) +no ( bday ` yO ) ) C_ ( bday ` ( x +s yO ) ) ) ) -> ( ( bday ` x ) +no ( bday ` y ) ) C_ ( bday ` ( x +s y ) ) ) ) with typecode |-
163	8 13 16 20 25 162	ons2ind	$$⊢\left(A\in {On}_s\wedge B\in {On}_s\right)\to \mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)\subseteq \mathrm{bday}\left(A{+}_{s}B\right)$$
164	4 163	eqssd	$$⊢\left(A\in {On}_s\wedge B\in {On}_s\right)\to \mathrm{bday}\left(A{+}_{s}B\right)=\mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)$$