Metamath Proof Explorer


Theorem cdleme17d3

Description: TODO: FIX COMMENT. (Contributed by NM, 5-Apr-2013)

Ref Expression
Hypotheses cdlemef46.b B=BaseK
cdlemef46.l ˙=K
cdlemef46.j ˙=joinK
cdlemef46.m ˙=meetK
cdlemef46.a A=AtomsK
cdlemef46.h H=LHypK
cdlemef46.u U=P˙Q˙W
cdlemef46.d D=t˙U˙Q˙P˙t˙W
cdlemefs46.e E=P˙Q˙D˙s˙t˙W
cdlemef46.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
Assertion cdleme17d3 KHLWHPA¬P˙WQA¬Q˙WPQFP=Q

Proof

Step Hyp Ref Expression
1 cdlemef46.b B=BaseK
2 cdlemef46.l ˙=K
3 cdlemef46.j ˙=joinK
4 cdlemef46.m ˙=meetK
5 cdlemef46.a A=AtomsK
6 cdlemef46.h H=LHypK
7 cdlemef46.u U=P˙Q˙W
8 cdlemef46.d D=t˙U˙Q˙P˙t˙W
9 cdlemefs46.e E=P˙Q˙D˙s˙t˙W
10 cdlemef46.f F=xBifPQ¬x˙WιzB|sA¬s˙Ws˙x˙W=xz=ifs˙P˙QιyB|tA¬t˙W¬t˙P˙Qy=Es/tD˙x˙Wx
11 simpl1 KHLWHPA¬P˙WQA¬Q˙WPQKHLWH
12 simpl2 KHLWHPA¬P˙WQA¬Q˙WPQPA¬P˙W
13 simpl3 KHLWHPA¬P˙WQA¬Q˙WPQQA¬Q˙W
14 simpr KHLWHPA¬P˙WQA¬Q˙WPQPQ
15 2 3 5 6 cdlemb2 KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙Q
16 11 12 13 14 15 syl121anc KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙Q
17 simp1 KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙QKHLWHPA¬P˙WQA¬Q˙W
18 simp2 KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙QPQ
19 simp3l KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙QeA
20 simp3rl KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙Q¬e˙W
21 19 20 jca KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙QeA¬e˙W
22 simp3rr KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙Q¬e˙P˙Q
23 1 2 3 4 5 6 7 8 9 10 cdleme17d2 KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙QFP=Q
24 17 18 21 22 23 syl121anc KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙QFP=Q
25 24 3expia KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙QFP=Q
26 25 expd KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙QFP=Q
27 26 rexlimdv KHLWHPA¬P˙WQA¬Q˙WPQeA¬e˙W¬e˙P˙QFP=Q
28 16 27 mpd KHLWHPA¬P˙WQA¬Q˙WPQFP=Q