# Metamath Proof Explorer

## Theorem mdsymlem3

Description: Lemma for mdsymi . (Contributed by NM, 2-Jul-2004) (New usage is discouraged.)

Ref Expression
Hypotheses mdsymlem1.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
mdsymlem1.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
mdsymlem1.3 ${⊢}{C}={A}{\vee }_{ℋ}{p}$
Assertion mdsymlem3 ${⊢}\left(\left(\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\wedge {p}\subseteq {A}{\vee }_{ℋ}{B}\right)\wedge {A}\ne {0}_{ℋ}\right)\to \exists {r}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({p}\subseteq {q}{\vee }_{ℋ}{r}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {B}\right)\right)$

### Proof

Step Hyp Ref Expression
1 mdsymlem1.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 mdsymlem1.2 ${⊢}{B}\in {\mathbf{C}}_{ℋ}$
3 mdsymlem1.3 ${⊢}{C}={A}{\vee }_{ℋ}{p}$
4 ssin ${⊢}\left({r}\subseteq {B}\wedge {r}\subseteq {C}\right)↔{r}\subseteq {B}\cap {C}$
5 3 sseq2i ${⊢}{r}\subseteq {C}↔{r}\subseteq {A}{\vee }_{ℋ}{p}$
6 5 biimpi ${⊢}{r}\subseteq {C}\to {r}\subseteq {A}{\vee }_{ℋ}{p}$
7 6 adantl ${⊢}\left({r}\subseteq {B}\wedge {r}\subseteq {C}\right)\to {r}\subseteq {A}{\vee }_{ℋ}{p}$
8 4 7 sylbir ${⊢}{r}\subseteq {B}\cap {C}\to {r}\subseteq {A}{\vee }_{ℋ}{p}$
9 1 atcvat4i ${⊢}\left({r}\in \mathrm{HAtoms}\wedge {p}\in \mathrm{HAtoms}\right)\to \left(\left({A}\ne {0}_{ℋ}\wedge {r}\subseteq {A}{\vee }_{ℋ}{p}\right)\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)$
10 9 exp4b ${⊢}{r}\in \mathrm{HAtoms}\to \left({p}\in \mathrm{HAtoms}\to \left({A}\ne {0}_{ℋ}\to \left({r}\subseteq {A}{\vee }_{ℋ}{p}\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)\right)\right)$
11 10 com34 ${⊢}{r}\in \mathrm{HAtoms}\to \left({p}\in \mathrm{HAtoms}\to \left({r}\subseteq {A}{\vee }_{ℋ}{p}\to \left({A}\ne {0}_{ℋ}\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)\right)\right)$
12 11 com23 ${⊢}{r}\in \mathrm{HAtoms}\to \left({r}\subseteq {A}{\vee }_{ℋ}{p}\to \left({p}\in \mathrm{HAtoms}\to \left({A}\ne {0}_{ℋ}\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)\right)\right)$
13 12 imp4b ${⊢}\left({r}\in \mathrm{HAtoms}\wedge {r}\subseteq {A}{\vee }_{ℋ}{p}\right)\to \left(\left({p}\in \mathrm{HAtoms}\wedge {A}\ne {0}_{ℋ}\right)\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)$
14 8 13 sylan2 ${⊢}\left({r}\in \mathrm{HAtoms}\wedge {r}\subseteq {B}\cap {C}\right)\to \left(\left({p}\in \mathrm{HAtoms}\wedge {A}\ne {0}_{ℋ}\right)\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)$
15 14 adantrr ${⊢}\left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\to \left(\left({p}\in \mathrm{HAtoms}\wedge {A}\ne {0}_{ℋ}\right)\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)$
16 15 com12 ${⊢}\left({p}\in \mathrm{HAtoms}\wedge {A}\ne {0}_{ℋ}\right)\to \left(\left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)$
17 16 adantlr ${⊢}\left(\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\wedge {A}\ne {0}_{ℋ}\right)\to \left(\left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)$
18 17 adantlr ${⊢}\left(\left(\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\wedge {p}\subseteq {A}{\vee }_{ℋ}{B}\right)\wedge {A}\ne {0}_{ℋ}\right)\to \left(\left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)$
19 18 imp ${⊢}\left(\left(\left(\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\wedge {p}\subseteq {A}{\vee }_{ℋ}{B}\right)\wedge {A}\ne {0}_{ℋ}\right)\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)$
20 nssne2 ${⊢}\left({q}\subseteq {A}\wedge ¬{r}\subseteq {A}\right)\to {q}\ne {r}$
21 20 adantrl ${⊢}\left({q}\subseteq {A}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\to {q}\ne {r}$
22 atnemeq0 ${⊢}\left({q}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\to \left({q}\ne {r}↔{q}\cap {r}={0}_{ℋ}\right)$
23 22 ancoms ${⊢}\left({r}\in \mathrm{HAtoms}\wedge {q}\in \mathrm{HAtoms}\right)\to \left({q}\ne {r}↔{q}\cap {r}={0}_{ℋ}\right)$
24 21 23 syl5ib ${⊢}\left({r}\in \mathrm{HAtoms}\wedge {q}\in \mathrm{HAtoms}\right)\to \left(\left({q}\subseteq {A}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\to {q}\cap {r}={0}_{ℋ}\right)$
25 24 adantll ${⊢}\left(\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\wedge {q}\in \mathrm{HAtoms}\right)\to \left(\left({q}\subseteq {A}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\to {q}\cap {r}={0}_{ℋ}\right)$
26 25 adantr ${⊢}\left(\left(\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\wedge {q}\in \mathrm{HAtoms}\right)\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\to \left(\left({q}\subseteq {A}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\to {q}\cap {r}={0}_{ℋ}\right)$
27 atelch ${⊢}{p}\in \mathrm{HAtoms}\to {p}\in {\mathbf{C}}_{ℋ}$
28 atelch ${⊢}{q}\in \mathrm{HAtoms}\to {q}\in {\mathbf{C}}_{ℋ}$
29 chjcom ${⊢}\left({p}\in {\mathbf{C}}_{ℋ}\wedge {q}\in {\mathbf{C}}_{ℋ}\right)\to {p}{\vee }_{ℋ}{q}={q}{\vee }_{ℋ}{p}$
30 27 28 29 syl2an ${⊢}\left({p}\in \mathrm{HAtoms}\wedge {q}\in \mathrm{HAtoms}\right)\to {p}{\vee }_{ℋ}{q}={q}{\vee }_{ℋ}{p}$
31 30 adantlr ${⊢}\left(\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\wedge {q}\in \mathrm{HAtoms}\right)\to {p}{\vee }_{ℋ}{q}={q}{\vee }_{ℋ}{p}$
32 31 sseq2d ${⊢}\left(\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\wedge {q}\in \mathrm{HAtoms}\right)\to \left({r}\subseteq {p}{\vee }_{ℋ}{q}↔{r}\subseteq {q}{\vee }_{ℋ}{p}\right)$
33 atexch ${⊢}\left({q}\in {\mathbf{C}}_{ℋ}\wedge {r}\in \mathrm{HAtoms}\wedge {p}\in \mathrm{HAtoms}\right)\to \left(\left({r}\subseteq {q}{\vee }_{ℋ}{p}\wedge {q}\cap {r}={0}_{ℋ}\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)$
34 28 33 syl3an1 ${⊢}\left({q}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\wedge {p}\in \mathrm{HAtoms}\right)\to \left(\left({r}\subseteq {q}{\vee }_{ℋ}{p}\wedge {q}\cap {r}={0}_{ℋ}\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)$
35 34 3com13 ${⊢}\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\wedge {q}\in \mathrm{HAtoms}\right)\to \left(\left({r}\subseteq {q}{\vee }_{ℋ}{p}\wedge {q}\cap {r}={0}_{ℋ}\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)$
36 35 3expa ${⊢}\left(\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\wedge {q}\in \mathrm{HAtoms}\right)\to \left(\left({r}\subseteq {q}{\vee }_{ℋ}{p}\wedge {q}\cap {r}={0}_{ℋ}\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)$
37 36 expd ${⊢}\left(\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\wedge {q}\in \mathrm{HAtoms}\right)\to \left({r}\subseteq {q}{\vee }_{ℋ}{p}\to \left({q}\cap {r}={0}_{ℋ}\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)\right)$
38 32 37 sylbid ${⊢}\left(\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\wedge {q}\in \mathrm{HAtoms}\right)\to \left({r}\subseteq {p}{\vee }_{ℋ}{q}\to \left({q}\cap {r}={0}_{ℋ}\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)\right)$
39 38 imp ${⊢}\left(\left(\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\wedge {q}\in \mathrm{HAtoms}\right)\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\to \left({q}\cap {r}={0}_{ℋ}\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)$
40 26 39 syld ${⊢}\left(\left(\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\wedge {q}\in \mathrm{HAtoms}\right)\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\to \left(\left({q}\subseteq {A}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)$
41 40 expd ${⊢}\left(\left(\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\wedge {q}\in \mathrm{HAtoms}\right)\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\to \left({q}\subseteq {A}\to \left(\left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)\right)$
42 41 exp31 ${⊢}\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\to \left({q}\in \mathrm{HAtoms}\to \left({r}\subseteq {p}{\vee }_{ℋ}{q}\to \left({q}\subseteq {A}\to \left(\left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)\right)\right)\right)$
43 42 com24 ${⊢}\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\to \left({q}\subseteq {A}\to \left({r}\subseteq {p}{\vee }_{ℋ}{q}\to \left({q}\in \mathrm{HAtoms}\to \left(\left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)\right)\right)\right)$
44 43 impd ${⊢}\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\to \left(\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\to \left({q}\in \mathrm{HAtoms}\to \left(\left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)\right)\right)$
45 44 com24 ${⊢}\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\to \left(\left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\to \left({q}\in \mathrm{HAtoms}\to \left(\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)\right)\right)$
46 45 imp4b ${⊢}\left(\left({p}\in \mathrm{HAtoms}\wedge {r}\in \mathrm{HAtoms}\right)\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\to \left(\left({q}\in \mathrm{HAtoms}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)$
47 46 anasss ${⊢}\left({p}\in \mathrm{HAtoms}\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to \left(\left({q}\in \mathrm{HAtoms}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)\to {p}\subseteq {q}{\vee }_{ℋ}{r}\right)$
48 simprl ${⊢}\left({q}\in \mathrm{HAtoms}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)\to {q}\subseteq {A}$
49 48 a1i ${⊢}\left({p}\in \mathrm{HAtoms}\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to \left(\left({q}\in \mathrm{HAtoms}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)\to {q}\subseteq {A}\right)$
50 simpl ${⊢}\left({r}\subseteq {B}\wedge {r}\subseteq {C}\right)\to {r}\subseteq {B}$
51 4 50 sylbir ${⊢}{r}\subseteq {B}\cap {C}\to {r}\subseteq {B}$
52 51 ad2antrl ${⊢}\left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\to {r}\subseteq {B}$
53 52 adantl ${⊢}\left({p}\in \mathrm{HAtoms}\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to {r}\subseteq {B}$
54 49 53 jctird ${⊢}\left({p}\in \mathrm{HAtoms}\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to \left(\left({q}\in \mathrm{HAtoms}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)\to \left({q}\subseteq {A}\wedge {r}\subseteq {B}\right)\right)$
55 47 54 jcad ${⊢}\left({p}\in \mathrm{HAtoms}\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to \left(\left({q}\in \mathrm{HAtoms}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\right)\to \left({p}\subseteq {q}{\vee }_{ℋ}{r}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {B}\right)\right)\right)$
56 55 expd ${⊢}\left({p}\in \mathrm{HAtoms}\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to \left({q}\in \mathrm{HAtoms}\to \left(\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\to \left({p}\subseteq {q}{\vee }_{ℋ}{r}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {B}\right)\right)\right)\right)$
57 56 adantlr ${⊢}\left(\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to \left({q}\in \mathrm{HAtoms}\to \left(\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\to \left({p}\subseteq {q}{\vee }_{ℋ}{r}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {B}\right)\right)\right)\right)$
58 57 adantlr ${⊢}\left(\left(\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\wedge {p}\subseteq {A}{\vee }_{ℋ}{B}\right)\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to \left({q}\in \mathrm{HAtoms}\to \left(\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\to \left({p}\subseteq {q}{\vee }_{ℋ}{r}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {B}\right)\right)\right)\right)$
59 58 adantlr ${⊢}\left(\left(\left(\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\wedge {p}\subseteq {A}{\vee }_{ℋ}{B}\right)\wedge {A}\ne {0}_{ℋ}\right)\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to \left({q}\in \mathrm{HAtoms}\to \left(\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\to \left({p}\subseteq {q}{\vee }_{ℋ}{r}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {B}\right)\right)\right)\right)$
60 59 reximdvai ${⊢}\left(\left(\left(\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\wedge {p}\subseteq {A}{\vee }_{ℋ}{B}\right)\wedge {A}\ne {0}_{ℋ}\right)\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to \left(\exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({q}\subseteq {A}\wedge {r}\subseteq {p}{\vee }_{ℋ}{q}\right)\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({p}\subseteq {q}{\vee }_{ℋ}{r}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {B}\right)\right)\right)$
61 19 60 mpd ${⊢}\left(\left(\left(\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\wedge {p}\subseteq {A}{\vee }_{ℋ}{B}\right)\wedge {A}\ne {0}_{ℋ}\right)\wedge \left({r}\in \mathrm{HAtoms}\wedge \left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)\right)\to \exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({p}\subseteq {q}{\vee }_{ℋ}{r}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {B}\right)\right)$
62 chjcl ${⊢}\left({A}\in {\mathbf{C}}_{ℋ}\wedge {p}\in {\mathbf{C}}_{ℋ}\right)\to {A}{\vee }_{ℋ}{p}\in {\mathbf{C}}_{ℋ}$
63 1 62 mpan ${⊢}{p}\in {\mathbf{C}}_{ℋ}\to {A}{\vee }_{ℋ}{p}\in {\mathbf{C}}_{ℋ}$
64 3 63 eqeltrid ${⊢}{p}\in {\mathbf{C}}_{ℋ}\to {C}\in {\mathbf{C}}_{ℋ}$
65 chincl ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {B}\cap {C}\in {\mathbf{C}}_{ℋ}$
66 2 64 65 sylancr ${⊢}{p}\in {\mathbf{C}}_{ℋ}\to {B}\cap {C}\in {\mathbf{C}}_{ℋ}$
67 27 66 syl ${⊢}{p}\in \mathrm{HAtoms}\to {B}\cap {C}\in {\mathbf{C}}_{ℋ}$
68 chrelat2 ${⊢}\left({B}\cap {C}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \left(¬{B}\cap {C}\subseteq {A}↔\exists {r}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)$
69 67 1 68 sylancl ${⊢}{p}\in \mathrm{HAtoms}\to \left(¬{B}\cap {C}\subseteq {A}↔\exists {r}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)\right)$
70 69 biimpa ${⊢}\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\to \exists {r}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)$
71 70 ad2antrr ${⊢}\left(\left(\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\wedge {p}\subseteq {A}{\vee }_{ℋ}{B}\right)\wedge {A}\ne {0}_{ℋ}\right)\to \exists {r}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({r}\subseteq {B}\cap {C}\wedge ¬{r}\subseteq {A}\right)$
72 61 71 reximddv ${⊢}\left(\left(\left({p}\in \mathrm{HAtoms}\wedge ¬{B}\cap {C}\subseteq {A}\right)\wedge {p}\subseteq {A}{\vee }_{ℋ}{B}\right)\wedge {A}\ne {0}_{ℋ}\right)\to \exists {r}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\exists {q}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}\left({p}\subseteq {q}{\vee }_{ℋ}{r}\wedge \left({q}\subseteq {A}\wedge {r}\subseteq {B}\right)\right)$