# Metamath Proof Explorer

## Theorem cdleme27cl

Description: Part of proof of Lemma E in Crawley p. 113. Closure of C . (Contributed by NM, 6-Feb-2013)

Ref Expression
Hypotheses cdleme26.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdleme26.l
cdleme26.j
cdleme26.m
cdleme26.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdleme26.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdleme27.u
cdleme27.f
cdleme27.z
cdleme27.n
cdleme27.d
cdleme27.c
Assertion cdleme27cl

### Proof

Step Hyp Ref Expression
1 cdleme26.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdleme26.l
3 cdleme26.j
4 cdleme26.m
5 cdleme26.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdleme26.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdleme27.u
8 cdleme27.f
9 cdleme27.z
10 cdleme27.n
11 cdleme27.d
12 cdleme27.c
13 simpl1
14 simpl2l
15 simpl2r
16 simpl3l
17 simpl3r
18 simpr
19 1 2 3 4 5 6 7 9 10 11 cdleme25cl
20 13 14 15 16 17 18 19 syl312anc
21 simp1l
22 simp1r
23 simp2ll
24 simp2rl
25 simp3ll
26 2 3 4 5 6 7 8 1 cdleme1b ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge \left({P}\in {A}\wedge {Q}\in {A}\wedge {s}\in {A}\right)\right)\to {F}\in {B}$
27 21 22 23 24 25 26 syl23anc