Metamath Proof Explorer


Theorem cdleme18a

Description: Part of proof of Lemma E in Crawley p. 114, 2nd sentence of 4th paragraph. F , G represent f(s), f_s(q) respectively. We show -. f_s(q) <_ w. (Contributed by NM, 12-Oct-2012)

Ref Expression
Hypotheses cdleme18.l ˙=K
cdleme18.j ˙=joinK
cdleme18.m ˙=meetK
cdleme18.a A=AtomsK
cdleme18.h H=LHypK
cdleme18.u U=P˙Q˙W
cdleme18.f F=S˙U˙Q˙P˙S˙W
cdleme18.g G=P˙Q˙F˙Q˙S˙W
Assertion cdleme18a KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙Q¬G˙W

Proof

Step Hyp Ref Expression
1 cdleme18.l ˙=K
2 cdleme18.j ˙=joinK
3 cdleme18.m ˙=meetK
4 cdleme18.a A=AtomsK
5 cdleme18.h H=LHypK
6 cdleme18.u U=P˙Q˙W
7 cdleme18.f F=S˙U˙Q˙P˙S˙W
8 cdleme18.g G=P˙Q˙F˙Q˙S˙W
9 simp1 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QKHLWH
10 simp21 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QPA¬P˙W
11 simp22 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QQA¬Q˙W
12 simp23 KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QSA¬S˙W
13 simp3l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QPQ
14 simp1l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QKHL
15 simp21l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QPA
16 simp22l KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QQA
17 1 2 4 hlatlej2 KHLPAQAQ˙P˙Q
18 14 15 16 17 syl3anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙QQ˙P˙Q
19 simp3r KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙Q¬S˙P˙Q
20 1 2 3 4 5 6 7 8 cdleme7 KHLWHPA¬P˙WQA¬Q˙WQA¬Q˙WSA¬S˙WPQQ˙P˙Q¬S˙P˙Q¬G˙W
21 9 10 11 11 12 13 18 19 20 syl323anc KHLWHPA¬P˙WQA¬Q˙WSA¬S˙WPQ¬S˙P˙Q¬G˙W