Metamath Proof Explorer


Theorem cdlemefs27cl

Description: Part of proof of Lemma E in Crawley p. 113. Closure of N . TODO FIX COMMENT This is the start of a re-proof of cdleme27cl etc. with the s .<_ ( P .\/ Q ) condition (so as to not have the C hypothesis). (Contributed by NM, 24-Mar-2013)

Ref Expression
Hypotheses cdlemefs26.b B=BaseK
cdlemefs26.l ˙=K
cdlemefs26.j ˙=joinK
cdlemefs26.m ˙=meetK
cdlemefs26.a A=AtomsK
cdlemefs26.h H=LHypK
cdlemefs27.u U=P˙Q˙W
cdlemefs27.d D=t˙U˙Q˙P˙t˙W
cdlemefs27.e E=P˙Q˙D˙s˙t˙W
cdlemefs27.i I=ιuB|tA¬t˙W¬t˙P˙Qu=E
cdlemefs27.n N=ifs˙P˙QIC
Assertion cdlemefs27cl KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQNB

Proof

Step Hyp Ref Expression
1 cdlemefs26.b B=BaseK
2 cdlemefs26.l ˙=K
3 cdlemefs26.j ˙=joinK
4 cdlemefs26.m ˙=meetK
5 cdlemefs26.a A=AtomsK
6 cdlemefs26.h H=LHypK
7 cdlemefs27.u U=P˙Q˙W
8 cdlemefs27.d D=t˙U˙Q˙P˙t˙W
9 cdlemefs27.e E=P˙Q˙D˙s˙t˙W
10 cdlemefs27.i I=ιuB|tA¬t˙W¬t˙P˙Qu=E
11 cdlemefs27.n N=ifs˙P˙QIC
12 simpr2 KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQs˙P˙Q
13 12 iftrued KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQifs˙P˙QIC=I
14 simpl1 KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQKHLWH
15 simpl2 KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQPA¬P˙W
16 simpl3 KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQQA¬Q˙W
17 simpr1 KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQsA¬s˙W
18 simpr3 KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQPQ
19 1 2 3 4 5 6 7 8 9 10 cdleme25cl KHLWHPA¬P˙WQA¬Q˙WsA¬s˙WPQs˙P˙QIB
20 14 15 16 17 18 12 19 syl312anc KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQIB
21 13 20 eqeltrd KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQifs˙P˙QICB
22 11 21 eqeltrid KHLWHPA¬P˙WQA¬Q˙WsA¬s˙Ws˙P˙QPQNB