Theorem addsbdaylem

Description: Lemma for addsbday . (Contributed by Scott Fenton, 13-Aug-2025)

	Ref	Expression
Hypotheses	addsbdaylem.1	$$⊢\phi \to A\in \mathrm{No}$$
	addsbdaylem.2	No typesetting found for |- ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( bday ` ( A +s yO ) ) C_ ( ( bday ` A ) +no ( bday ` yO ) ) ) with typecode |-
	addsbdaylem.3	$$⊢S\subseteq L\left(B\right)\cup R\left(B\right)$$
Assertion	addsbdaylem	Could not format assertion : No typesetting found for |- ( ph -> ( bday " { z | E. yL e. S z = ( A +s yL ) } ) C_ ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		addsbdaylem.1	$$⊢\phi \to A\in \mathrm{No}$$
2		addsbdaylem.2	Could not format ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( bday ` ( A +s yO ) ) C_ ( ( bday ` A ) +no ( bday ` yO ) ) ) : No typesetting found for |- ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( bday ` ( A +s yO ) ) C_ ( ( bday ` A ) +no ( bday ` yO ) ) ) with typecode |-
3		addsbdaylem.3	$$⊢S\subseteq L\left(B\right)\cup R\left(B\right)$$
4		oveq2	Could not format ( yO = yL -> ( A +s yO ) = ( A +s yL ) ) : No typesetting found for |- ( yO = yL -> ( A +s yO ) = ( A +s yL ) ) with typecode |-
5	4	fveq2d	Could not format ( yO = yL -> ( bday ` ( A +s yO ) ) = ( bday ` ( A +s yL ) ) ) : No typesetting found for |- ( yO = yL -> ( bday ` ( A +s yO ) ) = ( bday ` ( A +s yL ) ) ) with typecode |-
6		fveq2	Could not format ( yO = yL -> ( bday ` yO ) = ( bday ` yL ) ) : No typesetting found for |- ( yO = yL -> ( bday ` yO ) = ( bday ` yL ) ) with typecode |-
7	6	oveq2d	Could not format ( yO = yL -> ( ( bday ` A ) +no ( bday ` yO ) ) = ( ( bday ` A ) +no ( bday ` yL ) ) ) : No typesetting found for |- ( yO = yL -> ( ( bday ` A ) +no ( bday ` yO ) ) = ( ( bday ` A ) +no ( bday ` yL ) ) ) with typecode |-
8	5 7	sseq12d	Could not format ( yO = yL -> ( ( bday ` ( A +s yO ) ) C_ ( ( bday ` A ) +no ( bday ` yO ) ) <-> ( bday ` ( A +s yL ) ) C_ ( ( bday ` A ) +no ( bday ` yL ) ) ) ) : No typesetting found for |- ( yO = yL -> ( ( bday ` ( A +s yO ) ) C_ ( ( bday ` A ) +no ( bday ` yO ) ) <-> ( bday ` ( A +s yL ) ) C_ ( ( bday ` A ) +no ( bday ` yL ) ) ) ) with typecode |-
9	2	adantr	Could not format ( ( ph /\ yL e. S ) -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( bday ` ( A +s yO ) ) C_ ( ( bday ` A ) +no ( bday ` yO ) ) ) : No typesetting found for |- ( ( ph /\ yL e. S ) -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( bday ` ( A +s yO ) ) C_ ( ( bday ` A ) +no ( bday ` yO ) ) ) with typecode |-
10	3	sseli	Could not format ( yL e. S -> yL e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( yL e. S -> yL e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
11	10	adantl	Could not format ( ( ph /\ yL e. S ) -> yL e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) : No typesetting found for |- ( ( ph /\ yL e. S ) -> yL e. ( ( _Left ` B ) u. ( _Right ` B ) ) ) with typecode |-
12	8 9 11	rspcdva	Could not format ( ( ph /\ yL e. S ) -> ( bday ` ( A +s yL ) ) C_ ( ( bday ` A ) +no ( bday ` yL ) ) ) : No typesetting found for |- ( ( ph /\ yL e. S ) -> ( bday ` ( A +s yL ) ) C_ ( ( bday ` A ) +no ( bday ` yL ) ) ) with typecode |-
13		lrold	$$⊢L\left(B\right)\cup R\left(B\right)=\mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
14	3 13	sseqtri	$$⊢S\subseteq \mathrm{Old}\left(\mathrm{bday}\left(B\right)\right)$$
15	14	sseli	Could not format ( yL e. S -> yL e. ( _Old ` ( bday ` B ) ) ) : No typesetting found for |- ( yL e. S -> yL e. ( _Old ` ( bday ` B ) ) ) with typecode |-
16		oldbdayim	Could not format ( yL e. ( _Old ` ( bday ` B ) ) -> ( bday ` yL ) e. ( bday ` B ) ) : No typesetting found for |- ( yL e. ( _Old ` ( bday ` B ) ) -> ( bday ` yL ) e. ( bday ` B ) ) with typecode |-
17	15 16	syl	Could not format ( yL e. S -> ( bday ` yL ) e. ( bday ` B ) ) : No typesetting found for |- ( yL e. S -> ( bday ` yL ) e. ( bday ` B ) ) with typecode |-
18	17	adantl	Could not format ( ( ph /\ yL e. S ) -> ( bday ` yL ) e. ( bday ` B ) ) : No typesetting found for |- ( ( ph /\ yL e. S ) -> ( bday ` yL ) e. ( bday ` B ) ) with typecode |-
19		bdayelon	Could not format ( bday ` yL ) e. On : No typesetting found for |- ( bday ` yL ) e. On with typecode |-
20		bdayelon	$$⊢\mathrm{bday}\left(B\right)\in \mathrm{On}$$
21		bdayelon	$$⊢\mathrm{bday}\left(A\right)\in \mathrm{On}$$
22		naddel2	Could not format ( ( ( bday ` yL ) e. On /\ ( bday ` B ) e. On /\ ( bday ` A ) e. On ) -> ( ( bday ` yL ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` yL ) e. On /\ ( bday ` B ) e. On /\ ( bday ` A ) e. On ) -> ( ( bday ` yL ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
23	19 20 21 22	mp3an	Could not format ( ( bday ` yL ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( bday ` yL ) e. ( bday ` B ) <-> ( ( bday ` A ) +no ( bday ` yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
24	18 23	sylib	Could not format ( ( ph /\ yL e. S ) -> ( ( bday ` A ) +no ( bday ` yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( ph /\ yL e. S ) -> ( ( bday ` A ) +no ( bday ` yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
25		bdayelon	Could not format ( bday ` ( A +s yL ) ) e. On : No typesetting found for |- ( bday ` ( A +s yL ) ) e. On with typecode |-
26		naddcl	$$⊢\left(\mathrm{bday}\left(A\right)\in \mathrm{On}\wedge \mathrm{bday}\left(B\right)\in \mathrm{On}\right)\to \mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)\in \mathrm{On}$$
27	21 20 26	mp2an	$$⊢\mathrm{bday}\left(A\right)+\mathrm{bday}\left(B\right)\in \mathrm{On}$$
28		ontr2	Could not format ( ( ( bday ` ( A +s yL ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( bday ` ( A +s yL ) ) C_ ( ( bday ` A ) +no ( bday ` yL ) ) /\ ( ( bday ` A ) +no ( bday ` yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) -> ( bday ` ( A +s yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ( bday ` ( A +s yL ) ) e. On /\ ( ( bday ` A ) +no ( bday ` B ) ) e. On ) -> ( ( ( bday ` ( A +s yL ) ) C_ ( ( bday ` A ) +no ( bday ` yL ) ) /\ ( ( bday ` A ) +no ( bday ` yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) -> ( bday ` ( A +s yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
29	25 27 28	mp2an	Could not format ( ( ( bday ` ( A +s yL ) ) C_ ( ( bday ` A ) +no ( bday ` yL ) ) /\ ( ( bday ` A ) +no ( bday ` yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) -> ( bday ` ( A +s yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( ( bday ` ( A +s yL ) ) C_ ( ( bday ` A ) +no ( bday ` yL ) ) /\ ( ( bday ` A ) +no ( bday ` yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) -> ( bday ` ( A +s yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
30	12 24 29	syl2anc	Could not format ( ( ph /\ yL e. S ) -> ( bday ` ( A +s yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ( ph /\ yL e. S ) -> ( bday ` ( A +s yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
31		fveq2	Could not format ( w = ( A +s yL ) -> ( bday ` w ) = ( bday ` ( A +s yL ) ) ) : No typesetting found for |- ( w = ( A +s yL ) -> ( bday ` w ) = ( bday ` ( A +s yL ) ) ) with typecode |-
32	31	eleq1d	Could not format ( w = ( A +s yL ) -> ( ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( bday ` ( A +s yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( w = ( A +s yL ) -> ( ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> ( bday ` ( A +s yL ) ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
33	30 32	syl5ibrcom	Could not format ( ( ph /\ yL e. S ) -> ( w = ( A +s yL ) -> ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( ph /\ yL e. S ) -> ( w = ( A +s yL ) -> ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
34	33	rexlimdva	Could not format ( ph -> ( E. yL e. S w = ( A +s yL ) -> ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ph -> ( E. yL e. S w = ( A +s yL ) -> ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
35	34	alrimiv	Could not format ( ph -> A. w ( E. yL e. S w = ( A +s yL ) -> ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ph -> A. w ( E. yL e. S w = ( A +s yL ) -> ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
36		eqeq1	Could not format ( z = w -> ( z = ( A +s yL ) <-> w = ( A +s yL ) ) ) : No typesetting found for |- ( z = w -> ( z = ( A +s yL ) <-> w = ( A +s yL ) ) ) with typecode |-
37	36	rexbidv	Could not format ( z = w -> ( E. yL e. S z = ( A +s yL ) <-> E. yL e. S w = ( A +s yL ) ) ) : No typesetting found for |- ( z = w -> ( E. yL e. S z = ( A +s yL ) <-> E. yL e. S w = ( A +s yL ) ) ) with typecode |-
38	37	ralab	Could not format ( A. w e. { z | E. yL e. S z = ( A +s yL ) } ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> A. w ( E. yL e. S w = ( A +s yL ) -> ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( A. w e. { z | E. yL e. S z = ( A +s yL ) } ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) <-> A. w ( E. yL e. S w = ( A +s yL ) -> ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
39	35 38	sylibr	Could not format ( ph -> A. w e. { z | E. yL e. S z = ( A +s yL ) } ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> A. w e. { z | E. yL e. S z = ( A +s yL ) } ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-
40		bdayfun	$$⊢\mathrm{Fun}\mathrm{bday}$$
41	1	adantr	Could not format ( ( ph /\ yL e. S ) -> A e. No ) : No typesetting found for |- ( ( ph /\ yL e. S ) -> A e. No ) with typecode |-
42		leftssno	$$⊢L\left(B\right)\subseteq \mathrm{No}$$
43		rightssno	$$⊢R\left(B\right)\subseteq \mathrm{No}$$
44	42 43	unssi	$$⊢L\left(B\right)\cup R\left(B\right)\subseteq \mathrm{No}$$
45	3 44	sstri	$$⊢S\subseteq \mathrm{No}$$
46	45	sseli	Could not format ( yL e. S -> yL e. No ) : No typesetting found for |- ( yL e. S -> yL e. No ) with typecode |-
47	46	adantl	Could not format ( ( ph /\ yL e. S ) -> yL e. No ) : No typesetting found for |- ( ( ph /\ yL e. S ) -> yL e. No ) with typecode |-
48	41 47	addscld	Could not format ( ( ph /\ yL e. S ) -> ( A +s yL ) e. No ) : No typesetting found for |- ( ( ph /\ yL e. S ) -> ( A +s yL ) e. No ) with typecode |-
49		eleq1	Could not format ( z = ( A +s yL ) -> ( z e. No <-> ( A +s yL ) e. No ) ) : No typesetting found for |- ( z = ( A +s yL ) -> ( z e. No <-> ( A +s yL ) e. No ) ) with typecode |-
50	48 49	syl5ibrcom	Could not format ( ( ph /\ yL e. S ) -> ( z = ( A +s yL ) -> z e. No ) ) : No typesetting found for |- ( ( ph /\ yL e. S ) -> ( z = ( A +s yL ) -> z e. No ) ) with typecode |-
51	50	rexlimdva	Could not format ( ph -> ( E. yL e. S z = ( A +s yL ) -> z e. No ) ) : No typesetting found for |- ( ph -> ( E. yL e. S z = ( A +s yL ) -> z e. No ) ) with typecode |-
52	51	abssdv	Could not format ( ph -> { z | E. yL e. S z = ( A +s yL ) } C_ No ) : No typesetting found for |- ( ph -> { z | E. yL e. S z = ( A +s yL ) } C_ No ) with typecode |-
53		bdaydm	$$⊢\mathrm{dom}\mathrm{bday}=\mathrm{No}$$
54	52 53	sseqtrrdi	Could not format ( ph -> { z | E. yL e. S z = ( A +s yL ) } C_ dom bday ) : No typesetting found for |- ( ph -> { z | E. yL e. S z = ( A +s yL ) } C_ dom bday ) with typecode |-
55		funimass4	Could not format ( ( Fun bday /\ { z | E. yL e. S z = ( A +s yL ) } C_ dom bday ) -> ( ( bday " { z | E. yL e. S z = ( A +s yL ) } ) C_ ( ( bday ` A ) +no ( bday ` B ) ) <-> A. w e. { z | E. yL e. S z = ( A +s yL ) } ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ( Fun bday /\ { z | E. yL e. S z = ( A +s yL ) } C_ dom bday ) -> ( ( bday " { z | E. yL e. S z = ( A +s yL ) } ) C_ ( ( bday ` A ) +no ( bday ` B ) ) <-> A. w e. { z | E. yL e. S z = ( A +s yL ) } ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
56	40 54 55	sylancr	Could not format ( ph -> ( ( bday " { z | E. yL e. S z = ( A +s yL ) } ) C_ ( ( bday ` A ) +no ( bday ` B ) ) <-> A. w e. { z | E. yL e. S z = ( A +s yL ) } ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) : No typesetting found for |- ( ph -> ( ( bday " { z | E. yL e. S z = ( A +s yL ) } ) C_ ( ( bday ` A ) +no ( bday ` B ) ) <-> A. w e. { z | E. yL e. S z = ( A +s yL ) } ( bday ` w ) e. ( ( bday ` A ) +no ( bday ` B ) ) ) ) with typecode |-
57	39 56	mpbird	Could not format ( ph -> ( bday " { z | E. yL e. S z = ( A +s yL ) } ) C_ ( ( bday ` A ) +no ( bday ` B ) ) ) : No typesetting found for |- ( ph -> ( bday " { z | E. yL e. S z = ( A +s yL ) } ) C_ ( ( bday ` A ) +no ( bday ` B ) ) ) with typecode |-