Step |
Hyp |
Ref |
Expression |
1 |
|
atelch |
⊢ ( 𝐶 ∈ HAtoms → 𝐶 ∈ Cℋ ) |
2 |
|
chub2 |
⊢ ( ( 𝐶 ∈ Cℋ ∧ 𝐴 ∈ Cℋ ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) |
3 |
2
|
ancoms |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) |
4 |
1 3
|
sylan2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ HAtoms ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) |
5 |
4
|
3adant2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) |
6 |
5
|
adantr |
⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) |
7 |
|
cvp |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
8 |
|
atelch |
⊢ ( 𝐵 ∈ HAtoms → 𝐵 ∈ Cℋ ) |
9 |
|
chjcl |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) |
10 |
8 9
|
sylan2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) |
11 |
|
cvpss |
⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
12 |
10 11
|
syldan |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) → 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
13 |
7 12
|
sylbid |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
14 |
13
|
3adant3 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐴 ∩ 𝐵 ) = 0ℋ → 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
15 |
14
|
adantld |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
16 |
|
id |
⊢ ( 𝐴 ∈ Cℋ → 𝐴 ∈ Cℋ ) |
17 |
|
chub1 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) |
18 |
17
|
3adant2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) |
19 |
18
|
a1d |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) → 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
20 |
19
|
ancrd |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) → ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) ) |
21 |
|
chjcl |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐶 ) ∈ Cℋ ) |
22 |
21
|
3adant2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐶 ) ∈ Cℋ ) |
23 |
|
chlub |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐶 ) ∈ Cℋ ) → ( ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ↔ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
24 |
22 23
|
syld3an3 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( ( 𝐴 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ↔ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
25 |
20 24
|
sylibd |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) → ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
26 |
16 8 1 25
|
syl3an |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) → ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
27 |
26
|
adantrd |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
28 |
15 27
|
jcad |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) ) |
29 |
28
|
imp |
⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
30 |
|
simp1 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → 𝐴 ∈ Cℋ ) |
31 |
9
|
3adant3 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) |
32 |
30 22 31
|
3jca |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐶 ) ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) ) |
33 |
16 8 1 32
|
syl3an |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐶 ) ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) ) |
34 |
14 26
|
anim12d |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( ( 𝐴 ∩ 𝐵 ) = 0ℋ ∧ 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) ) |
35 |
34
|
ancomsd |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) ) ) |
36 |
|
psssstr |
⊢ ( ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐶 ) ) |
37 |
35 36
|
syl6 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
38 |
|
chcv2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐶 ) ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
39 |
38
|
3adant2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐶 ) ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
40 |
37 39
|
sylibd |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐶 ) ) ) |
41 |
|
cvnbtwn2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐶 ) ∈ Cℋ ∧ ( 𝐴 ∨ℋ 𝐵 ) ∈ Cℋ ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐶 ) → ( ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( 𝐴 ∨ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐶 ) ) ) ) |
42 |
33 40 41
|
sylsyld |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → ( ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( 𝐴 ∨ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐶 ) ) ) ) |
43 |
42
|
imp |
⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝐵 ) ∧ ( 𝐴 ∨ℋ 𝐵 ) ⊆ ( 𝐴 ∨ℋ 𝐶 ) ) → ( 𝐴 ∨ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐶 ) ) ) |
44 |
29 43
|
mpd |
⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → ( 𝐴 ∨ℋ 𝐵 ) = ( 𝐴 ∨ℋ 𝐶 ) ) |
45 |
6 44
|
sseqtrrd |
⊢ ( ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) ∧ ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) |
46 |
45
|
ex |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ HAtoms ∧ 𝐶 ∈ HAtoms ) → ( ( 𝐵 ⊆ ( 𝐴 ∨ℋ 𝐶 ) ∧ ( 𝐴 ∩ 𝐵 ) = 0ℋ ) → 𝐶 ⊆ ( 𝐴 ∨ℋ 𝐵 ) ) ) |