Metamath Proof Explorer


Theorem cdlemefs29cpre1N

Description: TODO: FIX COMMENT. (Contributed by NM, 26-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
Assertion cdlemefs29cpre1N K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q ∃! z B s A ¬ s ˙ W s ˙ P ˙ Q s ˙ R ˙ W = R z = N ˙ R ˙ W

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 breq1 s = R s ˙ P ˙ Q R ˙ P ˙ Q
13 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
14 simp3l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W s ˙ P ˙ Q s A
15 simp3rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q s A ¬ s ˙ W s ˙ P ˙ Q ¬ s ˙ W
16 14 15 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
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 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
20 13 16 17 18 19 syl13anc 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 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
22 1 2 3 4 5 6 12 20 21 cdlemefrs29cpre1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q ∃! z B s A ¬ s ˙ W s ˙ P ˙ Q s ˙ R ˙ W = R z = N ˙ R ˙ W