Metamath Proof Explorer


Theorem cdleme35sn2aw

Description: Part of proof of Lemma E in Crawley p. 113. Show that f(x) is one-to-one outside of P .\/ Q line case; compare cdleme32sn2awN . TODO: FIX COMMENT. (Contributed by NM, 18-Mar-2013)

Ref Expression
Hypotheses cdleme32s.b B=BaseK
cdleme32s.l ˙=K
cdleme32s.j ˙=joinK
cdleme32s.m ˙=meetK
cdleme32s.a A=AtomsK
cdleme32s.h H=LHypK
cdleme32s.u U=P˙Q˙W
cdleme32s.d D=s˙U˙Q˙P˙s˙W
cdleme32s.n N=ifs˙P˙QID
Assertion cdleme35sn2aw KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙Q¬S˙P˙QRSR/sNS/sN

Proof

Step Hyp Ref Expression
1 cdleme32s.b B=BaseK
2 cdleme32s.l ˙=K
3 cdleme32s.j ˙=joinK
4 cdleme32s.m ˙=meetK
5 cdleme32s.a A=AtomsK
6 cdleme32s.h H=LHypK
7 cdleme32s.u U=P˙Q˙W
8 cdleme32s.d D=s˙U˙Q˙P˙s˙W
9 cdleme32s.n N=ifs˙P˙QID
10 eqid R˙U˙Q˙P˙R˙W=R˙U˙Q˙P˙R˙W
11 eqid S˙U˙Q˙P˙S˙W=S˙U˙Q˙P˙S˙W
12 2 3 4 5 6 7 10 11 cdleme35h2 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙Q¬S˙P˙QRSR˙U˙Q˙P˙R˙WS˙U˙Q˙P˙S˙W
13 simp22l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙Q¬S˙P˙QRSRA
14 simp31 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙Q¬S˙P˙QRS¬R˙P˙Q
15 8 9 10 cdleme31sn2 RA¬R˙P˙QR/sN=R˙U˙Q˙P˙R˙W
16 13 14 15 syl2anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙Q¬S˙P˙QRSR/sN=R˙U˙Q˙P˙R˙W
17 simp23l KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙Q¬S˙P˙QRSSA
18 simp32 KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙Q¬S˙P˙QRS¬S˙P˙Q
19 8 9 11 cdleme31sn2 SA¬S˙P˙QS/sN=S˙U˙Q˙P˙S˙W
20 17 18 19 syl2anc KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙Q¬S˙P˙QRSS/sN=S˙U˙Q˙P˙S˙W
21 12 16 20 3netr4d KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WSA¬S˙W¬R˙P˙Q¬S˙P˙QRSR/sNS/sN