Metamath Proof Explorer

Theorem addsbdaylem

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

Ref Expression
Hypotheses addsbdaylem.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
addsbdaylem.2 ⊢ ( 𝜑 → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( bday ‘ ( 𝐴 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝑂 ) ) )
addsbdaylem.3 ⊢ 𝑆 ⊆ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) )
Assertion addsbdaylem ( 𝜑 → ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) } ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 addsbdaylem.1 ⊢ ( 𝜑 → 𝐴 ∈ No )
2 addsbdaylem.2 ⊢ ( 𝜑 → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( bday ‘ ( 𝐴 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝑂 ) ) )
3 addsbdaylem.3 ⊢ 𝑆 ⊆ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) )
4 oveq2 ⊢ ( 𝑦𝑂 = 𝑦𝐿 → ( 𝐴 +s 𝑦𝑂 ) = ( 𝐴 +s 𝑦𝐿 ) )
5 4 fveq2d ⊢ ( 𝑦𝑂 = 𝑦𝐿 → ( bday ‘ ( 𝐴 +s 𝑦𝑂 ) ) = ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) )
6 fveq2 ⊢ ( 𝑦𝑂 = 𝑦𝐿 → ( bday ‘ 𝑦𝑂 ) = ( bday ‘ 𝑦𝐿 ) )
7 6 oveq2d ⊢ ( 𝑦𝑂 = 𝑦𝐿 → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝑂 ) ) = ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝐿 ) ) )
8 5 7 sseq12d ⊢ ( 𝑦𝑂 = 𝑦𝐿 → ( ( bday ‘ ( 𝐴 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝑂 ) ) ↔ ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝐿 ) ) ) )
9 2 adantr ⊢ ( ( 𝜑 ∧ 𝑦𝐿 ∈ 𝑆 ) → ∀ 𝑦𝑂 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ( bday ‘ ( 𝐴 +s 𝑦𝑂 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝑂 ) ) )
10 3 sseli ⊢ ( 𝑦𝐿 ∈ 𝑆 → 𝑦𝐿 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑦𝐿 ∈ 𝑆 ) → 𝑦𝐿 ∈ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) )
12 8 9 11 rspcdva ⊢ ( ( 𝜑 ∧ 𝑦𝐿 ∈ 𝑆 ) → ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝐿 ) ) )
13 lrold ⊢ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) = ( O ‘ ( bday ‘ 𝐵 ) )
14 3 13 sseqtri ⊢ 𝑆 ⊆ ( O ‘ ( bday ‘ 𝐵 ) )
15 14 sseli ⊢ ( 𝑦𝐿 ∈ 𝑆 → 𝑦𝐿 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) )
16 oldbdayim ⊢ ( 𝑦𝐿 ∈ ( O ‘ ( bday ‘ 𝐵 ) ) → ( bday ‘ 𝑦𝐿 ) ∈ ( bday ‘ 𝐵 ) )
17 15 16 syl ⊢ ( 𝑦𝐿 ∈ 𝑆 → ( bday ‘ 𝑦𝐿 ) ∈ ( bday ‘ 𝐵 ) )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑦𝐿 ∈ 𝑆 ) → ( bday ‘ 𝑦𝐿 ) ∈ ( bday ‘ 𝐵 ) )
19 bdayelon ⊢ ( bday ‘ 𝑦𝐿 ) ∈ On
20 bdayelon ⊢ ( bday ‘ 𝐵 ) ∈ On
21 bdayelon ⊢ ( bday ‘ 𝐴 ) ∈ On
22 naddel2 ⊢ ( ( ( bday ‘ 𝑦𝐿 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ∧ ( bday ‘ 𝐴 ) ∈ On ) → ( ( bday ‘ 𝑦𝐿 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝐿 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
23 19 20 21 22 mp3an ⊢ ( ( bday ‘ 𝑦𝐿 ) ∈ ( bday ‘ 𝐵 ) ↔ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝐿 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
24 18 23 sylib ⊢ ( ( 𝜑 ∧ 𝑦𝐿 ∈ 𝑆 ) → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝐿 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
25 bdayelon ⊢ ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) ∈ On
26 naddcl ⊢ ( ( ( bday ‘ 𝐴 ) ∈ On ∧ ( bday ‘ 𝐵 ) ∈ On ) → ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On )
27 21 20 26 mp2an ⊢ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On
28 ontr2 ⊢ ( ( ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) ∈ On ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ∈ On ) → ( ( ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝐿 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝐿 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) → ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
29 25 27 28 mp2an ⊢ ( ( ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝐿 ) ) ∧ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝑦𝐿 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) → ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
30 12 24 29 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦𝐿 ∈ 𝑆 ) → ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
31 fveq2 ⊢ ( 𝑤 = ( 𝐴 +s 𝑦𝐿 ) → ( bday ‘ 𝑤 ) = ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) )
32 31 eleq1d ⊢ ( 𝑤 = ( 𝐴 +s 𝑦𝐿 ) → ( ( bday ‘ 𝑤 ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ( bday ‘ ( 𝐴 +s 𝑦𝐿 ) ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
33 30 32 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑦𝐿 ∈ 𝑆 ) → ( 𝑤 = ( 𝐴 +s 𝑦𝐿 ) → ( bday ‘ 𝑤 ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
34 33 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑦𝐿 ∈ 𝑆 𝑤 = ( 𝐴 +s 𝑦𝐿 ) → ( bday ‘ 𝑤 ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
35 34 alrimiv ⊢ ( 𝜑 → ∀ 𝑤 ( ∃ 𝑦𝐿 ∈ 𝑆 𝑤 = ( 𝐴 +s 𝑦𝐿 ) → ( bday ‘ 𝑤 ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
36 eqeq1 ⊢ ( 𝑧 = 𝑤 → ( 𝑧 = ( 𝐴 +s 𝑦𝐿 ) ↔ 𝑤 = ( 𝐴 +s 𝑦𝐿 ) ) )
37 36 rexbidv ⊢ ( 𝑧 = 𝑤 → ( ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) ↔ ∃ 𝑦𝐿 ∈ 𝑆 𝑤 = ( 𝐴 +s 𝑦𝐿 ) ) )
38 37 ralab ⊢ ( ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) } ( bday ‘ 𝑤 ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ∀ 𝑤 ( ∃ 𝑦𝐿 ∈ 𝑆 𝑤 = ( 𝐴 +s 𝑦𝐿 ) → ( bday ‘ 𝑤 ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
39 35 38 sylibr ⊢ ( 𝜑 → ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) } ( bday ‘ 𝑤 ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )
40 bdayfun ⊢ Fun bday
41 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦𝐿 ∈ 𝑆 ) → 𝐴 ∈ No )
42 leftssno ⊢ ( L ‘ 𝐵 ) ⊆ No
43 rightssno ⊢ ( R ‘ 𝐵 ) ⊆ No
44 42 43 unssi ⊢ ( ( L ‘ 𝐵 ) ∪ ( R ‘ 𝐵 ) ) ⊆ No
45 3 44 sstri ⊢ 𝑆 ⊆ No
46 45 sseli ⊢ ( 𝑦𝐿 ∈ 𝑆 → 𝑦𝐿 ∈ No )
47 46 adantl ⊢ ( ( 𝜑 ∧ 𝑦𝐿 ∈ 𝑆 ) → 𝑦𝐿 ∈ No )
48 41 47 addscld ⊢ ( ( 𝜑 ∧ 𝑦𝐿 ∈ 𝑆 ) → ( 𝐴 +s 𝑦𝐿 ) ∈ No )
49 eleq1 ⊢ ( 𝑧 = ( 𝐴 +s 𝑦𝐿 ) → ( 𝑧 ∈ No ↔ ( 𝐴 +s 𝑦𝐿 ) ∈ No ) )
50 48 49 syl5ibrcom ⊢ ( ( 𝜑 ∧ 𝑦𝐿 ∈ 𝑆 ) → ( 𝑧 = ( 𝐴 +s 𝑦𝐿 ) → 𝑧 ∈ No ) )
51 50 rexlimdva ⊢ ( 𝜑 → ( ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) → 𝑧 ∈ No ) )
52 51 abssdv ⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) } ⊆ No )
53 bdaydm ⊢ dom bday = No
54 52 53 sseqtrrdi ⊢ ( 𝜑 → { 𝑧 ∣ ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) } ⊆ dom bday )
55 funimass4 ⊢ ( ( Fun bday ∧ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) } ⊆ dom bday ) → ( ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) } ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) } ( bday ‘ 𝑤 ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
56 40 54 55 sylancr ⊢ ( 𝜑 → ( ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) } ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ↔ ∀ 𝑤 ∈ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) } ( bday ‘ 𝑤 ) ∈ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) ) )
57 39 56 mpbird ⊢ ( 𝜑 → ( bday “ { 𝑧 ∣ ∃ 𝑦𝐿 ∈ 𝑆 𝑧 = ( 𝐴 +s 𝑦𝐿 ) } ) ⊆ ( ( bday ‘ 𝐴 ) +no ( bday ‘ 𝐵 ) ) )