Step |
Hyp |
Ref |
Expression |
1 |
|
chpssat.1 |
⊢ 𝐴 ∈ Cℋ |
2 |
|
chpssat.2 |
⊢ 𝐵 ∈ Cℋ |
3 |
1 2
|
chincli |
⊢ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ |
4 |
|
cvpss |
⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) ) |
5 |
3 2 4
|
mp2an |
⊢ ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 ) |
6 |
3 2
|
chpssati |
⊢ ( ( 𝐴 ∩ 𝐵 ) ⊊ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ) |
7 |
5 6
|
syl |
⊢ ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ) |
8 |
|
ssin |
⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) |
9 |
|
ancom |
⊢ ( ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ) ) |
10 |
8 9
|
bitr3i |
⊢ ( 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐴 ) ) |
11 |
10
|
baibr |
⊢ ( 𝑥 ⊆ 𝐵 → ( 𝑥 ⊆ 𝐴 ↔ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ) |
12 |
11
|
notbid |
⊢ ( 𝑥 ⊆ 𝐵 → ( ¬ 𝑥 ⊆ 𝐴 ↔ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ) |
13 |
12
|
biimpar |
⊢ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) → ¬ 𝑥 ⊆ 𝐴 ) |
14 |
|
chcv1 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ HAtoms ) → ( ¬ 𝑥 ⊆ 𝐴 ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ) ) |
15 |
1 14
|
mpan |
⊢ ( 𝑥 ∈ HAtoms → ( ¬ 𝑥 ⊆ 𝐴 ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ) ) |
16 |
15
|
biimpa |
⊢ ( ( 𝑥 ∈ HAtoms ∧ ¬ 𝑥 ⊆ 𝐴 ) → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ) |
17 |
13 16
|
sylan2 |
⊢ ( ( 𝑥 ∈ HAtoms ∧ ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ) → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ) |
18 |
17
|
adantrr |
⊢ ( ( 𝑥 ∈ HAtoms ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ) |
19 |
|
atelch |
⊢ ( 𝑥 ∈ HAtoms → 𝑥 ∈ Cℋ ) |
20 |
|
chjass |
⊢ ( ( 𝐴 ∈ Cℋ ∧ ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) ) |
21 |
1 3 20
|
mp3an12 |
⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) ) |
22 |
1 2
|
chabs1i |
⊢ ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) = 𝐴 |
23 |
22
|
oveq1i |
⊢ ( ( 𝐴 ∨ℋ ( 𝐴 ∩ 𝐵 ) ) ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ 𝑥 ) |
24 |
21 23
|
eqtr3di |
⊢ ( 𝑥 ∈ Cℋ → ( 𝐴 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) = ( 𝐴 ∨ℋ 𝑥 ) ) |
25 |
24
|
adantr |
⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → ( 𝐴 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) = ( 𝐴 ∨ℋ 𝑥 ) ) |
26 |
|
ancom |
⊢ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ 𝑥 ⊆ 𝐵 ) ) |
27 |
|
chnle |
⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) ) |
28 |
3 27
|
mpan |
⊢ ( 𝑥 ∈ Cℋ → ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ↔ ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) ) |
29 |
|
inss2 |
⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 |
30 |
29
|
biantrur |
⊢ ( 𝑥 ⊆ 𝐵 ↔ ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ) |
31 |
|
chlub |
⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) |
32 |
3 2 31
|
mp3an13 |
⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) |
33 |
30 32
|
syl5bb |
⊢ ( 𝑥 ∈ Cℋ → ( 𝑥 ⊆ 𝐵 ↔ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) |
34 |
28 33
|
anbi12d |
⊢ ( 𝑥 ∈ Cℋ → ( ( ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ∧ 𝑥 ⊆ 𝐵 ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) ) |
35 |
26 34
|
syl5bb |
⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ↔ ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) ) |
36 |
|
chjcl |
⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∈ Cℋ ) |
37 |
3 36
|
mpan |
⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∈ Cℋ ) |
38 |
|
cvnbtwn2 |
⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∈ Cℋ ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 ) ) ) |
39 |
3 2 38
|
mp3an12 |
⊢ ( ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∈ Cℋ → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 ) ) ) |
40 |
37 39
|
syl |
⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 ) ) ) |
41 |
40
|
com23 |
⊢ ( 𝑥 ∈ Cℋ → ( ( ( 𝐴 ∩ 𝐵 ) ⊊ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ∧ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ⊆ 𝐵 ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 ) ) ) |
42 |
35 41
|
sylbid |
⊢ ( 𝑥 ∈ Cℋ → ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 ) ) ) |
43 |
42
|
imp32 |
⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) = 𝐵 ) |
44 |
43
|
oveq2d |
⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → ( 𝐴 ∨ℋ ( ( 𝐴 ∩ 𝐵 ) ∨ℋ 𝑥 ) ) = ( 𝐴 ∨ℋ 𝐵 ) ) |
45 |
25 44
|
eqtr3d |
⊢ ( ( 𝑥 ∈ Cℋ ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → ( 𝐴 ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ 𝐵 ) ) |
46 |
19 45
|
sylan |
⊢ ( ( 𝑥 ∈ HAtoms ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → ( 𝐴 ∨ℋ 𝑥 ) = ( 𝐴 ∨ℋ 𝐵 ) ) |
47 |
18 46
|
breqtrd |
⊢ ( ( 𝑥 ∈ HAtoms ∧ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) ∧ ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 ) ) → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) |
48 |
47
|
exp32 |
⊢ ( 𝑥 ∈ HAtoms → ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) ) |
49 |
48
|
rexlimiv |
⊢ ( ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ ( 𝐴 ∩ 𝐵 ) ) → ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) ) |
50 |
7 49
|
mpcom |
⊢ ( ( 𝐴 ∩ 𝐵 ) ⋖ℋ 𝐵 → 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝐵 ) ) |