Metamath Proof Explorer

Theorem 4atexlemnclw

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

Ref Expression
Hypotheses 4thatlem.ph ⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
4thatlem0.l ⊢ ≤ = ( le ‘ 𝐾 )
4thatlem0.j ⊢ ∨ = ( join ‘ 𝐾 )
4thatlem0.m ⊢ ∧ = ( meet ‘ 𝐾 )
4thatlem0.a ⊢ 𝐴 = ( Atoms ‘ 𝐾 )
4thatlem0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
4thatlem0.u ⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
4thatlem0.v ⊢ 𝑉 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
4thatlem0.c ⊢ 𝐶 = ( ( 𝑄 ∨ 𝑇 ) ∧ ( 𝑃 ∨ 𝑆 ) )
Assertion 4atexlemnclw ( 𝜑 → ¬ 𝐶 ≤ 𝑊 )

Proof

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