Metamath Proof Explorer


Theorem cdlemeg46fvcl

Description: TODO: fix comment. (Contributed by NM, 9-Apr-2013)

Ref Expression
Hypotheses cdlemef47.b B = Base K
cdlemef47.l ˙ = K
cdlemef47.j ˙ = join K
cdlemef47.m ˙ = meet K
cdlemef47.a A = Atoms K
cdlemef47.h H = LHyp K
cdlemef47.v V = Q ˙ P ˙ W
cdlemef47.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
cdlemefs47.o O = Q ˙ P ˙ N ˙ u ˙ v ˙ W
cdlemef47.g G = a B if Q P ¬ a ˙ W ι c B | u A ¬ u ˙ W u ˙ a ˙ W = a c = if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N ˙ a ˙ W a
Assertion cdlemeg46fvcl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B G X B

Proof

Step Hyp Ref Expression
1 cdlemef47.b B = Base K
2 cdlemef47.l ˙ = K
3 cdlemef47.j ˙ = join K
4 cdlemef47.m ˙ = meet K
5 cdlemef47.a A = Atoms K
6 cdlemef47.h H = LHyp K
7 cdlemef47.v V = Q ˙ P ˙ W
8 cdlemef47.n N = v ˙ V ˙ P ˙ Q ˙ v ˙ W
9 cdlemefs47.o O = Q ˙ P ˙ N ˙ u ˙ v ˙ W
10 cdlemef47.g G = a B if Q P ¬ a ˙ W ι c B | u A ¬ u ˙ W u ˙ a ˙ W = a c = if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N ˙ a ˙ W a
11 simpl1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B K HL W H
12 simpl3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B Q A ¬ Q ˙ W
13 simpl2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B P A ¬ P ˙ W
14 simpr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B X B
15 vex u V
16 eqid u ˙ V ˙ P ˙ Q ˙ u ˙ W = u ˙ V ˙ P ˙ Q ˙ u ˙ W
17 8 16 cdleme31sc u V u / v N = u ˙ V ˙ P ˙ Q ˙ u ˙ W
18 15 17 ax-mp u / v N = u ˙ V ˙ P ˙ Q ˙ u ˙ W
19 eqid ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O = ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O
20 eqid if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N = if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N
21 eqid ι c B | u A ¬ u ˙ W u ˙ a ˙ W = a c = if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N ˙ a ˙ W = ι c B | u A ¬ u ˙ W u ˙ a ˙ W = a c = if u ˙ Q ˙ P ι b B | v A ¬ v ˙ W ¬ v ˙ Q ˙ P b = O u / v N ˙ a ˙ W
22 1 2 3 4 5 6 7 18 8 9 19 20 21 10 cdleme32fvcl K HL W H Q A ¬ Q ˙ W P A ¬ P ˙ W X B G X B
23 11 12 13 14 22 syl31anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W X B G X B