Metamath Proof Explorer


Theorem cdlemb3

Description: Given two atoms not under the fiducial co-atom W , there is a third. Lemma B in Crawley p. 112. TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle ? Then replace cdlemb2 with it. This is a more general version of cdlemb2 without P =/= Q condition. (Contributed by NM, 27-Apr-2013)

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

Proof

Step Hyp Ref Expression
1 cdlemg5.l ˙=K
2 cdlemg5.j ˙=joinK
3 cdlemg5.a A=AtomsK
4 cdlemg5.h H=LHypK
5 simpl1 KHLWHPA¬P˙WQA¬Q˙WP=QKHLWH
6 simpl2 KHLWHPA¬P˙WQA¬Q˙WP=QPA¬P˙W
7 1 2 3 4 cdlemg5 KHLWHPA¬P˙WrAPr¬r˙W
8 5 6 7 syl2anc KHLWHPA¬P˙WQA¬Q˙WP=QrAPr¬r˙W
9 ancom Pr¬r˙W¬r˙WPr
10 eqcom P=rr=P
11 simp2 KHLWHPA¬P˙WQA¬Q˙WP=QrAP=Q
12 11 oveq2d KHLWHPA¬P˙WQA¬Q˙WP=QrAP˙P=P˙Q
13 simp11l KHLWHPA¬P˙WQA¬Q˙WP=QrAKHL
14 simp12l KHLWHPA¬P˙WQA¬Q˙WP=QrAPA
15 2 3 hlatjidm KHLPAP˙P=P
16 13 14 15 syl2anc KHLWHPA¬P˙WQA¬Q˙WP=QrAP˙P=P
17 12 16 eqtr3d KHLWHPA¬P˙WQA¬Q˙WP=QrAP˙Q=P
18 17 breq2d KHLWHPA¬P˙WQA¬Q˙WP=QrAr˙P˙Qr˙P
19 hlatl KHLKAtLat
20 13 19 syl KHLWHPA¬P˙WQA¬Q˙WP=QrAKAtLat
21 simp3 KHLWHPA¬P˙WQA¬Q˙WP=QrArA
22 1 3 atcmp KAtLatrAPAr˙Pr=P
23 20 21 14 22 syl3anc KHLWHPA¬P˙WQA¬Q˙WP=QrAr˙Pr=P
24 18 23 bitr2d KHLWHPA¬P˙WQA¬Q˙WP=QrAr=Pr˙P˙Q
25 10 24 syl5bb KHLWHPA¬P˙WQA¬Q˙WP=QrAP=rr˙P˙Q
26 25 necon3abid KHLWHPA¬P˙WQA¬Q˙WP=QrAPr¬r˙P˙Q
27 26 anbi2d KHLWHPA¬P˙WQA¬Q˙WP=QrA¬r˙WPr¬r˙W¬r˙P˙Q
28 9 27 syl5bb KHLWHPA¬P˙WQA¬Q˙WP=QrAPr¬r˙W¬r˙W¬r˙P˙Q
29 28 3expa KHLWHPA¬P˙WQA¬Q˙WP=QrAPr¬r˙W¬r˙W¬r˙P˙Q
30 29 rexbidva KHLWHPA¬P˙WQA¬Q˙WP=QrAPr¬r˙WrA¬r˙W¬r˙P˙Q
31 8 30 mpbid KHLWHPA¬P˙WQA¬Q˙WP=QrA¬r˙W¬r˙P˙Q
32 simpl1 KHLWHPA¬P˙WQA¬Q˙WPQKHLWH
33 simpl2 KHLWHPA¬P˙WQA¬Q˙WPQPA¬P˙W
34 simpl3 KHLWHPA¬P˙WQA¬Q˙WPQQA¬Q˙W
35 simpr KHLWHPA¬P˙WQA¬Q˙WPQPQ
36 1 2 3 4 cdlemb2 KHLWHPA¬P˙WQA¬Q˙WPQrA¬r˙W¬r˙P˙Q
37 32 33 34 35 36 syl121anc KHLWHPA¬P˙WQA¬Q˙WPQrA¬r˙W¬r˙P˙Q
38 31 37 pm2.61dane KHLWHPA¬P˙WQA¬Q˙WrA¬r˙W¬r˙P˙Q