Metamath Proof Explorer


Theorem cdleme32fvaw

Description: Show that ( FR ) is an atom not under W when R is an atom not under W . (Contributed by NM, 18-Apr-2013)

Ref Expression
Hypotheses cdleme32.b B = Base K
cdleme32.l ˙ = K
cdleme32.j ˙ = join K
cdleme32.m ˙ = meet K
cdleme32.a A = Atoms K
cdleme32.h H = LHyp K
cdleme32.u U = P ˙ Q ˙ W
cdleme32.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
cdleme32.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
cdleme32.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
cdleme32.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
cdleme32.n N = if s ˙ P ˙ Q I C
cdleme32.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
cdleme32.f F = x B if P Q ¬ x ˙ W O x
Assertion cdleme32fvaw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W F R A ¬ F R ˙ W

Proof

Step Hyp Ref Expression
1 cdleme32.b B = Base K
2 cdleme32.l ˙ = K
3 cdleme32.j ˙ = join K
4 cdleme32.m ˙ = meet K
5 cdleme32.a A = Atoms K
6 cdleme32.h H = LHyp K
7 cdleme32.u U = P ˙ Q ˙ W
8 cdleme32.c C = s ˙ U ˙ Q ˙ P ˙ s ˙ W
9 cdleme32.d D = t ˙ U ˙ Q ˙ P ˙ t ˙ W
10 cdleme32.e E = P ˙ Q ˙ D ˙ s ˙ t ˙ W
11 cdleme32.i I = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = E
12 cdleme32.n N = if s ˙ P ˙ Q I C
13 cdleme32.o O = ι z B | s A ¬ s ˙ W s ˙ x ˙ W = x z = N ˙ x ˙ W
14 cdleme32.f F = x B if P Q ¬ x ˙ W O x
15 simplr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P = Q R A ¬ R ˙ W
16 1 5 atbase R A R B
17 16 ad2antrl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W R B
18 14 cdleme31id R B P = Q F R = R
19 17 18 sylan K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P = Q F R = R
20 19 eleq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P = Q F R A R A
21 19 breq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P = Q F R ˙ W R ˙ W
22 21 notbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P = Q ¬ F R ˙ W ¬ R ˙ W
23 20 22 anbi12d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P = Q F R A ¬ F R ˙ W R A ¬ R ˙ W
24 15 23 mpbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P = Q F R A ¬ F R ˙ W
25 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
26 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q P Q
27 simp2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R A ¬ R ˙ W
28 1 2 3 4 5 6 7 8 9 10 11 12 cdleme32snaw K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R / s N A ¬ R / s N ˙ W
29 25 26 27 28 syl12anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R / s N A ¬ R / s N ˙ W
30 1 2 3 4 5 6 7 8 9 10 11 12 13 14 cdleme32fva1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q F R = R / s N
31 30 eleq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q F R A R / s N A
32 30 breq1d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q F R ˙ W R / s N ˙ W
33 32 notbid K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q ¬ F R ˙ W ¬ R / s N ˙ W
34 31 33 anbi12d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q F R A ¬ F R ˙ W R / s N A ¬ R / s N ˙ W
35 29 34 mpbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q F R A ¬ F R ˙ W
36 35 3expa K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q F R A ¬ F R ˙ W
37 24 36 pm2.61dane K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W F R A ¬ F R ˙ W