Metamath Proof Explorer


Theorem cdleme32a

Description: Part of proof of Lemma D in Crawley p. 113. (Contributed by NM, 19-Feb-2013)

Ref Expression
Hypotheses cdleme32.b B=BaseK
cdleme32.l ˙=K
cdleme32.j ˙=joinK
cdleme32.m ˙=meetK
cdleme32.a A=AtomsK
cdleme32.h H=LHypK
cdleme32.u U=P˙Q˙W
cdleme32.c C=s˙U˙Q˙P˙s˙W
cdleme32.d D=t˙U˙Q˙P˙t˙W
cdleme32.e E=P˙Q˙D˙s˙t˙W
cdleme32.i I=ιyB|tA¬t˙W¬t˙P˙Qy=E
cdleme32.n N=ifs˙P˙QIC
cdleme32.o O=ιzB|sA¬s˙Ws˙x˙W=xz=N˙x˙W
cdleme32.f F=xBifPQ¬x˙WOx
Assertion cdleme32a KHLWHPA¬P˙WQA¬Q˙WXBPQ¬X˙WsA¬s˙Ws˙X˙W=XFX=N˙X˙W

Proof

Step Hyp Ref Expression
1 cdleme32.b B=BaseK
2 cdleme32.l ˙=K
3 cdleme32.j ˙=joinK
4 cdleme32.m ˙=meetK
5 cdleme32.a A=AtomsK
6 cdleme32.h H=LHypK
7 cdleme32.u U=P˙Q˙W
8 cdleme32.c C=s˙U˙Q˙P˙s˙W
9 cdleme32.d D=t˙U˙Q˙P˙t˙W
10 cdleme32.e E=P˙Q˙D˙s˙t˙W
11 cdleme32.i I=ιyB|tA¬t˙W¬t˙P˙Qy=E
12 cdleme32.n N=ifs˙P˙QIC
13 cdleme32.o O=ιzB|sA¬s˙Ws˙x˙W=xz=N˙x˙W
14 cdleme32.f F=xBifPQ¬x˙WOx
15 1 fvexi BV
16 anass sA¬s˙Ws˙X˙W=XsA¬s˙Ws˙X˙W=X
17 eqid ιzB|sA¬s˙Ws˙X˙W=Xz=N˙X˙W=ιzB|sA¬s˙Ws˙X˙W=Xz=N˙X˙W
18 13 14 17 cdleme31fv1 XBPQ¬X˙WFX=ιzB|sA¬s˙Ws˙X˙W=Xz=N˙X˙W
19 18 adantl KHLWHPA¬P˙WQA¬Q˙WXBPQ¬X˙WFX=ιzB|sA¬s˙Ws˙X˙W=Xz=N˙X˙W
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme32fvcl KHLWHPA¬P˙WQA¬Q˙WXBFXB
21 20 adantrr KHLWHPA¬P˙WQA¬Q˙WXBPQ¬X˙WFXB
22 19 21 riotasvd KHLWHPA¬P˙WQA¬Q˙WXBPQ¬X˙WBVsA¬s˙Ws˙X˙W=XFX=N˙X˙W
23 16 22 syl5bi KHLWHPA¬P˙WQA¬Q˙WXBPQ¬X˙WBVsA¬s˙Ws˙X˙W=XFX=N˙X˙W
24 15 23 mpan2 KHLWHPA¬P˙WQA¬Q˙WXBPQ¬X˙WsA¬s˙Ws˙X˙W=XFX=N˙X˙W
25 24 3impia KHLWHPA¬P˙WQA¬Q˙WXBPQ¬X˙WsA¬s˙Ws˙X˙W=XFX=N˙X˙W