Step |
Hyp |
Ref |
Expression |
1 |
|
chpssat.1 |
⊢ 𝐴 ∈ Cℋ |
2 |
|
chpssat.2 |
⊢ 𝐵 ∈ Cℋ |
3 |
1 2
|
chpssati |
⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) ) |
4 |
|
ancom |
⊢ ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) ↔ ( ¬ 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ) |
5 |
|
pssss |
⊢ ( 𝐴 ⊊ 𝐵 → 𝐴 ⊆ 𝐵 ) |
6 |
|
atelch |
⊢ ( 𝑥 ∈ HAtoms → 𝑥 ∈ Cℋ ) |
7 |
|
chnle |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ) → ( ¬ 𝑥 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ) ) |
8 |
1 7
|
mpan |
⊢ ( 𝑥 ∈ Cℋ → ( ¬ 𝑥 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ) ) |
9 |
8
|
adantl |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Cℋ ) → ( ¬ 𝑥 ⊆ 𝐴 ↔ 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ) ) |
10 |
|
ibar |
⊢ ( 𝐴 ⊆ 𝐵 → ( 𝑥 ⊆ 𝐵 ↔ ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ) ) |
11 |
|
chlub |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) |
12 |
1 2 11
|
mp3an13 |
⊢ ( 𝑥 ∈ Cℋ → ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) |
13 |
10 12
|
sylan9bb |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Cℋ ) → ( 𝑥 ⊆ 𝐵 ↔ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) |
14 |
9 13
|
anbi12d |
⊢ ( ( 𝐴 ⊆ 𝐵 ∧ 𝑥 ∈ Cℋ ) → ( ( ¬ 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) ) |
15 |
5 6 14
|
syl2an |
⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ HAtoms ) → ( ( ¬ 𝑥 ⊆ 𝐴 ∧ 𝑥 ⊆ 𝐵 ) ↔ ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) ) |
16 |
4 15
|
syl5bb |
⊢ ( ( 𝐴 ⊊ 𝐵 ∧ 𝑥 ∈ HAtoms ) → ( ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) ↔ ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) ) |
17 |
16
|
rexbidva |
⊢ ( 𝐴 ⊊ 𝐵 → ( ∃ 𝑥 ∈ HAtoms ( 𝑥 ⊆ 𝐵 ∧ ¬ 𝑥 ⊆ 𝐴 ) ↔ ∃ 𝑥 ∈ HAtoms ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) ) |
18 |
3 17
|
mpbid |
⊢ ( 𝐴 ⊊ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ∧ ( 𝐴 ∨ℋ 𝑥 ) ⊆ 𝐵 ) ) |