Step |
Hyp |
Ref |
Expression |
1 |
|
chpssat.1 |
⊢ 𝐴 ∈ Cℋ |
2 |
|
chpssat.2 |
⊢ 𝐵 ∈ Cℋ |
3 |
|
cvpss |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ( 𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵 ) ) |
4 |
1 2 3
|
mp2an |
⊢ ( 𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵 ) |
5 |
1 2
|
cvati |
⊢ ( 𝐴 ⋖ℋ 𝐵 → ∃ 𝑥 ∈ HAtoms ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) |
6 |
4 5
|
jca |
⊢ ( 𝐴 ⋖ℋ 𝐵 → ( 𝐴 ⊊ 𝐵 ∧ ∃ 𝑥 ∈ HAtoms ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) ) |
7 |
|
chcv2 |
⊢ ( ( 𝐴 ∈ Cℋ ∧ 𝑥 ∈ HAtoms ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ) ) |
8 |
1 7
|
mpan |
⊢ ( 𝑥 ∈ HAtoms → ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ) ) |
9 |
8
|
adantr |
⊢ ( ( 𝑥 ∈ HAtoms ∧ ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ↔ 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ) ) |
10 |
|
psseq2 |
⊢ ( ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 → ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ↔ 𝐴 ⊊ 𝐵 ) ) |
11 |
10
|
adantl |
⊢ ( ( 𝑥 ∈ HAtoms ∧ ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) → ( 𝐴 ⊊ ( 𝐴 ∨ℋ 𝑥 ) ↔ 𝐴 ⊊ 𝐵 ) ) |
12 |
|
breq2 |
⊢ ( ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ↔ 𝐴 ⋖ℋ 𝐵 ) ) |
13 |
12
|
adantl |
⊢ ( ( 𝑥 ∈ HAtoms ∧ ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) → ( 𝐴 ⋖ℋ ( 𝐴 ∨ℋ 𝑥 ) ↔ 𝐴 ⋖ℋ 𝐵 ) ) |
14 |
9 11 13
|
3bitr3d |
⊢ ( ( 𝑥 ∈ HAtoms ∧ ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) → ( 𝐴 ⊊ 𝐵 ↔ 𝐴 ⋖ℋ 𝐵 ) ) |
15 |
14
|
biimpd |
⊢ ( ( 𝑥 ∈ HAtoms ∧ ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) → ( 𝐴 ⊊ 𝐵 → 𝐴 ⋖ℋ 𝐵 ) ) |
16 |
15
|
ex |
⊢ ( 𝑥 ∈ HAtoms → ( ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 → ( 𝐴 ⊊ 𝐵 → 𝐴 ⋖ℋ 𝐵 ) ) ) |
17 |
16
|
com3r |
⊢ ( 𝐴 ⊊ 𝐵 → ( 𝑥 ∈ HAtoms → ( ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 → 𝐴 ⋖ℋ 𝐵 ) ) ) |
18 |
17
|
rexlimdv |
⊢ ( 𝐴 ⊊ 𝐵 → ( ∃ 𝑥 ∈ HAtoms ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 → 𝐴 ⋖ℋ 𝐵 ) ) |
19 |
18
|
imp |
⊢ ( ( 𝐴 ⊊ 𝐵 ∧ ∃ 𝑥 ∈ HAtoms ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) → 𝐴 ⋖ℋ 𝐵 ) |
20 |
6 19
|
impbii |
⊢ ( 𝐴 ⋖ℋ 𝐵 ↔ ( 𝐴 ⊊ 𝐵 ∧ ∃ 𝑥 ∈ HAtoms ( 𝐴 ∨ℋ 𝑥 ) = 𝐵 ) ) |