Metamath Proof Explorer


Theorem cdlemefr29clN

Description: Show closure of the unique element in cdleme29c . TODO fix comment. TODO Not needed? (Contributed by NM, 29-Mar-2013) (New usage is discouraged.)

Ref Expression
Hypotheses cdlemefr27.b B = Base K
cdlemefr27.l ˙ = K
cdlemefr27.j ˙ = join K
cdlemefr27.m ˙ = meet K
cdlemefr27.a A = Atoms K
cdlemefr27.h H = LHyp K
cdlemefr27.u U = P ˙ Q ˙ W
cdlemefr27.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdlemefr27.n N = if s ˙ P ˙ Q I C
cdlemefr29cl.o O = ι z B | s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
Assertion cdlemefr29clN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q O B

Proof

Step Hyp Ref Expression
1 cdlemefr27.b B = Base K
2 cdlemefr27.l ˙ = K
3 cdlemefr27.j ˙ = join K
4 cdlemefr27.m ˙ = meet K
5 cdlemefr27.a A = Atoms K
6 cdlemefr27.h H = LHyp K
7 cdlemefr27.u U = P ˙ Q ˙ W
8 cdlemefr27.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdlemefr27.n N = if s ˙ P ˙ Q I C
10 cdlemefr29cl.o O = ι z B | s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
11 breq1 s = R s ˙ P ˙ Q R ˙ P ˙ Q
12 11 notbid s = R ¬ s ˙ P ˙ Q ¬ R ˙ P ˙ Q
13 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q K HL W H
14 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q P A
15 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q Q A
16 simp3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q s A
17 simp3rr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q ¬ s ˙ P ˙ Q
18 simp2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q P Q
19 1 2 3 4 5 6 7 8 9 cdlemefr27cl K HL W H P A Q A s A ¬ s ˙ P ˙ Q P Q N B
20 13 14 15 16 17 18 19 syl33anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W ¬ s ˙ P ˙ Q N B
21 1 2 3 4 5 6 7 8 9 cdlemefr32snb K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q R / s N B
22 1 2 3 4 5 6 12 20 21 10 cdlemefrs29clN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W ¬ R ˙ P ˙ Q O B