Step |
Hyp |
Ref |
Expression |
1 |
|
atoml.1 |
⊢ 𝐴 ∈ Cℋ |
2 |
|
atelch |
⊢ ( 𝐵 ∈ HAtoms → 𝐵 ∈ Cℋ ) |
3 |
|
pjoml5 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 𝐵 ) ) |
4 |
1 2 3
|
sylancr |
⊢ ( 𝐵 ∈ HAtoms → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 𝐵 ) ) |
5 |
|
incom |
⊢ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) |
6 |
5
|
eqeq1i |
⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ↔ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 0ℋ ) |
7 |
6
|
biimpi |
⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) = 0ℋ ) |
8 |
7
|
oveq2d |
⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = ( 𝐴 ∨ℋ 0ℋ ) ) |
9 |
1
|
chj0i |
⊢ ( 𝐴 ∨ℋ 0ℋ ) = 𝐴 |
10 |
8 9
|
eqtrdi |
⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → ( 𝐴 ∨ℋ ( ( ⊥ ‘ 𝐴 ) ∩ ( 𝐴 ∨ℋ 𝐵 ) ) ) = 𝐴 ) |
11 |
4 10
|
sylan9req |
⊢ ( ( 𝐵 ∈ HAtoms ∧ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) = 𝐴 ) |
12 |
11
|
ex |
⊢ ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → ( 𝐴 ∨ℋ 𝐵 ) = 𝐴 ) ) |
13 |
|
chlejb2 |
⊢ ( ( 𝐵 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∨ℋ 𝐵 ) = 𝐴 ) ) |
14 |
2 1 13
|
sylancl |
⊢ ( 𝐵 ∈ HAtoms → ( 𝐵 ⊆ 𝐴 ↔ ( 𝐴 ∨ℋ 𝐵 ) = 𝐴 ) ) |
15 |
12 14
|
sylibrd |
⊢ ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → 𝐵 ⊆ 𝐴 ) ) |
16 |
15
|
con3d |
⊢ ( 𝐵 ∈ HAtoms → ( ¬ 𝐵 ⊆ 𝐴 → ¬ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ) ) |
17 |
1
|
atomli |
⊢ ( 𝐵 ∈ HAtoms → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0ℋ } ) ) |
18 |
|
elun |
⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0ℋ } ) ↔ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0ℋ } ) ) |
19 |
|
h0elch |
⊢ 0ℋ ∈ Cℋ |
20 |
19
|
elexi |
⊢ 0ℋ ∈ V |
21 |
20
|
elsn2 |
⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0ℋ } ↔ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ) |
22 |
21
|
orbi2i |
⊢ ( ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ { 0ℋ } ) ↔ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ) ) |
23 |
|
orcom |
⊢ ( ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ) ↔ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) ) |
24 |
18 22 23
|
3bitri |
⊢ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ ( HAtoms ∪ { 0ℋ } ) ↔ ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) ) |
25 |
17 24
|
sylib |
⊢ ( 𝐵 ∈ HAtoms → ( ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ ∨ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) ) |
26 |
25
|
ord |
⊢ ( 𝐵 ∈ HAtoms → ( ¬ ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) = 0ℋ → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) ) |
27 |
16 26
|
syld |
⊢ ( 𝐵 ∈ HAtoms → ( ¬ 𝐵 ⊆ 𝐴 → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) ) |
28 |
27
|
imp |
⊢ ( ( 𝐵 ∈ HAtoms ∧ ¬ 𝐵 ⊆ 𝐴 ) → ( ( 𝐴 ∨ℋ 𝐵 ) ∩ ( ⊥ ‘ 𝐴 ) ) ∈ HAtoms ) |