Step |
Hyp |
Ref |
Expression |
1 |
|
shincl.1 |
⊢ 𝐴 ∈ Sℋ |
2 |
|
shincl.2 |
⊢ 𝐵 ∈ Sℋ |
3 |
1 2
|
shseli |
⊢ ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) ↔ ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) ) |
4 |
|
ssun1 |
⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) |
5 |
1 2
|
shunssji |
⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) |
6 |
4 5
|
sstri |
⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) |
7 |
6
|
sseli |
⊢ ( 𝑦 ∈ 𝐴 → 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) ) |
8 |
|
ssun2 |
⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) |
9 |
8 5
|
sstri |
⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) |
10 |
9
|
sseli |
⊢ ( 𝑧 ∈ 𝐵 → 𝑧 ∈ ( 𝐴 ∨ℋ 𝐵 ) ) |
11 |
|
shjcl |
⊢ ( ( 𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) |
12 |
1 2 11
|
mp2an |
⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ |
13 |
12
|
chshii |
⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Sℋ |
14 |
|
shaddcl |
⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∈ Sℋ ∧ 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑦 +ℎ 𝑧 ) ∈ ( 𝐴 ∨ℋ 𝐵 ) ) |
15 |
13 14
|
mp3an1 |
⊢ ( ( 𝑦 ∈ ( 𝐴 ∨ℋ 𝐵 ) ∧ 𝑧 ∈ ( 𝐴 ∨ℋ 𝐵 ) ) → ( 𝑦 +ℎ 𝑧 ) ∈ ( 𝐴 ∨ℋ 𝐵 ) ) |
16 |
7 10 15
|
syl2an |
⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑦 +ℎ 𝑧 ) ∈ ( 𝐴 ∨ℋ 𝐵 ) ) |
17 |
|
eleq1a |
⊢ ( ( 𝑦 +ℎ 𝑧 ) ∈ ( 𝐴 ∨ℋ 𝐵 ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
18 |
16 17
|
syl |
⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐵 ) → ( 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
19 |
18
|
rexlimivv |
⊢ ( ∃ 𝑦 ∈ 𝐴 ∃ 𝑧 ∈ 𝐵 𝑥 = ( 𝑦 +ℎ 𝑧 ) → 𝑥 ∈ ( 𝐴 ∨ℋ 𝐵 ) ) |
20 |
3 19
|
sylbi |
⊢ ( 𝑥 ∈ ( 𝐴 +ℋ 𝐵 ) → 𝑥 ∈ ( 𝐴 ∨ℋ 𝐵 ) ) |
21 |
20
|
ssriv |
⊢ ( 𝐴 +ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) |