Step |
Hyp |
Ref |
Expression |
1 |
|
shlesb1.1 |
⊢ 𝐴 ∈ Sℋ |
2 |
|
shlesb1.2 |
⊢ 𝐵 ∈ Sℋ |
3 |
|
ssun1 |
⊢ 𝐴 ⊆ ( 𝐴 ∪ 𝐵 ) |
4 |
|
ssintub |
⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } |
5 |
3 4
|
sstri |
⊢ 𝐴 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } |
6 |
|
ssun2 |
⊢ 𝐵 ⊆ ( 𝐴 ∪ 𝐵 ) |
7 |
6 4
|
sstri |
⊢ 𝐵 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } |
8 |
5 7
|
pm3.2i |
⊢ ( 𝐴 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∧ 𝐵 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ) |
9 |
|
ssrab2 |
⊢ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ Sℋ |
10 |
1 2
|
shscli |
⊢ ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ |
11 |
1 2
|
shunssi |
⊢ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) |
12 |
|
sseq2 |
⊢ ( 𝑥 = ( 𝐴 +ℋ 𝐵 ) → ( ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 ↔ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) ) |
13 |
12
|
rspcev |
⊢ ( ( ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) → ∃ 𝑥 ∈ Sℋ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 ) |
14 |
10 11 13
|
mp2an |
⊢ ∃ 𝑥 ∈ Sℋ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 |
15 |
|
rabn0 |
⊢ ( { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ≠ ∅ ↔ ∃ 𝑥 ∈ Sℋ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 ) |
16 |
14 15
|
mpbir |
⊢ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ≠ ∅ |
17 |
|
shintcl |
⊢ ( ( { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ Sℋ ∧ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ≠ ∅ ) → ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∈ Sℋ ) |
18 |
9 16 17
|
mp2an |
⊢ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∈ Sℋ |
19 |
1 2 18
|
shslubi |
⊢ ( ( 𝐴 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ∧ 𝐵 ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ) ↔ ( 𝐴 +ℋ 𝐵 ) ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ) |
20 |
8 19
|
mpbi |
⊢ ( 𝐴 +ℋ 𝐵 ) ⊆ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } |
21 |
12
|
elrab |
⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ↔ ( ( 𝐴 +ℋ 𝐵 ) ∈ Sℋ ∧ ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐴 +ℋ 𝐵 ) ) ) |
22 |
10 11 21
|
mpbir2an |
⊢ ( 𝐴 +ℋ 𝐵 ) ∈ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } |
23 |
|
intss1 |
⊢ ( ( 𝐴 +ℋ 𝐵 ) ∈ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } → ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ ( 𝐴 +ℋ 𝐵 ) ) |
24 |
22 23
|
ax-mp |
⊢ ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } ⊆ ( 𝐴 +ℋ 𝐵 ) |
25 |
20 24
|
eqssi |
⊢ ( 𝐴 +ℋ 𝐵 ) = ∩ { 𝑥 ∈ Sℋ ∣ ( 𝐴 ∪ 𝐵 ) ⊆ 𝑥 } |