Step |
Hyp |
Ref |
Expression |
1 |
|
shlesb1.1 |
|- A e. SH |
2 |
|
shlesb1.2 |
|- B e. SH |
3 |
|
ssun1 |
|- A C_ ( A u. B ) |
4 |
|
ssintub |
|- ( A u. B ) C_ |^| { x e. SH | ( A u. B ) C_ x } |
5 |
3 4
|
sstri |
|- A C_ |^| { x e. SH | ( A u. B ) C_ x } |
6 |
|
ssun2 |
|- B C_ ( A u. B ) |
7 |
6 4
|
sstri |
|- B C_ |^| { x e. SH | ( A u. B ) C_ x } |
8 |
5 7
|
pm3.2i |
|- ( A C_ |^| { x e. SH | ( A u. B ) C_ x } /\ B C_ |^| { x e. SH | ( A u. B ) C_ x } ) |
9 |
|
ssrab2 |
|- { x e. SH | ( A u. B ) C_ x } C_ SH |
10 |
1 2
|
shscli |
|- ( A +H B ) e. SH |
11 |
1 2
|
shunssi |
|- ( A u. B ) C_ ( A +H B ) |
12 |
|
sseq2 |
|- ( x = ( A +H B ) -> ( ( A u. B ) C_ x <-> ( A u. B ) C_ ( A +H B ) ) ) |
13 |
12
|
rspcev |
|- ( ( ( A +H B ) e. SH /\ ( A u. B ) C_ ( A +H B ) ) -> E. x e. SH ( A u. B ) C_ x ) |
14 |
10 11 13
|
mp2an |
|- E. x e. SH ( A u. B ) C_ x |
15 |
|
rabn0 |
|- ( { x e. SH | ( A u. B ) C_ x } =/= (/) <-> E. x e. SH ( A u. B ) C_ x ) |
16 |
14 15
|
mpbir |
|- { x e. SH | ( A u. B ) C_ x } =/= (/) |
17 |
|
shintcl |
|- ( ( { x e. SH | ( A u. B ) C_ x } C_ SH /\ { x e. SH | ( A u. B ) C_ x } =/= (/) ) -> |^| { x e. SH | ( A u. B ) C_ x } e. SH ) |
18 |
9 16 17
|
mp2an |
|- |^| { x e. SH | ( A u. B ) C_ x } e. SH |
19 |
1 2 18
|
shslubi |
|- ( ( A C_ |^| { x e. SH | ( A u. B ) C_ x } /\ B C_ |^| { x e. SH | ( A u. B ) C_ x } ) <-> ( A +H B ) C_ |^| { x e. SH | ( A u. B ) C_ x } ) |
20 |
8 19
|
mpbi |
|- ( A +H B ) C_ |^| { x e. SH | ( A u. B ) C_ x } |
21 |
12
|
elrab |
|- ( ( A +H B ) e. { x e. SH | ( A u. B ) C_ x } <-> ( ( A +H B ) e. SH /\ ( A u. B ) C_ ( A +H B ) ) ) |
22 |
10 11 21
|
mpbir2an |
|- ( A +H B ) e. { x e. SH | ( A u. B ) C_ x } |
23 |
|
intss1 |
|- ( ( A +H B ) e. { x e. SH | ( A u. B ) C_ x } -> |^| { x e. SH | ( A u. B ) C_ x } C_ ( A +H B ) ) |
24 |
22 23
|
ax-mp |
|- |^| { x e. SH | ( A u. B ) C_ x } C_ ( A +H B ) |
25 |
20 24
|
eqssi |
|- ( A +H B ) = |^| { x e. SH | ( A u. B ) C_ x } |