Metamath Proof Explorer


Theorem cdleme0ex2N

Description: Part of proof of Lemma E in Crawley p. 113. Note that ( P .\/ u ) = ( Q .\/ u ) is a shorter way to express u =/= P /\ u =/= Q /\ u .<_ ( P .\/ Q ) . (Contributed by NM, 9-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses cdleme0.l ˙ = K
cdleme0.j ˙ = join K
cdleme0.m ˙ = meet K
cdleme0.a A = Atoms K
cdleme0.h H = LHyp K
cdleme0.u U = P ˙ Q ˙ W
Assertion cdleme0ex2N K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A P ˙ u = Q ˙ u u ˙ W

Proof

Step Hyp Ref Expression
1 cdleme0.l ˙ = K
2 cdleme0.j ˙ = join K
3 cdleme0.m ˙ = meet K
4 cdleme0.a A = Atoms K
5 cdleme0.h H = LHyp K
6 cdleme0.u U = P ˙ Q ˙ W
7 simp1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q K HL W H
8 simp2l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P A ¬ P ˙ W
9 simp2rl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q Q A
10 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P Q
11 1 2 3 4 5 6 cdleme0ex1N K HL W H P A ¬ P ˙ W Q A P Q u A u ˙ P ˙ Q u ˙ W
12 7 8 9 10 11 syl121anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ P ˙ Q u ˙ W
13 simp11l K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W K HL
14 hlcvl K HL K CvLat
15 13 14 syl K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W K CvLat
16 simp2ll K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q P A
17 16 3ad2ant1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W P A
18 9 3ad2ant1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W Q A
19 simp2 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W u A
20 simp13 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W P Q
21 4 1 2 cvlsupr2 K CvLat P A Q A u A P Q P ˙ u = Q ˙ u u P u Q u ˙ P ˙ Q
22 15 17 18 19 20 21 syl131anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W P ˙ u = Q ˙ u u P u Q u ˙ P ˙ Q
23 df-3an u P u Q u ˙ P ˙ Q u P u Q u ˙ P ˙ Q
24 simp3 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W u ˙ W
25 simp2lr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ P ˙ W
26 25 3ad2ant1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W ¬ P ˙ W
27 nbrne2 u ˙ W ¬ P ˙ W u P
28 24 26 27 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W u P
29 simp2rr K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q ¬ Q ˙ W
30 29 3ad2ant1 K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W ¬ Q ˙ W
31 nbrne2 u ˙ W ¬ Q ˙ W u Q
32 24 30 31 syl2anc K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W u Q
33 28 32 jca K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W u P u Q
34 33 biantrurd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W u ˙ P ˙ Q u P u Q u ˙ P ˙ Q
35 23 34 bitr4id K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W u P u Q u ˙ P ˙ Q u ˙ P ˙ Q
36 22 35 bitrd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W P ˙ u = Q ˙ u u ˙ P ˙ Q
37 36 3expia K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A u ˙ W P ˙ u = Q ˙ u u ˙ P ˙ Q
38 37 pm5.32rd K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A P ˙ u = Q ˙ u u ˙ W u ˙ P ˙ Q u ˙ W
39 38 rexbidva K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A P ˙ u = Q ˙ u u ˙ W u A u ˙ P ˙ Q u ˙ W
40 12 39 mpbird K HL W H P A ¬ P ˙ W Q A ¬ Q ˙ W P Q u A P ˙ u = Q ˙ u u ˙ W