Step | Hyp | Ref
| Expression |
1 | | fvoveq1 7468 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → ( bday ‘(𝑥 +s 𝑦)) = ( bday
‘(𝑥𝑂 +s 𝑦))) |
2 | | fveq2 6919 |
. . . 4
⊢ (𝑥 = 𝑥𝑂 → ( bday ‘𝑥) = ( bday
‘𝑥𝑂)) |
3 | 2 | oveq1d 7460 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (( bday ‘𝑥) +no ( bday
‘𝑦)) = (( bday ‘𝑥𝑂) +no ( bday ‘𝑦))) |
4 | 1, 3 | sseq12d 4036 |
. 2
⊢ (𝑥 = 𝑥𝑂 → (( bday ‘(𝑥 +s 𝑦)) ⊆ (( bday
‘𝑥) +no ( bday ‘𝑦)) ↔ ( bday
‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)))) |
5 | | oveq2 7453 |
. . . 4
⊢ (𝑦 = 𝑦𝑂 → (𝑥𝑂
+s 𝑦) = (𝑥𝑂
+s 𝑦𝑂)) |
6 | 5 | fveq2d 6923 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → ( bday ‘(𝑥𝑂 +s 𝑦)) = (
bday ‘(𝑥𝑂 +s 𝑦𝑂))) |
7 | | fveq2 6919 |
. . . 4
⊢ (𝑦 = 𝑦𝑂 → ( bday ‘𝑦) = ( bday
‘𝑦𝑂)) |
8 | 7 | oveq2d 7461 |
. . 3
⊢ (𝑦 = 𝑦𝑂 → (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) = (( bday
‘𝑥𝑂) +no ( bday ‘𝑦𝑂))) |
9 | 6, 8 | sseq12d 4036 |
. 2
⊢ (𝑦 = 𝑦𝑂 → (( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ↔ ( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)))) |
10 | | fvoveq1 7468 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → ( bday ‘(𝑥 +s 𝑦𝑂)) = ( bday ‘(𝑥𝑂 +s 𝑦𝑂))) |
11 | 2 | oveq1d 7460 |
. . 3
⊢ (𝑥 = 𝑥𝑂 → (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)) = (( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂))) |
12 | 10, 11 | sseq12d 4036 |
. 2
⊢ (𝑥 = 𝑥𝑂 → (( bday ‘(𝑥 +s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)) ↔ ( bday ‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)))) |
13 | | fvoveq1 7468 |
. . 3
⊢ (𝑥 = 𝐴 → ( bday
‘(𝑥
+s 𝑦)) = ( bday ‘(𝐴 +s 𝑦))) |
14 | | fveq2 6919 |
. . . 4
⊢ (𝑥 = 𝐴 → ( bday
‘𝑥) = ( bday ‘𝐴)) |
15 | 14 | oveq1d 7460 |
. . 3
⊢ (𝑥 = 𝐴 → (( bday
‘𝑥) +no ( bday ‘𝑦)) = (( bday
‘𝐴) +no ( bday ‘𝑦))) |
16 | 13, 15 | sseq12d 4036 |
. 2
⊢ (𝑥 = 𝐴 → (( bday
‘(𝑥
+s 𝑦)) ⊆
(( bday ‘𝑥) +no ( bday
‘𝑦)) ↔
( bday ‘(𝐴 +s 𝑦)) ⊆ (( bday
‘𝐴) +no ( bday ‘𝑦)))) |
17 | | oveq2 7453 |
. . . 4
⊢ (𝑦 = 𝐵 → (𝐴 +s 𝑦) = (𝐴 +s 𝐵)) |
18 | 17 | fveq2d 6923 |
. . 3
⊢ (𝑦 = 𝐵 → ( bday
‘(𝐴
+s 𝑦)) = ( bday ‘(𝐴 +s 𝐵))) |
19 | | fveq2 6919 |
. . . 4
⊢ (𝑦 = 𝐵 → ( bday
‘𝑦) = ( bday ‘𝐵)) |
20 | 19 | oveq2d 7461 |
. . 3
⊢ (𝑦 = 𝐵 → (( bday
‘𝐴) +no ( bday ‘𝑦)) = (( bday
‘𝐴) +no ( bday ‘𝐵))) |
21 | 18, 20 | sseq12d 4036 |
. 2
⊢ (𝑦 = 𝐵 → (( bday
‘(𝐴
+s 𝑦)) ⊆
(( bday ‘𝐴) +no ( bday
‘𝑦)) ↔
( bday ‘(𝐴 +s 𝐵)) ⊆ (( bday
‘𝐴) +no ( bday ‘𝐵)))) |
22 | | addsval2 28005 |
. . . . . 6
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → (𝑥 +s 𝑦) = (({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) |s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) |
23 | 22 | fveq2d 6923 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → ( bday
‘(𝑥
+s 𝑦)) = ( bday ‘(({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) |s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})))) |
24 | 23 | adantr 480 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday ‘(𝑥 +s 𝑦)) = ( bday
‘(({𝑧 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) |s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})))) |
25 | | simpl 482 |
. . . . . 6
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → 𝑥 ∈ No
) |
26 | | simpr 484 |
. . . . . 6
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → 𝑦 ∈ No
) |
27 | 25, 26 | addscut2 28021 |
. . . . 5
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → ({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) <<s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) |
28 | | imaundi 6180 |
. . . . . . 7
⊢ ( bday “ (({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) ∪ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) = (( bday “ ({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) ∪ ( bday “ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) |
29 | | imaundi 6180 |
. . . . . . . 8
⊢ ( bday “ ({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) = (( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) |
30 | | imaundi 6180 |
. . . . . . . 8
⊢ ( bday “ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) = (( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) |
31 | 29, 30 | uneq12i 4183 |
. . . . . . 7
⊢ (( bday “ ({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) ∪ ( bday “ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) = ((( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) ∪ (( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) |
32 | 28, 31 | eqtri 2762 |
. . . . . 6
⊢ ( bday “ (({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) ∪ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) = ((( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) ∪ (( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) |
33 | | simplr 768 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → 𝑦 ∈
No ) |
34 | | simpr2 1195 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦))) |
35 | | simplr 768 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → 𝑦 ∈ No
) |
36 | | leftssno 27928 |
. . . . . . . . . . . . . . . . . . 19
⊢ ( L
‘𝑥) ⊆ No |
37 | | rightssno 27929 |
. . . . . . . . . . . . . . . . . . 19
⊢ ( R
‘𝑥) ⊆ No |
38 | 36, 37 | unssi 4208 |
. . . . . . . . . . . . . . . . . 18
⊢ (( L
‘𝑥) ∪ ( R
‘𝑥)) ⊆ No |
39 | 38 | sseli 3998 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥)) → 𝑥𝑂 ∈
No ) |
40 | 39 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → 𝑥𝑂 ∈ No ) |
41 | 35, 40 | addscomd 28009 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → (𝑦 +s 𝑥𝑂) = (𝑥𝑂 +s 𝑦)) |
42 | 41 | fveq2d 6923 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → ( bday ‘(𝑦 +s 𝑥𝑂)) = ( bday ‘(𝑥𝑂 +s 𝑦))) |
43 | | bdayelon 27830 |
. . . . . . . . . . . . . . . 16
⊢ ( bday ‘𝑦) ∈ On |
44 | | bdayelon 27830 |
. . . . . . . . . . . . . . . 16
⊢ ( bday ‘𝑥𝑂) ∈
On |
45 | | naddcom 8734 |
. . . . . . . . . . . . . . . 16
⊢ ((( bday ‘𝑦) ∈ On ∧ (
bday ‘𝑥𝑂) ∈ On) →
(( bday ‘𝑦) +no ( bday
‘𝑥𝑂)) = (( bday ‘𝑥𝑂) +no ( bday ‘𝑦))) |
46 | 43, 44, 45 | mp2an 691 |
. . . . . . . . . . . . . . 15
⊢ (( bday ‘𝑦) +no ( bday
‘𝑥𝑂)) = (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) |
47 | 46 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → (( bday ‘𝑦) +no ( bday
‘𝑥𝑂)) = (( bday ‘𝑥𝑂) +no ( bday ‘𝑦))) |
48 | 42, 47 | sseq12d 4036 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))) → (( bday ‘(𝑦 +s 𝑥𝑂)) ⊆ (( bday ‘𝑦) +no ( bday
‘𝑥𝑂)) ↔ ( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)))) |
49 | 48 | ralbidva 3178 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))( bday
‘(𝑦
+s 𝑥𝑂)) ⊆ (( bday ‘𝑦) +no ( bday
‘𝑥𝑂)) ↔ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)))) |
50 | 49 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) →
(∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))( bday
‘(𝑦
+s 𝑥𝑂)) ⊆ (( bday ‘𝑦) +no ( bday
‘𝑥𝑂)) ↔ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)))) |
51 | 34, 50 | mpbird 257 |
. . . . . . . . . 10
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑦 +s 𝑥𝑂)) ⊆ (( bday ‘𝑦) +no ( bday
‘𝑥𝑂))) |
52 | | ssun1 4195 |
. . . . . . . . . 10
⊢ ( L
‘𝑥) ⊆ (( L
‘𝑥) ∪ ( R
‘𝑥)) |
53 | 33, 51, 52 | addsbdaylem 28058 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑦 +s 𝑥𝐿)}) ⊆ (( bday ‘𝑦) +no ( bday
‘𝑥))) |
54 | 36 | sseli 3998 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥𝐿 ∈ ( L
‘𝑥) → 𝑥𝐿 ∈
No ) |
55 | 54 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝐿 ∈ ( L ‘𝑥)) → 𝑥𝐿 ∈ No ) |
56 | | simplr 768 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝐿 ∈ ( L ‘𝑥)) → 𝑦 ∈ No
) |
57 | 55, 56 | addscomd 28009 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝐿 ∈ ( L ‘𝑥)) → (𝑥𝐿 +s 𝑦) = (𝑦 +s 𝑥𝐿)) |
58 | 57 | eqeq2d 2745 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝐿 ∈ ( L ‘𝑥)) → (𝑧 = (𝑥𝐿 +s 𝑦) ↔ 𝑧 = (𝑦 +s 𝑥𝐿))) |
59 | 58 | rexbidva 3179 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → (∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦) ↔ ∃𝑥𝐿 ∈ ( L
‘𝑥)𝑧 = (𝑦 +s 𝑥𝐿))) |
60 | 59 | abbidv 2805 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} = {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑦 +s 𝑥𝐿)}) |
61 | 60 | imaeq2d 6088 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → ( bday
“ {𝑧 ∣
∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) = (
bday “ {𝑧
∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑦 +s 𝑥𝐿)})) |
62 | 61 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) = (
bday “ {𝑧
∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑦 +s 𝑥𝐿)})) |
63 | | bdayelon 27830 |
. . . . . . . . . . 11
⊢ ( bday ‘𝑥) ∈ On |
64 | | naddcom 8734 |
. . . . . . . . . . 11
⊢ ((( bday ‘𝑥) ∈ On ∧ (
bday ‘𝑦)
∈ On) → (( bday ‘𝑥) +no (
bday ‘𝑦)) =
(( bday ‘𝑦) +no ( bday
‘𝑥))) |
65 | 63, 43, 64 | mp2an 691 |
. . . . . . . . . 10
⊢ (( bday ‘𝑥) +no ( bday
‘𝑦)) = (( bday ‘𝑦) +no ( bday
‘𝑥)) |
66 | 65 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → (( bday ‘𝑥) +no ( bday
‘𝑦)) = (( bday ‘𝑦) +no ( bday
‘𝑥))) |
67 | 53, 62, 66 | 3sstr4d 4050 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) |
68 | | simpll 766 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → 𝑥 ∈
No ) |
69 | | simpr3 1196 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ∀𝑦𝑂 ∈ (( L
‘𝑦) ∪ ( R
‘𝑦))( bday ‘(𝑥 +s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂))) |
70 | | ssun1 4195 |
. . . . . . . . 9
⊢ ( L
‘𝑦) ⊆ (( L
‘𝑦) ∪ ( R
‘𝑦)) |
71 | 68, 69, 70 | addsbdaylem 28058 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) |
72 | 67, 71 | unssd 4209 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → (( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) |
73 | | ssun2 4196 |
. . . . . . . . . 10
⊢ ( R
‘𝑥) ⊆ (( L
‘𝑥) ∪ ( R
‘𝑥)) |
74 | 33, 51, 73 | addsbdaylem 28058 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑦 +s 𝑥𝑅)}) ⊆ (( bday ‘𝑦) +no ( bday
‘𝑥))) |
75 | 37 | sseli 3998 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥𝑅 ∈ ( R
‘𝑥) → 𝑥𝑅 ∈
No ) |
76 | 75 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝑅 ∈ ( R ‘𝑥)) → 𝑥𝑅 ∈ No ) |
77 | | simplr 768 |
. . . . . . . . . . . . . . 15
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝑅 ∈ ( R ‘𝑥)) → 𝑦 ∈ No
) |
78 | 76, 77 | addscomd 28009 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝑅 ∈ ( R ‘𝑥)) → (𝑥𝑅 +s 𝑦) = (𝑦 +s 𝑥𝑅)) |
79 | 78 | eqeq2d 2745 |
. . . . . . . . . . . . 13
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ 𝑥𝑅 ∈ ( R ‘𝑥)) → (𝑧 = (𝑥𝑅 +s 𝑦) ↔ 𝑧 = (𝑦 +s 𝑥𝑅))) |
80 | 79 | rexbidva 3179 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → (∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦) ↔ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑦 +s 𝑥𝑅))) |
81 | 80 | abbidv 2805 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} = {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑦 +s 𝑥𝑅)}) |
82 | 81 | imaeq2d 6088 |
. . . . . . . . . 10
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → ( bday
“ {𝑧 ∣
∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) = (
bday “ {𝑧
∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑦 +s 𝑥𝑅)})) |
83 | 82 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) = (
bday “ {𝑧
∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑦 +s 𝑥𝑅)})) |
84 | 74, 83, 66 | 3sstr4d 4050 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) |
85 | | ssun2 4196 |
. . . . . . . . 9
⊢ ( R
‘𝑦) ⊆ (( L
‘𝑦) ∪ ( R
‘𝑦)) |
86 | 68, 69, 85 | addsbdaylem 28058 |
. . . . . . . 8
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) |
87 | 84, 86 | unssd 4209 |
. . . . . . 7
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → (( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) |
88 | 72, 87 | unssd 4209 |
. . . . . 6
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ((( bday “ {𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)})) ∪ (( bday “ {𝑧 ∣ ∃𝑥𝑅 ∈ ( R ‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)}) ∪ ( bday “ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) |
89 | 32, 88 | eqsstrid 4051 |
. . . . 5
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday “ (({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) ∪ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) |
90 | | naddcl 8729 |
. . . . . . 7
⊢ ((( bday ‘𝑥) ∈ On ∧ (
bday ‘𝑦)
∈ On) → (( bday ‘𝑥) +no (
bday ‘𝑦))
∈ On) |
91 | 63, 43, 90 | mp2an 691 |
. . . . . 6
⊢ (( bday ‘𝑥) +no ( bday
‘𝑦)) ∈
On |
92 | | scutbdaybnd 27869 |
. . . . . 6
⊢ ((({𝑧 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) <<s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) ∧ (( bday ‘𝑥) +no ( bday
‘𝑦)) ∈ On
∧ ( bday “ (({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) ∪ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) →
( bday ‘(({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) |s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) |
93 | 91, 92 | mp3an2 1449 |
. . . . 5
⊢ ((({𝑧 ∣ ∃𝑥𝐿 ∈ ( L
‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) <<s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) ∧ ( bday “ (({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) ∪ ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) →
( bday ‘(({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) |s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) |
94 | 27, 89, 93 | syl2an2r 684 |
. . . 4
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday ‘(({𝑧 ∣ ∃𝑥𝐿 ∈ ( L ‘𝑥)𝑧 = (𝑥𝐿 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( L ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}) |s ({𝑧 ∣ ∃𝑥𝑅 ∈ ( R
‘𝑥)𝑧 = (𝑥𝑅 +s 𝑦)} ∪ {𝑧 ∣ ∃𝑦𝐿 ∈ ( R ‘𝑦)𝑧 = (𝑥 +s 𝑦𝐿)}))) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦))) |
95 | 24, 94 | eqsstrd 4041 |
. . 3
⊢ (((𝑥 ∈
No ∧ 𝑦 ∈
No ) ∧ (∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂)))) → ( bday ‘(𝑥 +s 𝑦)) ⊆ (( bday
‘𝑥) +no ( bday ‘𝑦))) |
96 | 95 | ex 412 |
. 2
⊢ ((𝑥 ∈
No ∧ 𝑦 ∈
No ) → ((∀𝑥𝑂 ∈ (( L ‘𝑥) ∪ ( R ‘𝑥))∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥𝑂 +s 𝑦𝑂)) ⊆
(( bday ‘𝑥𝑂) +no ( bday ‘𝑦𝑂)) ∧ ∀𝑥𝑂 ∈ (( L
‘𝑥) ∪ ( R
‘𝑥))( bday ‘(𝑥𝑂 +s 𝑦)) ⊆ (( bday ‘𝑥𝑂) +no ( bday ‘𝑦)) ∧ ∀𝑦𝑂 ∈ (( L ‘𝑦) ∪ ( R ‘𝑦))( bday
‘(𝑥
+s 𝑦𝑂)) ⊆ (( bday ‘𝑥) +no ( bday
‘𝑦𝑂))) → ( bday ‘(𝑥 +s 𝑦)) ⊆ (( bday
‘𝑥) +no ( bday ‘𝑦)))) |
97 | 4, 9, 12, 16, 21, 96 | no2inds 27997 |
1
⊢ ((𝐴 ∈
No ∧ 𝐵 ∈
No ) → ( bday
‘(𝐴
+s 𝐵)) ⊆
(( bday ‘𝐴) +no ( bday
‘𝐵))) |