Metamath Proof Explorer


Theorem cdlemg5

Description: TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle ? TODO: The .\/ hypothesis is unused. FIX COMMENT. (Contributed by NM, 26-Apr-2013)

Ref Expression
Hypotheses cdlemg5.l ˙=K
cdlemg5.j ˙=joinK
cdlemg5.a A=AtomsK
cdlemg5.h H=LHypK
Assertion cdlemg5 KHLWHPA¬P˙WqAPq¬q˙W

Proof

Step Hyp Ref Expression
1 cdlemg5.l ˙=K
2 cdlemg5.j ˙=joinK
3 cdlemg5.a A=AtomsK
4 cdlemg5.h H=LHypK
5 1 3 4 lhpexle KHLWHrAr˙W
6 5 adantr KHLWHPA¬P˙WrAr˙W
7 simpll KHLWHPA¬P˙WrAr˙WKHLWH
8 simpr KHLWHPA¬P˙WrAr˙WrAr˙W
9 simplr KHLWHPA¬P˙WrAr˙WPA¬P˙W
10 1 2 3 4 cdlemf1 KHLWHrAr˙WPA¬P˙WqAPq¬q˙Wr˙P˙q
11 7 8 9 10 syl3anc KHLWHPA¬P˙WrAr˙WqAPq¬q˙Wr˙P˙q
12 3simpa Pq¬q˙Wr˙P˙qPq¬q˙W
13 12 reximi qAPq¬q˙Wr˙P˙qqAPq¬q˙W
14 11 13 syl KHLWHPA¬P˙WrAr˙WqAPq¬q˙W
15 6 14 rexlimddv KHLWHPA¬P˙WqAPq¬q˙W