Step |
Hyp |
Ref |
Expression |
1 |
|
choccl |
⊢ ( 𝐵 ∈ Cℋ → ( ⊥ ‘ 𝐵 ) ∈ Cℋ ) |
2 |
|
chdmj1 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ ( ⊥ ‘ 𝐵 ) ∈ Cℋ ) → ( ⊥ ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) |
3 |
1 2
|
sylan2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) |
4 |
|
ococ |
⊢ ( 𝐵 ∈ Cℋ → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝐵 ) |
5 |
4
|
adantl |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝐵 ) |
6 |
5
|
ineq2d |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ⊥ ‘ 𝐴 ) ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) |
7 |
3 6
|
eqtrd |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ⊥ ‘ ( 𝐴 ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ 𝐵 ) ) |