Step |
Hyp |
Ref |
Expression |
1 |
|
pjoml2.1 |
⊢ 𝐴 ∈ Cℋ |
2 |
|
pjoml2.2 |
⊢ 𝐵 ∈ Cℋ |
3 |
|
inss1 |
⊢ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ 𝐵 |
4 |
1
|
choccli |
⊢ ( ⊥ ‘ 𝐴 ) ∈ Cℋ |
5 |
2
|
choccli |
⊢ ( ⊥ ‘ 𝐵 ) ∈ Cℋ |
6 |
4 5
|
chjcli |
⊢ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∈ Cℋ |
7 |
2 6
|
chincli |
⊢ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ∈ Cℋ |
8 |
7 2 1
|
chlej2i |
⊢ ( ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ⊆ 𝐵 → ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) |
9 |
3 8
|
ax-mp |
⊢ ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) |
10 |
1 7
|
chub1i |
⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) |
11 |
1 2
|
chdmm1i |
⊢ ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) = ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) |
12 |
11
|
ineq1i |
⊢ ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐵 ) = ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ 𝐵 ) |
13 |
|
incom |
⊢ ( ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ∩ 𝐵 ) = ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) |
14 |
12 13
|
eqtri |
⊢ ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐵 ) = ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) |
15 |
14
|
oveq2i |
⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐵 ) ) = ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) |
16 |
|
inss2 |
⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 |
17 |
1 2
|
chincli |
⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ |
18 |
17 2
|
pjoml2i |
⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐵 ) ) = 𝐵 ) |
19 |
16 18
|
ax-mp |
⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( ( ⊥ ‘ ( 𝐴 ∩ 𝐵 ) ) ∩ 𝐵 ) ) = 𝐵 |
20 |
15 19
|
eqtr3i |
⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) = 𝐵 |
21 |
|
inss1 |
⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 |
22 |
17 1 7
|
chlej1i |
⊢ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐴 → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) ) |
23 |
21 22
|
ax-mp |
⊢ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) |
24 |
20 23
|
eqsstrri |
⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) |
25 |
1 7
|
chjcli |
⊢ ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) ∈ Cℋ |
26 |
1 2 25
|
chlubii |
⊢ ( ( 𝐴 ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) ) → ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) ) |
27 |
10 24 26
|
mp2an |
⊢ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) |
28 |
9 27
|
eqssi |
⊢ ( 𝐴 ∨ℋ ( 𝐵 ∩ ( ( ⊥ ‘ 𝐴 ) ∨ℋ ( ⊥ ‘ 𝐵 ) ) ) ) = ( 𝐴 ∨ℋ 𝐵 ) |