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 | |
|
cdlemg5.j | |
||
cdlemg5.a | |
||
cdlemg5.h | |
||
Assertion | cdlemb3 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemg5.l | |
|
2 | cdlemg5.j | |
|
3 | cdlemg5.a | |
|
4 | cdlemg5.h | |
|
5 | simpl1 | |
|
6 | simpl2 | |
|
7 | 1 2 3 4 | cdlemg5 | |
8 | 5 6 7 | syl2anc | |
9 | ancom | |
|
10 | eqcom | |
|
11 | simp2 | |
|
12 | 11 | oveq2d | |
13 | simp11l | |
|
14 | simp12l | |
|
15 | 2 3 | hlatjidm | |
16 | 13 14 15 | syl2anc | |
17 | 12 16 | eqtr3d | |
18 | 17 | breq2d | |
19 | hlatl | |
|
20 | 13 19 | syl | |
21 | simp3 | |
|
22 | 1 3 | atcmp | |
23 | 20 21 14 22 | syl3anc | |
24 | 18 23 | bitr2d | |
25 | 10 24 | syl5bb | |
26 | 25 | necon3abid | |
27 | 26 | anbi2d | |
28 | 9 27 | syl5bb | |
29 | 28 | 3expa | |
30 | 29 | rexbidva | |
31 | 8 30 | mpbid | |
32 | simpl1 | |
|
33 | simpl2 | |
|
34 | simpl3 | |
|
35 | simpr | |
|
36 | 1 2 3 4 | cdlemb2 | |
37 | 32 33 34 35 36 | syl121anc | |
38 | 31 37 | pm2.61dane | |