Step |
Hyp |
Ref |
Expression |
1 |
|
ledi.1 |
⊢ 𝐴 ∈ Cℋ |
2 |
|
ledi.2 |
⊢ 𝐵 ∈ Cℋ |
3 |
|
ledi.3 |
⊢ 𝐶 ∈ Cℋ |
4 |
1 2
|
chub1i |
⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐵 ) |
5 |
1 3
|
chub1i |
⊢ 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐶 ) |
6 |
4 5
|
ssini |
⊢ 𝐴 ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) |
7 |
|
inss1 |
⊢ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐵 |
8 |
2 1
|
chub2i |
⊢ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐵 ) |
9 |
7 8
|
sstri |
⊢ ( 𝐵 ∩ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐵 ) |
10 |
|
inss2 |
⊢ ( 𝐵 ∩ 𝐶 ) ⊆ 𝐶 |
11 |
3 1
|
chub2i |
⊢ 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐶 ) |
12 |
10 11
|
sstri |
⊢ ( 𝐵 ∩ 𝐶 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) |
13 |
9 12
|
ssini |
⊢ ( 𝐵 ∩ 𝐶 ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) |
14 |
2 3
|
chincli |
⊢ ( 𝐵 ∩ 𝐶 ) ∈ Cℋ |
15 |
1 2
|
chjcli |
⊢ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ |
16 |
1 3
|
chjcli |
⊢ ( 𝐴 ∨ℋ 𝐶 ) ∈ Cℋ |
17 |
15 16
|
chincli |
⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ∈ Cℋ |
18 |
1 14 17
|
chlubi |
⊢ ( ( 𝐴 ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ∧ ( 𝐵 ∩ 𝐶 ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ) ↔ ( 𝐴 ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
19 |
18
|
bicomi |
⊢ ( ( 𝐴 ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ↔ ( 𝐴 ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ∧ ( 𝐵 ∩ 𝐶 ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) ) ) |
20 |
6 13 19
|
mpbir2an |
⊢ ( 𝐴 ∨ℋ ( 𝐵 ∩ 𝐶 ) ) ⊆ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( 𝐴 ∨ℋ 𝐶 ) ) |