Metamath Proof Explorer

Theorem addsbdaylem

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

Ref Expression
Hypotheses addsbdaylem.1 
|- ( ph -> A e. No )
addsbdaylem.2 
|- ( ph -> A. yO e. ( ( _Left ` B ) u. ( _Right ` B ) ) ( bday ` ( A +s yO ) ) C_ ( ( bday ` A ) +no ( bday ` yO ) ) )
addsbdaylem.3 
|- S C_ ( ( _Left ` B ) u. ( _Right ` B ) )
Assertion addsbdaylem 
|- ( ph -> ( bday " { z | E. yL e. S z = ( A +s yL ) } ) C_ ( ( bday ` A ) +no ( bday ` B ) ) )

Proof

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