Metamath Proof Explorer

Theorem 4atexlemnclw

Description: Lemma for 4atexlem7 . (Contributed by NM, 24-Nov-2012)

Ref Expression
Hypotheses 4thatlem.ph ⊢ φ ↔ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ S ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ W ∧ P ∨ ˙ R = Q ∨ ˙ R ∧ T ∈ A ∧ U ∨ ˙ T = V ∨ ˙ T ∧ P ≠ Q ∧ ¬ S ≤ ˙ P ∨ ˙ Q
4thatlem0.l ⊢ ≤ ˙ = ≤ K
4thatlem0.j ⊢ ∨ ˙ = join ⁡ K
4thatlem0.m ⊢ ∧ ˙ = meet ⁡ K
4thatlem0.a ⊢ A = Atoms ⁡ K
4thatlem0.h ⊢ H = LHyp ⁡ K
4thatlem0.u ⊢ U = P ∨ ˙ Q ∧ ˙ W
4thatlem0.v ⊢ V = P ∨ ˙ S ∧ ˙ W
4thatlem0.c ⊢ C = Q ∨ ˙ T ∧ ˙ P ∨ ˙ S
Assertion 4atexlemnclw ⊢ φ → ¬ C ≤ ˙ W

Proof

Step Hyp Ref Expression
1 4thatlem.ph ⊢ φ ↔ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ S ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ W ∧ P ∨ ˙ R = Q ∨ ˙ R ∧ T ∈ A ∧ U ∨ ˙ T = V ∨ ˙ T ∧ P ≠ Q ∧ ¬ S ≤ ˙ P ∨ ˙ Q
2 4thatlem0.l ⊢ ≤ ˙ = ≤ K
3 4thatlem0.j ⊢ ∨ ˙ = join ⁡ K
4 4thatlem0.m ⊢ ∧ ˙ = meet ⁡ K
5 4thatlem0.a ⊢ A = Atoms ⁡ K
6 4thatlem0.h ⊢ H = LHyp ⁡ K
7 4thatlem0.u ⊢ U = P ∨ ˙ Q ∧ ˙ W
8 4thatlem0.v ⊢ V = P ∨ ˙ S ∧ ˙ W
9 4thatlem0.c ⊢ C = Q ∨ ˙ T ∧ ˙ P ∨ ˙ S
10 1 4atexlemkl ⊢ φ → K ∈ Lat
11 1 3 5 4atexlemqtb ⊢ φ → Q ∨ ˙ T ∈ Base K
12 1 3 5 4atexlempsb ⊢ φ → P ∨ ˙ S ∈ Base K
13 eqid ⊢ Base K = Base K
14 13 2 4 latmle1 ⊢ K ∈ Lat ∧ Q ∨ ˙ T ∈ Base K ∧ P ∨ ˙ S ∈ Base K → Q ∨ ˙ T ∧ ˙ P ∨ ˙ S ≤ ˙ Q ∨ ˙ T
15 10 11 12 14 syl3anc ⊢ φ → Q ∨ ˙ T ∧ ˙ P ∨ ˙ S ≤ ˙ Q ∨ ˙ T
16 9 15 eqbrtrid ⊢ φ → C ≤ ˙ Q ∨ ˙ T
17 simp13r ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ Q ∈ A ∧ ¬ Q ≤ ˙ W ∧ S ∈ A ∧ R ∈ A ∧ ¬ R ≤ ˙ W ∧ P ∨ ˙ R = Q ∨ ˙ R ∧ T ∈ A ∧ U ∨ ˙ T = V ∨ ˙ T ∧ P ≠ Q ∧ ¬ S ≤ ˙ P ∨ ˙ Q → ¬ Q ≤ ˙ W
18 1 17 sylbi ⊢ φ → ¬ Q ≤ ˙ W
19 1 4atexlemkc ⊢ φ → K ∈ CvLat
20 1 2 3 4 5 6 7 8 4atexlemv ⊢ φ → V ∈ A
21 1 4atexlemq ⊢ φ → Q ∈ A
22 1 4atexlemt ⊢ φ → T ∈ A
23 1 2 3 4 5 6 7 4atexlemu ⊢ φ → U ∈ A
24 1 2 3 4 5 6 7 8 4atexlemunv ⊢ φ → U ≠ V
25 1 4atexlemutvt ⊢ φ → U ∨ ˙ T = V ∨ ˙ T
26 5 3 cvlsupr6 ⊢ K ∈ CvLat ∧ U ∈ A ∧ V ∈ A ∧ T ∈ A ∧ U ≠ V ∧ U ∨ ˙ T = V ∨ ˙ T → T ≠ V
27 26 necomd ⊢ K ∈ CvLat ∧ U ∈ A ∧ V ∈ A ∧ T ∈ A ∧ U ≠ V ∧ U ∨ ˙ T = V ∨ ˙ T → V ≠ T
28 19 23 20 22 24 25 27 syl132anc ⊢ φ → V ≠ T
29 2 3 5 cvlatexch2 ⊢ K ∈ CvLat ∧ V ∈ A ∧ Q ∈ A ∧ T ∈ A ∧ V ≠ T → V ≤ ˙ Q ∨ ˙ T → Q ≤ ˙ V ∨ ˙ T
30 19 20 21 22 28 29 syl131anc ⊢ φ → V ≤ ˙ Q ∨ ˙ T → Q ≤ ˙ V ∨ ˙ T
31 1 6 4atexlemwb ⊢ φ → W ∈ Base K
32 13 2 4 latmle2 ⊢ K ∈ Lat ∧ P ∨ ˙ S ∈ Base K ∧ W ∈ Base K → P ∨ ˙ S ∧ ˙ W ≤ ˙ W
33 10 12 31 32 syl3anc ⊢ φ → P ∨ ˙ S ∧ ˙ W ≤ ˙ W
34 8 33 eqbrtrid ⊢ φ → V ≤ ˙ W
35 1 2 3 4 5 6 7 8 4atexlemtlw ⊢ φ → T ≤ ˙ W
36 13 5 atbase ⊢ V ∈ A → V ∈ Base K
37 20 36 syl ⊢ φ → V ∈ Base K
38 13 5 atbase ⊢ T ∈ A → T ∈ Base K
39 22 38 syl ⊢ φ → T ∈ Base K
40 13 2 3 latjle12 ⊢ K ∈ Lat ∧ V ∈ Base K ∧ T ∈ Base K ∧ W ∈ Base K → V ≤ ˙ W ∧ T ≤ ˙ W ↔ V ∨ ˙ T ≤ ˙ W
41 10 37 39 31 40 syl13anc ⊢ φ → V ≤ ˙ W ∧ T ≤ ˙ W ↔ V ∨ ˙ T ≤ ˙ W
42 34 35 41 mpbi2and ⊢ φ → V ∨ ˙ T ≤ ˙ W
43 13 5 atbase ⊢ Q ∈ A → Q ∈ Base K
44 21 43 syl ⊢ φ → Q ∈ Base K
45 1 4atexlemk ⊢ φ → K ∈ HL
46 13 3 5 hlatjcl ⊢ K ∈ HL ∧ V ∈ A ∧ T ∈ A → V ∨ ˙ T ∈ Base K
47 45 20 22 46 syl3anc ⊢ φ → V ∨ ˙ T ∈ Base K
48 13 2 lattr ⊢ K ∈ Lat ∧ Q ∈ Base K ∧ V ∨ ˙ T ∈ Base K ∧ W ∈ Base K → Q ≤ ˙ V ∨ ˙ T ∧ V ∨ ˙ T ≤ ˙ W → Q ≤ ˙ W
49 10 44 47 31 48 syl13anc ⊢ φ → Q ≤ ˙ V ∨ ˙ T ∧ V ∨ ˙ T ≤ ˙ W → Q ≤ ˙ W
50 42 49 mpan2d ⊢ φ → Q ≤ ˙ V ∨ ˙ T → Q ≤ ˙ W
51 30 50 syld ⊢ φ → V ≤ ˙ Q ∨ ˙ T → Q ≤ ˙ W
52 18 51 mtod ⊢ φ → ¬ V ≤ ˙ Q ∨ ˙ T
53 nbrne2 ⊢ C ≤ ˙ Q ∨ ˙ T ∧ ¬ V ≤ ˙ Q ∨ ˙ T → C ≠ V
54 16 52 53 syl2anc ⊢ φ → C ≠ V
55 1 4atexlemw ⊢ φ → W ∈ H
56 45 55 jca ⊢ φ → K ∈ HL ∧ W ∈ H
57 1 4atexlempw ⊢ φ → P ∈ A ∧ ¬ P ≤ ˙ W
58 1 4atexlems ⊢ φ → S ∈ A
59 1 2 3 4 5 6 7 8 9 4atexlemc ⊢ φ → C ∈ A
60 1 2 3 5 4atexlempns ⊢ φ → P ≠ S
61 13 2 4 latmle2 ⊢ K ∈ Lat ∧ Q ∨ ˙ T ∈ Base K ∧ P ∨ ˙ S ∈ Base K → Q ∨ ˙ T ∧ ˙ P ∨ ˙ S ≤ ˙ P ∨ ˙ S
62 10 11 12 61 syl3anc ⊢ φ → Q ∨ ˙ T ∧ ˙ P ∨ ˙ S ≤ ˙ P ∨ ˙ S
63 9 62 eqbrtrid ⊢ φ → C ≤ ˙ P ∨ ˙ S
64 2 3 4 5 6 8 lhpat3 ⊢ K ∈ HL ∧ W ∈ H ∧ P ∈ A ∧ ¬ P ≤ ˙ W ∧ S ∈ A ∧ C ∈ A ∧ P ≠ S ∧ C ≤ ˙ P ∨ ˙ S → ¬ C ≤ ˙ W ↔ C ≠ V
65 56 57 58 59 60 63 64 syl222anc ⊢ φ → ¬ C ≤ ˙ W ↔ C ≠ V
66 54 65 mpbird ⊢ φ → ¬ C ≤ ˙ W