# Metamath Proof Explorer

## Theorem cdlemk19-2N

Description: Part of proof of Lemma K of Crawley p. 118. Line 22 on p. 119. N , V , Q , C are k, sigma_2 (p), k_2, f_2. (Contributed by NM, 2-Jul-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemk2.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
cdlemk2.l
cdlemk2.j
cdlemk2.m
cdlemk2.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
cdlemk2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
cdlemk2.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
cdlemk2.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
cdlemk2.s
cdlemk2.q ${⊢}{Q}={S}\left({C}\right)$
cdlemk2.v
Assertion cdlemk19-2N

### Proof

Step Hyp Ref Expression
1 cdlemk2.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 cdlemk2.l
3 cdlemk2.j
4 cdlemk2.m
5 cdlemk2.a ${⊢}{A}=\mathrm{Atoms}\left({K}\right)$
6 cdlemk2.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
7 cdlemk2.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
8 cdlemk2.r ${⊢}{R}=\mathrm{trL}\left({K}\right)\left({W}\right)$
9 cdlemk2.s
10 cdlemk2.q ${⊢}{Q}={S}\left({C}\right)$
11 cdlemk2.v
12 simp11
13 simp12
14 12 13 jca
15 simp21
16 simp22
17 simp23
18 simp33
19 simp13
20 simp32l
21 simp32r
22 simp31
23 1 2 3 4 5 6 7 8 9 10 11 cdlemk19
24 14 15 16 17 18 19 20 21 22 23 syl333anc