Metamath Proof Explorer


Theorem cdlemefs32fvaN

Description: Part of proof of Lemma E in Crawley p. 113. Value of F at an atom not under W . TODO: FIX COMMENT. TODO: consolidate uses of lhpmat here and elsewhere, and presence/absence of s .<_ ( P .\/ Q ) term. Also, why can proof be shortened with cdleme27cl ? What is difference from cdlemefs27cl ? (Contributed by NM, 29-Mar-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemefs32.b B=BaseK
cdlemefs32.l ˙=K
cdlemefs32.j ˙=joinK
cdlemefs32.m ˙=meetK
cdlemefs32.a A=AtomsK
cdlemefs32.h H=LHypK
cdlemefs32.u U=P˙Q˙W
cdlemefs32.d D=t˙U˙Q˙P˙t˙W
cdlemefs32.e E=P˙Q˙D˙s˙t˙W
cdlemefs32.i I=ιyB|tA¬t˙W¬t˙P˙Qy=E
cdlemefs32.n N=ifs˙P˙QIC
cdleme29fs.o O=ιzB|sA¬s˙Ws˙x˙W=xz=N˙x˙W
Assertion cdlemefs32fvaN KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QR/xO=R/sN

Proof

Step Hyp Ref Expression
1 cdlemefs32.b B=BaseK
2 cdlemefs32.l ˙=K
3 cdlemefs32.j ˙=joinK
4 cdlemefs32.m ˙=meetK
5 cdlemefs32.a A=AtomsK
6 cdlemefs32.h H=LHypK
7 cdlemefs32.u U=P˙Q˙W
8 cdlemefs32.d D=t˙U˙Q˙P˙t˙W
9 cdlemefs32.e E=P˙Q˙D˙s˙t˙W
10 cdlemefs32.i I=ιyB|tA¬t˙W¬t˙P˙Qy=E
11 cdlemefs32.n N=ifs˙P˙QIC
12 cdleme29fs.o O=ιzB|sA¬s˙Ws˙x˙W=xz=N˙x˙W
13 breq1 s=Rs˙P˙QR˙P˙Q
14 simp1 KHLWHPA¬P˙WQA¬Q˙WPQsA¬s˙Ws˙P˙QKHLWHPA¬P˙WQA¬Q˙W
15 simp3l KHLWHPA¬P˙WQA¬Q˙WPQsA¬s˙Ws˙P˙QsA
16 simp3rl KHLWHPA¬P˙WQA¬Q˙WPQsA¬s˙Ws˙P˙Q¬s˙W
17 15 16 jca KHLWHPA¬P˙WQA¬Q˙WPQsA¬s˙Ws˙P˙QsA¬s˙W
18 simp3rr KHLWHPA¬P˙WQA¬Q˙WPQsA¬s˙Ws˙P˙Qs˙P˙Q
19 simp2 KHLWHPA¬P˙WQA¬Q˙WPQsA¬s˙Ws˙P˙QPQ
20 1 2 3 4 5 6 7 8 9 10 11 cdlemefs27cl KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQNB
21 14 17 18 19 20 syl13anc KHLWHPA¬P˙WQA¬Q˙WPQsA¬s˙Ws˙P˙QNB
22 1 2 3 4 5 6 7 8 9 10 11 cdlemefs32snb KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QR/sNB
23 1 2 3 4 5 6 13 21 22 12 cdlemefrs32fva KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QR/xO=R/sN