Metamath Proof Explorer


Theorem cdlemb2

Description: Given two atoms not under the fiducial (reference) co-atom W , there is a third. Lemma B in Crawley p. 112. (Contributed by NM, 30-May-2012)

Ref Expression
Hypotheses cdlemb2.l ˙=K
cdlemb2.j ˙=joinK
cdlemb2.a A=AtomsK
cdlemb2.h H=LHypK
Assertion cdlemb2 KHLWHPA¬P˙WQA¬Q˙WPQrA¬r˙W¬r˙P˙Q

Proof

Step Hyp Ref Expression
1 cdlemb2.l ˙=K
2 cdlemb2.j ˙=joinK
3 cdlemb2.a A=AtomsK
4 cdlemb2.h H=LHypK
5 simp1l KHLWHPA¬P˙WQA¬Q˙WPQKHL
6 simp2ll KHLWHPA¬P˙WQA¬Q˙WPQPA
7 simp2rl KHLWHPA¬P˙WQA¬Q˙WPQQA
8 simp1r KHLWHPA¬P˙WQA¬Q˙WPQWH
9 eqid BaseK=BaseK
10 9 4 lhpbase WHWBaseK
11 8 10 syl KHLWHPA¬P˙WQA¬Q˙WPQWBaseK
12 simp3 KHLWHPA¬P˙WQA¬Q˙WPQPQ
13 eqid 1.K=1.K
14 eqid K=K
15 13 14 4 lhp1cvr KHLWHWK1.K
16 15 3ad2ant1 KHLWHPA¬P˙WQA¬Q˙WPQWK1.K
17 simp2lr KHLWHPA¬P˙WQA¬Q˙WPQ¬P˙W
18 simp2rr KHLWHPA¬P˙WQA¬Q˙WPQ¬Q˙W
19 9 1 2 13 14 3 cdlemb KHLPAQAWBaseKPQWK1.K¬P˙W¬Q˙WrA¬r˙W¬r˙P˙Q
20 5 6 7 11 12 16 17 18 19 syl323anc KHLWHPA¬P˙WQA¬Q˙WPQrA¬r˙W¬r˙P˙Q