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 = Base K
cdlemefs32.l ˙ = K
cdlemefs32.j ˙ = join K
cdlemefs32.m ˙ = meet K
cdlemefs32.a A = Atoms K
cdlemefs32.h H = LHyp K
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 = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
cdlemefs32.n N = if s ˙ P ˙ Q I C
cdlemefs29cl.o O = ι z B | s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
Assertion cdlemefs29clN 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 cdlemefs32.b B = Base K
2 cdlemefs32.l ˙ = K
3 cdlemefs32.j ˙ = join K
4 cdlemefs32.m ˙ = meet K
5 cdlemefs32.a A = Atoms K
6 cdlemefs32.h H = LHyp K
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 = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
11 cdlemefs32.n N = if s ˙ P ˙ Q I C
12 cdlemefs29cl.o O = ι z B | s A ¬ s ˙ W s ˙ R ˙ W = R z = N ˙ R ˙ W
13 breq1 s = R s ˙ P ˙ Q R ˙ P ˙ Q
14 simp1 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 P A ¬ P ˙ W Q A ¬ Q ˙ W
15 simp3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W s ˙ P ˙ Q s A
16 simp3rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W s ˙ P ˙ Q ¬ s ˙ W
17 15 16 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W s ˙ P ˙ Q s A ¬ s ˙ W
18 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
19 simp2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W s ˙ P ˙ Q P Q
20 1 2 3 4 5 6 7 8 9 10 11 cdlemefs27cl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W s A ¬ s ˙ W s ˙ P ˙ Q P Q N B
21 14 17 18 19 20 syl13anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W s ˙ P ˙ Q N B
22 1 2 3 4 5 6 7 8 9 10 11 cdlemefs32snb 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
23 1 2 3 4 5 6 13 21 22 12 cdlemefrs29clN K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q O B