Metamath Proof Explorer

Theorem 4atexlemc

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 4atexlemc ⊢ φ → C ∈ A

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 4 latmcom ⊢ K ∈ Lat ∧ Q ∨ ˙ T ∈ Base K ∧ P ∨ ˙ S ∈ Base K → Q ∨ ˙ T ∧ ˙ P ∨ ˙ S = P ∨ ˙ S ∧ ˙ Q ∨ ˙ T
15 10 11 12 14 syl3anc ⊢ φ → Q ∨ ˙ T ∧ ˙ P ∨ ˙ S = P ∨ ˙ S ∧ ˙ Q ∨ ˙ T
16 9 15 syl5eq ⊢ φ → C = P ∨ ˙ S ∧ ˙ Q ∨ ˙ T
17 1 4atexlemk ⊢ φ → K ∈ HL
18 1 4atexlemp ⊢ φ → P ∈ A
19 1 4atexlems ⊢ φ → S ∈ A
20 1 4atexlemq ⊢ φ → Q ∈ A
21 1 4atexlemt ⊢ φ → T ∈ A
22 1 2 3 5 4atexlempns ⊢ φ → P ≠ S
23 1 2 3 4 5 6 7 8 4atexlemntlpq ⊢ φ → ¬ T ≤ ˙ P ∨ ˙ Q
24 2 3 5 atnlej2 ⊢ K ∈ HL ∧ T ∈ A ∧ P ∈ A ∧ Q ∈ A ∧ ¬ T ≤ ˙ P ∨ ˙ Q → T ≠ Q
25 24 necomd ⊢ K ∈ HL ∧ T ∈ A ∧ P ∈ A ∧ Q ∈ A ∧ ¬ T ≤ ˙ P ∨ ˙ Q → Q ≠ T
26 17 21 18 20 23 25 syl131anc ⊢ φ → Q ≠ T
27 1 4atexlempnq ⊢ φ → P ≠ Q
28 1 4atexlemnslpq ⊢ φ → ¬ S ≤ ˙ P ∨ ˙ Q
29 2 3 5 4atlem0ae ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A ∧ P ≠ Q ∧ ¬ S ≤ ˙ P ∨ ˙ Q → ¬ Q ≤ ˙ P ∨ ˙ S
30 17 18 20 19 27 28 29 syl132anc ⊢ φ → ¬ Q ≤ ˙ P ∨ ˙ S
31 13 5 atbase ⊢ T ∈ A → T ∈ Base K
32 21 31 syl ⊢ φ → T ∈ Base K
33 1 2 3 4 5 6 7 4atexlemu ⊢ φ → U ∈ A
34 1 2 3 4 5 6 7 8 4atexlemv ⊢ φ → V ∈ A
35 13 3 5 hlatjcl ⊢ K ∈ HL ∧ U ∈ A ∧ V ∈ A → U ∨ ˙ V ∈ Base K
36 17 33 34 35 syl3anc ⊢ φ → U ∨ ˙ V ∈ Base K
37 13 5 atbase ⊢ Q ∈ A → Q ∈ Base K
38 20 37 syl ⊢ φ → Q ∈ Base K
39 13 3 latjcl ⊢ K ∈ Lat ∧ P ∨ ˙ S ∈ Base K ∧ Q ∈ Base K → P ∨ ˙ S ∨ ˙ Q ∈ Base K
40 10 12 38 39 syl3anc ⊢ φ → P ∨ ˙ S ∨ ˙ Q ∈ Base K
41 1 4atexlemkc ⊢ φ → K ∈ CvLat
42 1 2 3 4 5 6 7 8 4atexlemunv ⊢ φ → U ≠ V
43 1 4atexlemutvt ⊢ φ → U ∨ ˙ T = V ∨ ˙ T
44 5 2 3 cvlsupr4 ⊢ K ∈ CvLat ∧ U ∈ A ∧ V ∈ A ∧ T ∈ A ∧ U ≠ V ∧ U ∨ ˙ T = V ∨ ˙ T → T ≤ ˙ U ∨ ˙ V
45 41 33 34 21 42 43 44 syl132anc ⊢ φ → T ≤ ˙ U ∨ ˙ V
46 13 3 5 hlatjcl ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A → P ∨ ˙ Q ∈ Base K
47 17 18 20 46 syl3anc ⊢ φ → P ∨ ˙ Q ∈ Base K
48 1 6 4atexlemwb ⊢ φ → W ∈ Base K
49 13 2 4 latmle1 ⊢ K ∈ Lat ∧ P ∨ ˙ Q ∈ Base K ∧ W ∈ Base K → P ∨ ˙ Q ∧ ˙ W ≤ ˙ P ∨ ˙ Q
50 10 47 48 49 syl3anc ⊢ φ → P ∨ ˙ Q ∧ ˙ W ≤ ˙ P ∨ ˙ Q
51 7 50 eqbrtrid ⊢ φ → U ≤ ˙ P ∨ ˙ Q
52 13 2 4 latmle1 ⊢ K ∈ Lat ∧ P ∨ ˙ S ∈ Base K ∧ W ∈ Base K → P ∨ ˙ S ∧ ˙ W ≤ ˙ P ∨ ˙ S
53 10 12 48 52 syl3anc ⊢ φ → P ∨ ˙ S ∧ ˙ W ≤ ˙ P ∨ ˙ S
54 8 53 eqbrtrid ⊢ φ → V ≤ ˙ P ∨ ˙ S
55 13 5 atbase ⊢ U ∈ A → U ∈ Base K
56 33 55 syl ⊢ φ → U ∈ Base K
57 13 5 atbase ⊢ V ∈ A → V ∈ Base K
58 34 57 syl ⊢ φ → V ∈ Base K
59 13 2 3 latjlej12 ⊢ K ∈ Lat ∧ U ∈ Base K ∧ P ∨ ˙ Q ∈ Base K ∧ V ∈ Base K ∧ P ∨ ˙ S ∈ Base K → U ≤ ˙ P ∨ ˙ Q ∧ V ≤ ˙ P ∨ ˙ S → U ∨ ˙ V ≤ ˙ P ∨ ˙ Q ∨ ˙ P ∨ ˙ S
60 10 56 47 58 12 59 syl122anc ⊢ φ → U ≤ ˙ P ∨ ˙ Q ∧ V ≤ ˙ P ∨ ˙ S → U ∨ ˙ V ≤ ˙ P ∨ ˙ Q ∨ ˙ P ∨ ˙ S
61 51 54 60 mp2and ⊢ φ → U ∨ ˙ V ≤ ˙ P ∨ ˙ Q ∨ ˙ P ∨ ˙ S
62 3 5 hlatjass ⊢ K ∈ HL ∧ P ∈ A ∧ Q ∈ A ∧ S ∈ A → P ∨ ˙ Q ∨ ˙ S = P ∨ ˙ Q ∨ ˙ S
63 17 18 20 19 62 syl13anc ⊢ φ → P ∨ ˙ Q ∨ ˙ S = P ∨ ˙ Q ∨ ˙ S
64 13 5 atbase ⊢ P ∈ A → P ∈ Base K
65 18 64 syl ⊢ φ → P ∈ Base K
66 13 5 atbase ⊢ S ∈ A → S ∈ Base K
67 19 66 syl ⊢ φ → S ∈ Base K
68 13 3 latj32 ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K ∧ S ∈ Base K → P ∨ ˙ Q ∨ ˙ S = P ∨ ˙ S ∨ ˙ Q
69 10 65 38 67 68 syl13anc ⊢ φ → P ∨ ˙ Q ∨ ˙ S = P ∨ ˙ S ∨ ˙ Q
70 13 3 latjjdi ⊢ K ∈ Lat ∧ P ∈ Base K ∧ Q ∈ Base K ∧ S ∈ Base K → P ∨ ˙ Q ∨ ˙ S = P ∨ ˙ Q ∨ ˙ P ∨ ˙ S
71 10 65 38 67 70 syl13anc ⊢ φ → P ∨ ˙ Q ∨ ˙ S = P ∨ ˙ Q ∨ ˙ P ∨ ˙ S
72 63 69 71 3eqtr3rd ⊢ φ → P ∨ ˙ Q ∨ ˙ P ∨ ˙ S = P ∨ ˙ S ∨ ˙ Q
73 61 72 breqtrd ⊢ φ → U ∨ ˙ V ≤ ˙ P ∨ ˙ S ∨ ˙ Q
74 13 2 10 32 36 40 45 73 lattrd ⊢ φ → T ≤ ˙ P ∨ ˙ S ∨ ˙ Q
75 2 3 4 5 2atmat ⊢ K ∈ HL ∧ P ∈ A ∧ S ∈ A ∧ Q ∈ A ∧ T ∈ A ∧ P ≠ S ∧ Q ≠ T ∧ ¬ Q ≤ ˙ P ∨ ˙ S ∧ T ≤ ˙ P ∨ ˙ S ∨ ˙ Q → P ∨ ˙ S ∧ ˙ Q ∨ ˙ T ∈ A
76 17 18 19 20 21 22 26 30 74 75 syl333anc ⊢ φ → P ∨ ˙ S ∧ ˙ Q ∨ ˙ T ∈ A
77 16 76 eqeltrd ⊢ φ → C ∈ A