Metamath Proof Explorer


Theorem cdlemefs29clN

Description: Show closure of the unique element in cdleme29c . (Contributed by NM, 27-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
cdlemefs29cl.o O=ιzB|sA¬s˙Ws˙R˙W=Rz=N˙R˙W
Assertion cdlemefs29clN KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QOB

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 cdlemefs29cl.o O=ιzB|sA¬s˙Ws˙R˙W=Rz=N˙R˙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 cdlemefrs29clN KHLWHPA¬P˙WQA¬Q˙WPQRA¬R˙WR˙P˙QOB