# Metamath Proof Explorer

## Theorem atcvatlem

Description: Lemma for atcvati . (Contributed by NM, 27-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypothesis atoml.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
Assertion atcvatlem ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left({A}\ne {0}_{ℋ}\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to \left(¬{B}\subseteq {A}\to {A}\in \mathrm{HAtoms}\right)$

### Proof

Step Hyp Ref Expression
1 atoml.1 ${⊢}{A}\in {\mathbf{C}}_{ℋ}$
2 1 hatomici ${⊢}{A}\ne {0}_{ℋ}\to \exists {x}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}{x}\subseteq {A}$
3 nssne2 ${⊢}\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\to {x}\ne {B}$
4 3 adantrl ${⊢}\left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\to {x}\ne {B}$
5 atnemeq0 ${⊢}\left({x}\in \mathrm{HAtoms}\wedge {B}\in \mathrm{HAtoms}\right)\to \left({x}\ne {B}↔{x}\cap {B}={0}_{ℋ}\right)$
6 4 5 syl5ib ${⊢}\left({x}\in \mathrm{HAtoms}\wedge {B}\in \mathrm{HAtoms}\right)\to \left(\left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\to {x}\cap {B}={0}_{ℋ}\right)$
7 atelch ${⊢}{x}\in \mathrm{HAtoms}\to {x}\in {\mathbf{C}}_{ℋ}$
8 cvp ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to \left({x}\cap {B}={0}_{ℋ}↔{x}{⋖}_{ℋ}\left({x}{\vee }_{ℋ}{B}\right)\right)$
9 atelch ${⊢}{B}\in \mathrm{HAtoms}\to {B}\in {\mathbf{C}}_{ℋ}$
10 chjcom ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}\in {\mathbf{C}}_{ℋ}\right)\to {x}{\vee }_{ℋ}{B}={B}{\vee }_{ℋ}{x}$
11 9 10 sylan2 ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to {x}{\vee }_{ℋ}{B}={B}{\vee }_{ℋ}{x}$
12 11 breq2d ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to \left({x}{⋖}_{ℋ}\left({x}{\vee }_{ℋ}{B}\right)↔{x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\right)$
13 8 12 bitrd ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}\in \mathrm{HAtoms}\right)\to \left({x}\cap {B}={0}_{ℋ}↔{x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\right)$
14 7 13 sylan ${⊢}\left({x}\in \mathrm{HAtoms}\wedge {B}\in \mathrm{HAtoms}\right)\to \left({x}\cap {B}={0}_{ℋ}↔{x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\right)$
15 6 14 sylibd ${⊢}\left({x}\in \mathrm{HAtoms}\wedge {B}\in \mathrm{HAtoms}\right)\to \left(\left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\to {x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\right)$
16 15 ancoms ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\right)\to \left(\left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\to {x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\right)$
17 16 adantlr ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\to \left(\left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\to {x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\right)$
18 17 imp ${⊢}\left(\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\right)\to {x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)$
19 chub1 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {B}\subseteq {B}{\vee }_{ℋ}{x}$
20 9 7 19 syl2an ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\right)\to {B}\subseteq {B}{\vee }_{ℋ}{x}$
21 20 3adant3 ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\to {B}\subseteq {B}{\vee }_{ℋ}{x}$
22 21 adantr ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to {B}\subseteq {B}{\vee }_{ℋ}{x}$
23 pssss ${⊢}{A}\subset {B}{\vee }_{ℋ}{C}\to {A}\subseteq {B}{\vee }_{ℋ}{C}$
24 sstr ${⊢}\left({x}\subseteq {A}\wedge {A}\subseteq {B}{\vee }_{ℋ}{C}\right)\to {x}\subseteq {B}{\vee }_{ℋ}{C}$
25 23 24 sylan2 ${⊢}\left({x}\subseteq {A}\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\to {x}\subseteq {B}{\vee }_{ℋ}{C}$
26 25 adantlr ${⊢}\left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\to {x}\subseteq {B}{\vee }_{ℋ}{C}$
27 26 adantl ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to {x}\subseteq {B}{\vee }_{ℋ}{C}$
28 incom ${⊢}{B}\cap {x}={x}\cap {B}$
29 3 5 syl5ib ${⊢}\left({x}\in \mathrm{HAtoms}\wedge {B}\in \mathrm{HAtoms}\right)\to \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\to {x}\cap {B}={0}_{ℋ}\right)$
30 29 ancoms ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\right)\to \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\to {x}\cap {B}={0}_{ℋ}\right)$
31 30 3adant3 ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\to \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\to {x}\cap {B}={0}_{ℋ}\right)$
32 31 imp ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\right)\to {x}\cap {B}={0}_{ℋ}$
33 28 32 syl5eq ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\right)\to {B}\cap {x}={0}_{ℋ}$
34 33 adantrr ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to {B}\cap {x}={0}_{ℋ}$
35 atexch ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\to \left(\left({x}\subseteq {B}{\vee }_{ℋ}{C}\wedge {B}\cap {x}={0}_{ℋ}\right)\to {C}\subseteq {B}{\vee }_{ℋ}{x}\right)$
36 9 35 syl3an1 ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\to \left(\left({x}\subseteq {B}{\vee }_{ℋ}{C}\wedge {B}\cap {x}={0}_{ℋ}\right)\to {C}\subseteq {B}{\vee }_{ℋ}{x}\right)$
37 36 adantr ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to \left(\left({x}\subseteq {B}{\vee }_{ℋ}{C}\wedge {B}\cap {x}={0}_{ℋ}\right)\to {C}\subseteq {B}{\vee }_{ℋ}{x}\right)$
38 27 34 37 mp2and ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to {C}\subseteq {B}{\vee }_{ℋ}{x}$
39 atelch ${⊢}{C}\in \mathrm{HAtoms}\to {C}\in {\mathbf{C}}_{ℋ}$
40 simp1 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {B}\in {\mathbf{C}}_{ℋ}$
41 simp3 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {C}\in {\mathbf{C}}_{ℋ}$
42 chjcl ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}$
43 42 3adant3 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}$
44 40 41 43 3jca ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left({B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\wedge {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}\right)$
45 9 7 39 44 syl3an ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\to \left({B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\wedge {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}\right)$
46 chlub ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\wedge {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({B}\subseteq {B}{\vee }_{ℋ}{x}\wedge {C}\subseteq {B}{\vee }_{ℋ}{x}\right)↔{B}{\vee }_{ℋ}{C}\subseteq {B}{\vee }_{ℋ}{x}\right)$
47 45 46 syl ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\to \left(\left({B}\subseteq {B}{\vee }_{ℋ}{x}\wedge {C}\subseteq {B}{\vee }_{ℋ}{x}\right)↔{B}{\vee }_{ℋ}{C}\subseteq {B}{\vee }_{ℋ}{x}\right)$
48 47 adantr ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to \left(\left({B}\subseteq {B}{\vee }_{ℋ}{x}\wedge {C}\subseteq {B}{\vee }_{ℋ}{x}\right)↔{B}{\vee }_{ℋ}{C}\subseteq {B}{\vee }_{ℋ}{x}\right)$
49 22 38 48 mpbi2and ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to {B}{\vee }_{ℋ}{C}\subseteq {B}{\vee }_{ℋ}{x}$
50 chub1 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {B}\subseteq {B}{\vee }_{ℋ}{C}$
51 50 3adant2 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {B}\subseteq {B}{\vee }_{ℋ}{C}$
52 51 26 anim12i ${⊢}\left(\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to \left({B}\subseteq {B}{\vee }_{ℋ}{C}\wedge {x}\subseteq {B}{\vee }_{ℋ}{C}\right)$
53 chjcl ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {B}{\vee }_{ℋ}{C}\in {\mathbf{C}}_{ℋ}$
54 53 3adant2 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to {B}{\vee }_{ℋ}{C}\in {\mathbf{C}}_{ℋ}$
55 chlub ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {B}{\vee }_{ℋ}{C}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({B}\subseteq {B}{\vee }_{ℋ}{C}\wedge {x}\subseteq {B}{\vee }_{ℋ}{C}\right)↔{B}{\vee }_{ℋ}{x}\subseteq {B}{\vee }_{ℋ}{C}\right)$
56 54 55 syld3an3 ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\to \left(\left({B}\subseteq {B}{\vee }_{ℋ}{C}\wedge {x}\subseteq {B}{\vee }_{ℋ}{C}\right)↔{B}{\vee }_{ℋ}{x}\subseteq {B}{\vee }_{ℋ}{C}\right)$
57 56 adantr ${⊢}\left(\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to \left(\left({B}\subseteq {B}{\vee }_{ℋ}{C}\wedge {x}\subseteq {B}{\vee }_{ℋ}{C}\right)↔{B}{\vee }_{ℋ}{x}\subseteq {B}{\vee }_{ℋ}{C}\right)$
58 52 57 mpbid ${⊢}\left(\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\wedge {C}\in {\mathbf{C}}_{ℋ}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to {B}{\vee }_{ℋ}{x}\subseteq {B}{\vee }_{ℋ}{C}$
59 9 7 39 58 syl3anl ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to {B}{\vee }_{ℋ}{x}\subseteq {B}{\vee }_{ℋ}{C}$
60 49 59 eqssd ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left(\left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to {B}{\vee }_{ℋ}{C}={B}{\vee }_{ℋ}{x}$
61 60 anassrs ${⊢}\left(\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\to {B}{\vee }_{ℋ}{C}={B}{\vee }_{ℋ}{x}$
62 61 psseq2d ${⊢}\left(\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\right)\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\to \left({A}\subset {B}{\vee }_{ℋ}{C}↔{A}\subset {B}{\vee }_{ℋ}{x}\right)$
63 62 ex ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\right)\to \left({A}\subset {B}{\vee }_{ℋ}{C}\to \left({A}\subset {B}{\vee }_{ℋ}{C}↔{A}\subset {B}{\vee }_{ℋ}{x}\right)\right)$
64 63 ibd ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge ¬{B}\subseteq {A}\right)\right)\to \left({A}\subset {B}{\vee }_{ℋ}{C}\to {A}\subset {B}{\vee }_{ℋ}{x}\right)$
65 64 exp32 ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\to \left({x}\subseteq {A}\to \left(¬{B}\subseteq {A}\to \left({A}\subset {B}{\vee }_{ℋ}{C}\to {A}\subset {B}{\vee }_{ℋ}{x}\right)\right)\right)$
66 65 3expa ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\right)\wedge {C}\in \mathrm{HAtoms}\right)\to \left({x}\subseteq {A}\to \left(¬{B}\subseteq {A}\to \left({A}\subset {B}{\vee }_{ℋ}{C}\to {A}\subset {B}{\vee }_{ℋ}{x}\right)\right)\right)$
67 66 an32s ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\to \left({x}\subseteq {A}\to \left(¬{B}\subseteq {A}\to \left({A}\subset {B}{\vee }_{ℋ}{C}\to {A}\subset {B}{\vee }_{ℋ}{x}\right)\right)\right)$
68 67 com34 ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\to \left({x}\subseteq {A}\to \left({A}\subset {B}{\vee }_{ℋ}{C}\to \left(¬{B}\subseteq {A}\to {A}\subset {B}{\vee }_{ℋ}{x}\right)\right)\right)$
69 68 imp45 ${⊢}\left(\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\right)\to {A}\subset {B}{\vee }_{ℋ}{x}$
70 simpr ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to {x}\in {\mathbf{C}}_{ℋ}$
71 70 42 jca ${⊢}\left({B}\in {\mathbf{C}}_{ℋ}\wedge {x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}\right)$
72 9 7 71 syl2an ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\right)\to \left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}\right)$
73 cvnbtwn3 ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}\wedge {A}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\to \left(\left({x}\subseteq {A}\wedge {A}\subset {B}{\vee }_{ℋ}{x}\right)\to {A}={x}\right)\right)$
74 1 73 mp3an3 ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\to \left(\left({x}\subseteq {A}\wedge {A}\subset {B}{\vee }_{ℋ}{x}\right)\to {A}={x}\right)\right)$
75 74 exp4a ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\to \left({x}\subseteq {A}\to \left({A}\subset {B}{\vee }_{ℋ}{x}\to {A}={x}\right)\right)\right)$
76 75 com23 ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}\subseteq {A}\to \left({x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\to \left({A}\subset {B}{\vee }_{ℋ}{x}\to {A}={x}\right)\right)\right)$
77 76 imp4a ${⊢}\left({x}\in {\mathbf{C}}_{ℋ}\wedge {B}{\vee }_{ℋ}{x}\in {\mathbf{C}}_{ℋ}\right)\to \left({x}\subseteq {A}\to \left(\left({x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{x}\right)\to {A}={x}\right)\right)$
78 72 77 syl ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {x}\in \mathrm{HAtoms}\right)\to \left({x}\subseteq {A}\to \left(\left({x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{x}\right)\to {A}={x}\right)\right)$
79 78 adantlr ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\to \left({x}\subseteq {A}\to \left(\left({x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{x}\right)\to {A}={x}\right)\right)$
80 79 imp ${⊢}\left(\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\wedge {x}\subseteq {A}\right)\to \left(\left({x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{x}\right)\to {A}={x}\right)$
81 80 adantrr ${⊢}\left(\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\right)\to \left(\left({x}{⋖}_{ℋ}\left({B}{\vee }_{ℋ}{x}\right)\wedge {A}\subset {B}{\vee }_{ℋ}{x}\right)\to {A}={x}\right)$
82 18 69 81 mp2and ${⊢}\left(\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\right)\to {A}={x}$
83 82 eleq1d ${⊢}\left(\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\right)\to \left({A}\in \mathrm{HAtoms}↔{x}\in \mathrm{HAtoms}\right)$
84 83 biimprcd ${⊢}{x}\in \mathrm{HAtoms}\to \left(\left(\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\wedge \left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\right)\to {A}\in \mathrm{HAtoms}\right)$
85 84 exp4c ${⊢}{x}\in \mathrm{HAtoms}\to \left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\to \left({x}\in \mathrm{HAtoms}\to \left(\left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\to {A}\in \mathrm{HAtoms}\right)\right)\right)$
86 85 pm2.43b ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\to \left({x}\in \mathrm{HAtoms}\to \left(\left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\to {A}\in \mathrm{HAtoms}\right)\right)$
87 86 imp ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\to \left(\left({x}\subseteq {A}\wedge \left({A}\subset {B}{\vee }_{ℋ}{C}\wedge ¬{B}\subseteq {A}\right)\right)\to {A}\in \mathrm{HAtoms}\right)$
88 87 exp4d ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge {x}\in \mathrm{HAtoms}\right)\to \left({x}\subseteq {A}\to \left({A}\subset {B}{\vee }_{ℋ}{C}\to \left(¬{B}\subseteq {A}\to {A}\in \mathrm{HAtoms}\right)\right)\right)$
89 88 rexlimdva ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\to \left(\exists {x}\in \mathrm{HAtoms}\phantom{\rule{.4em}{0ex}}{x}\subseteq {A}\to \left({A}\subset {B}{\vee }_{ℋ}{C}\to \left(¬{B}\subseteq {A}\to {A}\in \mathrm{HAtoms}\right)\right)\right)$
90 2 89 syl5 ${⊢}\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\to \left({A}\ne {0}_{ℋ}\to \left({A}\subset {B}{\vee }_{ℋ}{C}\to \left(¬{B}\subseteq {A}\to {A}\in \mathrm{HAtoms}\right)\right)\right)$
91 90 imp32 ${⊢}\left(\left({B}\in \mathrm{HAtoms}\wedge {C}\in \mathrm{HAtoms}\right)\wedge \left({A}\ne {0}_{ℋ}\wedge {A}\subset {B}{\vee }_{ℋ}{C}\right)\right)\to \left(¬{B}\subseteq {A}\to {A}\in \mathrm{HAtoms}\right)$