Metamath Proof Explorer


Theorem cdleme41sn3a

Description: Show that [_ R / s ]_ N is under P .\/ Q when R .<_ ( P .\/ Q ) . (Contributed by NM, 19-Mar-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
cdleme32a1.y Y = P ˙ Q ˙ D ˙ R ˙ t ˙ W
cdleme32a1.z Z = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = Y
Assertion cdleme41sn3a K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q R / s N ˙ P ˙ Q

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 cdleme32a1.y Y = P ˙ Q ˙ D ˙ R ˙ t ˙ W
14 cdleme32a1.z Z = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = Y
15 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q R A
16 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q R ˙ P ˙ Q
17 10 11 12 13 14 cdleme31sn1c R A R ˙ P ˙ Q R / s N = Z
18 15 16 17 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q R / s N = Z
19 1 fvexi B V
20 nfv t K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q
21 nfra1 t t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = Y
22 nfcv _ t B
23 21 22 nfriota _ t ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = Y
24 14 23 nfcxfr _ t Z
25 nfcv _ t ˙
26 nfcv _ t P ˙ Q
27 24 25 26 nfbr t Z ˙ P ˙ Q
28 27 a1i K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q t Z ˙ P ˙ Q
29 14 a1i K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q Z = ι y B | t A ¬ t ˙ W ¬ t ˙ P ˙ Q y = Y
30 breq1 Y = Z Y ˙ P ˙ Q Z ˙ P ˙ Q
31 30 adantl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q Y = Z Y ˙ P ˙ Q Z ˙ P ˙ Q
32 simpl11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q t A ¬ t ˙ W ¬ t ˙ P ˙ Q K HL W H
33 simp12l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q P A
34 33 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q t A ¬ t ˙ W ¬ t ˙ P ˙ Q P A
35 simp13l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q Q A
36 35 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q t A ¬ t ˙ W ¬ t ˙ P ˙ Q Q A
37 15 adantr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q t A ¬ t ˙ W ¬ t ˙ P ˙ Q R A
38 simprl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q t A ¬ t ˙ W ¬ t ˙ P ˙ Q t A
39 2 3 4 5 6 7 9 13 cdleme4a K HL W H P A Q A R A t A Y ˙ P ˙ Q
40 32 34 36 37 38 39 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q t A ¬ t ˙ W ¬ t ˙ P ˙ Q Y ˙ P ˙ Q
41 40 ex K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q t A ¬ t ˙ W ¬ t ˙ P ˙ Q Y ˙ P ˙ Q
42 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W
43 simp2rr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q ¬ R ˙ W
44 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q P Q
45 1 2 3 4 5 6 7 9 13 14 cdleme25cl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W R A ¬ R ˙ W P Q R ˙ P ˙ Q Z B
46 42 15 43 44 16 45 syl122anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q Z B
47 simp11 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q K HL W H
48 simp12 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q P A ¬ P ˙ W
49 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q Q A ¬ Q ˙ W
50 2 3 5 6 cdlemb2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q t A ¬ t ˙ W ¬ t ˙ P ˙ Q
51 47 48 49 44 50 syl121anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q t A ¬ t ˙ W ¬ t ˙ P ˙ Q
52 20 28 29 31 41 46 51 riotasv3d K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q B V Z ˙ P ˙ Q
53 19 52 mpan2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q Z ˙ P ˙ Q
54 18 53 eqbrtrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q R A ¬ R ˙ W R ˙ P ˙ Q R / s N ˙ P ˙ Q