Metamath Proof Explorer


Theorem cdlemk38

Description: Part of proof of Lemma K of Crawley p. 118. Line 31, p. 119. TODO: derive more directly with r19.23 ? (Contributed by NM, 19-Jul-2013)

Ref Expression
Hypotheses cdlemk4.b B=BaseK
cdlemk4.l ˙=K
cdlemk4.j ˙=joinK
cdlemk4.m ˙=meetK
cdlemk4.a A=AtomsK
cdlemk4.h H=LHypK
cdlemk4.t T=LTrnKW
cdlemk4.r R=trLKW
cdlemk4.z Z=P˙Rb˙NP˙RbF-1
cdlemk4.y Y=P˙RG˙Z˙RGb-1
cdlemk4.x X=ιzT|bTbIBRbRFRbRGzP=Y
Assertion cdlemk38 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNXP˙P˙RG

Proof

Step Hyp Ref Expression
1 cdlemk4.b B=BaseK
2 cdlemk4.l ˙=K
3 cdlemk4.j ˙=joinK
4 cdlemk4.m ˙=meetK
5 cdlemk4.a A=AtomsK
6 cdlemk4.h H=LHypK
7 cdlemk4.t T=LTrnKW
8 cdlemk4.r R=trLKW
9 cdlemk4.z Z=P˙Rb˙NP˙RbF-1
10 cdlemk4.y Y=P˙RG˙Z˙RGb-1
11 cdlemk4.x X=ιzT|bTbIBRbRFRbRGzP=Y
12 1 6 7 8 cdlemftr2 KHLWHbTbIBRbRFRbRG
13 12 3ad2ant1 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRG
14 nfv bKHLWHFTFIBGTGIBNTPA¬P˙WRF=RN
15 nfra1 bbTbIBRbRFRbRGzP=Y
16 nfcv _bT
17 15 16 nfriota _bιzT|bTbIBRbRFRbRGzP=Y
18 11 17 nfcxfr _bX
19 nfcv _bP
20 18 19 nffv _bXP
21 nfcv _b˙
22 nfcv _bP˙RG
23 20 21 22 nfbr bXP˙P˙RG
24 simpl1 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGKHLWH
25 simpl21 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGFTFIB
26 simpl22 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGGTGIB
27 simpl23 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGNT
28 simpl3l KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGPA¬P˙W
29 simpl3r KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGRF=RN
30 simpr KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGbTbIBRbRFRbRG
31 1 2 3 4 5 6 7 8 9 10 11 cdlemk37 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGXP˙P˙RG
32 24 25 26 27 28 29 30 31 syl331anc KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGXP˙P˙RG
33 32 exp32 KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGXP˙P˙RG
34 14 23 33 rexlimd KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNbTbIBRbRFRbRGXP˙P˙RG
35 13 34 mpd KHLWHFTFIBGTGIBNTPA¬P˙WRF=RNXP˙P˙RG