Step |
Hyp |
Ref |
Expression |
1 |
|
ax-hilex |
|- ~H e. _V |
2 |
1
|
elpw2 |
|- ( A e. ~P ~H <-> A C_ ~H ) |
3 |
1
|
elpw2 |
|- ( B e. ~P ~H <-> B C_ ~H ) |
4 |
|
uniprg |
|- ( ( A e. ~P ~H /\ B e. ~P ~H ) -> U. { A , B } = ( A u. B ) ) |
5 |
2 3 4
|
syl2anbr |
|- ( ( A C_ ~H /\ B C_ ~H ) -> U. { A , B } = ( A u. B ) ) |
6 |
5
|
fveq2d |
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( _|_ ` U. { A , B } ) = ( _|_ ` ( A u. B ) ) ) |
7 |
6
|
fveq2d |
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( _|_ ` ( _|_ ` U. { A , B } ) ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) ) |
8 |
|
prssi |
|- ( ( A e. ~P ~H /\ B e. ~P ~H ) -> { A , B } C_ ~P ~H ) |
9 |
2 3 8
|
syl2anbr |
|- ( ( A C_ ~H /\ B C_ ~H ) -> { A , B } C_ ~P ~H ) |
10 |
|
hsupval |
|- ( { A , B } C_ ~P ~H -> ( \/H ` { A , B } ) = ( _|_ ` ( _|_ ` U. { A , B } ) ) ) |
11 |
9 10
|
syl |
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( \/H ` { A , B } ) = ( _|_ ` ( _|_ ` U. { A , B } ) ) ) |
12 |
|
sshjval |
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) = ( _|_ ` ( _|_ ` ( A u. B ) ) ) ) |
13 |
7 11 12
|
3eqtr4rd |
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A vH B ) = ( \/H ` { A , B } ) ) |