Step |
Hyp |
Ref |
Expression |
1 |
|
ax-hilex |
⊢ ℋ ∈ V |
2 |
1
|
elpw2 |
⊢ ( 𝐴 ∈ 𝒫 ℋ ↔ 𝐴 ⊆ ℋ ) |
3 |
1
|
elpw2 |
⊢ ( 𝐵 ∈ 𝒫 ℋ ↔ 𝐵 ⊆ ℋ ) |
4 |
|
uniprg |
⊢ ( ( 𝐴 ∈ 𝒫 ℋ ∧ 𝐵 ∈ 𝒫 ℋ ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) ) |
5 |
2 3 4
|
syl2anbr |
⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ∪ { 𝐴 , 𝐵 } = ( 𝐴 ∪ 𝐵 ) ) |
6 |
5
|
fveq2d |
⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( ⊥ ‘ ∪ { 𝐴 , 𝐵 } ) = ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) |
7 |
6
|
fveq2d |
⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( ⊥ ‘ ( ⊥ ‘ ∪ { 𝐴 , 𝐵 } ) ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) |
8 |
|
prssi |
⊢ ( ( 𝐴 ∈ 𝒫 ℋ ∧ 𝐵 ∈ 𝒫 ℋ ) → { 𝐴 , 𝐵 } ⊆ 𝒫 ℋ ) |
9 |
2 3 8
|
syl2anbr |
⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → { 𝐴 , 𝐵 } ⊆ 𝒫 ℋ ) |
10 |
|
hsupval |
⊢ ( { 𝐴 , 𝐵 } ⊆ 𝒫 ℋ → ( ∨ℋ ‘ { 𝐴 , 𝐵 } ) = ( ⊥ ‘ ( ⊥ ‘ ∪ { 𝐴 , 𝐵 } ) ) ) |
11 |
9 10
|
syl |
⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( ∨ℋ ‘ { 𝐴 , 𝐵 } ) = ( ⊥ ‘ ( ⊥ ‘ ∪ { 𝐴 , 𝐵 } ) ) ) |
12 |
|
sshjval |
⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( ⊥ ‘ ( ⊥ ‘ ( 𝐴 ∪ 𝐵 ) ) ) ) |
13 |
7 11 12
|
3eqtr4rd |
⊢ ( ( 𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = ( ∨ℋ ‘ { 𝐴 , 𝐵 } ) ) |