Step |
Hyp |
Ref |
Expression |
1 |
|
pjoml2.1 |
⊢ 𝐴 ∈ Cℋ |
2 |
|
pjoml2.2 |
⊢ 𝐵 ∈ Cℋ |
3 |
1 2
|
chincli |
⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ |
4 |
2
|
choccli |
⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ |
5 |
1 4
|
chincli |
⊢ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ |
6 |
3 5
|
chjcomi |
⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) |
7 |
2
|
pjococi |
⊢ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) = 𝐵 |
8 |
7
|
ineq2i |
⊢ ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) = ( 𝐴 ∩ 𝐵 ) |
9 |
8
|
oveq2i |
⊢ ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) = ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ 𝐵 ) ) |
10 |
6 9
|
eqtr4i |
⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) = ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) |
11 |
10
|
eqeq2i |
⊢ ( 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ↔ 𝐴 = ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) ) |
12 |
1 2
|
cmbri |
⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ) ) |
13 |
1 4
|
cmbri |
⊢ ( 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 ) ↔ 𝐴 = ( ( 𝐴 ∩ ( ⊥ ‘ 𝐵 ) ) ∨ℋ ( 𝐴 ∩ ( ⊥ ‘ ( ⊥ ‘ 𝐵 ) ) ) ) ) |
14 |
11 12 13
|
3bitr4i |
⊢ ( 𝐴 𝐶ℋ 𝐵 ↔ 𝐴 𝐶ℋ ( ⊥ ‘ 𝐵 ) ) |