Step | Hyp | Ref
| Expression |
1 | | oveq2 7453 |
. . . . . . . . . 10
⊢ (𝑦𝑂 = 𝑦𝐿 →
(𝐴 +s 𝑦𝑂) = (𝐴 +s 𝑦𝐿)) |
2 | 1 | fveq2d 6923 |
. . . . . . . . 9
⊢ (𝑦𝑂 = 𝑦𝐿 →
( bday ‘(𝐴 +s 𝑦𝑂)) = ( bday ‘(𝐴 +s 𝑦𝐿))) |
3 | | fveq2 6919 |
. . . . . . . . . 10
⊢ (𝑦𝑂 = 𝑦𝐿 →
( bday ‘𝑦𝑂) = ( bday ‘𝑦𝐿)) |
4 | 3 | oveq2d 7461 |
. . . . . . . . 9
⊢ (𝑦𝑂 = 𝑦𝐿 →
(( bday ‘𝐴) +no ( bday
‘𝑦𝑂)) = (( bday ‘𝐴) +no ( bday
‘𝑦𝐿))) |
5 | 2, 4 | sseq12d 4036 |
. . . . . . . 8
⊢ (𝑦𝑂 = 𝑦𝐿 →
(( bday ‘(𝐴 +s 𝑦𝑂)) ⊆ (( bday ‘𝐴) +no ( bday
‘𝑦𝑂)) ↔ ( bday ‘(𝐴 +s 𝑦𝐿)) ⊆ (( bday ‘𝐴) +no ( bday
‘𝑦𝐿)))) |
6 | | addsbdaylem.2 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))( bday
‘(𝐴
+s 𝑦𝑂)) ⊆ (( bday ‘𝐴) +no ( bday
‘𝑦𝑂))) |
7 | 6 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦𝐿 ∈ 𝑆) → ∀𝑦𝑂 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))( bday
‘(𝐴
+s 𝑦𝑂)) ⊆ (( bday ‘𝐴) +no ( bday
‘𝑦𝑂))) |
8 | | addsbdaylem.3 |
. . . . . . . . . 10
⊢ 𝑆 ⊆ (( L ‘𝐵) ∪ ( R ‘𝐵)) |
9 | 8 | sseli 3998 |
. . . . . . . . 9
⊢ (𝑦𝐿 ∈ 𝑆 → 𝑦𝐿 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))) |
10 | 9 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦𝐿 ∈ 𝑆) → 𝑦𝐿 ∈ (( L ‘𝐵) ∪ ( R ‘𝐵))) |
11 | 5, 7, 10 | rspcdva 3632 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦𝐿 ∈ 𝑆) → ( bday
‘(𝐴
+s 𝑦𝐿)) ⊆ (( bday ‘𝐴) +no ( bday
‘𝑦𝐿))) |
12 | | lrold 27944 |
. . . . . . . . . . . 12
⊢ (( L
‘𝐵) ∪ ( R
‘𝐵)) = ( O
‘( bday ‘𝐵)) |
13 | 8, 12 | sseqtri 4039 |
. . . . . . . . . . 11
⊢ 𝑆 ⊆ ( O ‘( bday ‘𝐵)) |
14 | 13 | sseli 3998 |
. . . . . . . . . 10
⊢ (𝑦𝐿 ∈ 𝑆 → 𝑦𝐿 ∈ ( O ‘( bday ‘𝐵))) |
15 | | oldbdayim 27936 |
. . . . . . . . . 10
⊢ (𝑦𝐿 ∈ ( O
‘( bday ‘𝐵)) → ( bday
‘𝑦𝐿) ∈ ( bday ‘𝐵)) |
16 | 14, 15 | syl 17 |
. . . . . . . . 9
⊢ (𝑦𝐿 ∈ 𝑆 → (
bday ‘𝑦𝐿) ∈ ( bday ‘𝐵)) |
17 | 16 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦𝐿 ∈ 𝑆) → ( bday
‘𝑦𝐿) ∈ ( bday ‘𝐵)) |
18 | | bdayelon 27830 |
. . . . . . . . 9
⊢ ( bday ‘𝑦𝐿) ∈
On |
19 | | bdayelon 27830 |
. . . . . . . . 9
⊢ ( bday ‘𝐵) ∈ On |
20 | | bdayelon 27830 |
. . . . . . . . 9
⊢ ( bday ‘𝐴) ∈ On |
21 | | naddel2 8740 |
. . . . . . . . 9
⊢ ((( bday ‘𝑦𝐿) ∈ On ∧ ( bday ‘𝐵) ∈ On ∧ (
bday ‘𝐴)
∈ On) → (( bday ‘𝑦𝐿) ∈
( bday ‘𝐵) ↔ (( bday
‘𝐴) +no ( bday ‘𝑦𝐿)) ∈ (( bday ‘𝐴) +no ( bday
‘𝐵)))) |
22 | 18, 19, 20, 21 | mp3an 1461 |
. . . . . . . 8
⊢ (( bday ‘𝑦𝐿) ∈ ( bday ‘𝐵) ↔ (( bday
‘𝐴) +no ( bday ‘𝑦𝐿)) ∈ (( bday ‘𝐴) +no ( bday
‘𝐵))) |
23 | 17, 22 | sylib 218 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦𝐿 ∈ 𝑆) → (( bday
‘𝐴) +no ( bday ‘𝑦𝐿)) ∈ (( bday ‘𝐴) +no ( bday
‘𝐵))) |
24 | | bdayelon 27830 |
. . . . . . . 8
⊢ ( bday ‘(𝐴 +s 𝑦𝐿)) ∈
On |
25 | | naddcl 8729 |
. . . . . . . . 9
⊢ ((( bday ‘𝐴) ∈ On ∧ (
bday ‘𝐵)
∈ On) → (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) |
26 | 20, 19, 25 | mp2an 691 |
. . . . . . . 8
⊢ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On |
27 | | ontr2 6441 |
. . . . . . . 8
⊢ ((( bday ‘(𝐴 +s 𝑦𝐿)) ∈ On ∧ (( bday ‘𝐴) +no ( bday
‘𝐵)) ∈
On) → ((( bday ‘(𝐴 +s 𝑦𝐿)) ⊆ (( bday ‘𝐴) +no ( bday
‘𝑦𝐿)) ∧ (( bday ‘𝐴) +no ( bday
‘𝑦𝐿)) ∈ (( bday ‘𝐴) +no ( bday
‘𝐵))) →
( bday ‘(𝐴 +s 𝑦𝐿)) ∈ (( bday ‘𝐴) +no ( bday
‘𝐵)))) |
28 | 24, 26, 27 | mp2an 691 |
. . . . . . 7
⊢ ((( bday ‘(𝐴 +s 𝑦𝐿)) ⊆ (( bday ‘𝐴) +no ( bday
‘𝑦𝐿)) ∧ (( bday ‘𝐴) +no ( bday
‘𝑦𝐿)) ∈ (( bday ‘𝐴) +no ( bday
‘𝐵))) →
( bday ‘(𝐴 +s 𝑦𝐿)) ∈ (( bday ‘𝐴) +no ( bday
‘𝐵))) |
29 | 11, 23, 28 | syl2anc 583 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦𝐿 ∈ 𝑆) → ( bday
‘(𝐴
+s 𝑦𝐿)) ∈ (( bday ‘𝐴) +no ( bday
‘𝐵))) |
30 | | fveq2 6919 |
. . . . . . 7
⊢ (𝑤 = (𝐴 +s 𝑦𝐿) → ( bday ‘𝑤) = ( bday
‘(𝐴
+s 𝑦𝐿))) |
31 | 30 | eleq1d 2823 |
. . . . . 6
⊢ (𝑤 = (𝐴 +s 𝑦𝐿) → (( bday ‘𝑤) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)) ↔ ( bday
‘(𝐴
+s 𝑦𝐿)) ∈ (( bday ‘𝐴) +no ( bday
‘𝐵)))) |
32 | 29, 31 | syl5ibrcom 247 |
. . . . 5
⊢ ((𝜑 ∧ 𝑦𝐿 ∈ 𝑆) → (𝑤 = (𝐴 +s 𝑦𝐿) → ( bday ‘𝑤) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
33 | 32 | rexlimdva 3157 |
. . . 4
⊢ (𝜑 → (∃𝑦𝐿 ∈ 𝑆 𝑤 = (𝐴 +s 𝑦𝐿) → ( bday ‘𝑤) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
34 | 33 | alrimiv 1926 |
. . 3
⊢ (𝜑 → ∀𝑤(∃𝑦𝐿 ∈ 𝑆 𝑤 = (𝐴 +s 𝑦𝐿) → ( bday ‘𝑤) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
35 | | eqeq1 2738 |
. . . . 5
⊢ (𝑧 = 𝑤 → (𝑧 = (𝐴 +s 𝑦𝐿) ↔ 𝑤 = (𝐴 +s 𝑦𝐿))) |
36 | 35 | rexbidv 3181 |
. . . 4
⊢ (𝑧 = 𝑤 → (∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿) ↔ ∃𝑦𝐿 ∈ 𝑆 𝑤 = (𝐴 +s 𝑦𝐿))) |
37 | 36 | ralab 3707 |
. . 3
⊢
(∀𝑤 ∈
{𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} (
bday ‘𝑤)
∈ (( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
∀𝑤(∃𝑦𝐿 ∈ 𝑆 𝑤 = (𝐴 +s 𝑦𝐿) → ( bday ‘𝑤) ∈ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
38 | 34, 37 | sylibr 234 |
. 2
⊢ (𝜑 → ∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} (
bday ‘𝑤)
∈ (( bday ‘𝐴) +no ( bday
‘𝐵))) |
39 | | bdayfun 27826 |
. . 3
⊢ Fun bday |
40 | | addsbdaylem.1 |
. . . . . . . . 9
⊢ (𝜑 → 𝐴 ∈ No
) |
41 | 40 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦𝐿 ∈ 𝑆) → 𝐴 ∈ No
) |
42 | | leftssno 27928 |
. . . . . . . . . . . 12
⊢ ( L
‘𝐵) ⊆ No |
43 | | rightssno 27929 |
. . . . . . . . . . . 12
⊢ ( R
‘𝐵) ⊆ No |
44 | 42, 43 | unssi 4208 |
. . . . . . . . . . 11
⊢ (( L
‘𝐵) ∪ ( R
‘𝐵)) ⊆ No |
45 | 8, 44 | sstri 4012 |
. . . . . . . . . 10
⊢ 𝑆 ⊆
No |
46 | 45 | sseli 3998 |
. . . . . . . . 9
⊢ (𝑦𝐿 ∈ 𝑆 → 𝑦𝐿 ∈ No ) |
47 | 46 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦𝐿 ∈ 𝑆) → 𝑦𝐿 ∈ No ) |
48 | 41, 47 | addscld 28022 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦𝐿 ∈ 𝑆) → (𝐴 +s 𝑦𝐿) ∈ No ) |
49 | | eleq1 2826 |
. . . . . . 7
⊢ (𝑧 = (𝐴 +s 𝑦𝐿) → (𝑧 ∈
No ↔ (𝐴
+s 𝑦𝐿) ∈ No )) |
50 | 48, 49 | syl5ibrcom 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦𝐿 ∈ 𝑆) → (𝑧 = (𝐴 +s 𝑦𝐿) → 𝑧 ∈
No )) |
51 | 50 | rexlimdva 3157 |
. . . . 5
⊢ (𝜑 → (∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿) → 𝑧 ∈
No )) |
52 | 51 | abssdv 4085 |
. . . 4
⊢ (𝜑 → {𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} ⊆ No ) |
53 | | bdaydm 27828 |
. . . 4
⊢ dom bday = No
|
54 | 52, 53 | sseqtrrdi 4054 |
. . 3
⊢ (𝜑 → {𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} ⊆ dom bday ) |
55 | | funimass4 6985 |
. . 3
⊢ ((Fun
bday ∧ {𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} ⊆ dom bday ) → (( bday
“ {𝑧 ∣
∃𝑦𝐿
∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ (( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} (
bday ‘𝑤)
∈ (( bday ‘𝐴) +no ( bday
‘𝐵)))) |
56 | 39, 54, 55 | sylancr 586 |
. 2
⊢ (𝜑 → ((
bday “ {𝑧
∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ (( bday ‘𝐴) +no ( bday
‘𝐵)) ↔
∀𝑤 ∈ {𝑧 ∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)} (
bday ‘𝑤)
∈ (( bday ‘𝐴) +no ( bday
‘𝐵)))) |
57 | 38, 56 | mpbird 257 |
1
⊢ (𝜑 → (
bday “ {𝑧
∣ ∃𝑦𝐿 ∈ 𝑆 𝑧 = (𝐴 +s 𝑦𝐿)}) ⊆ (( bday ‘𝐴) +no ( bday
‘𝐵))) |