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 |
1 2 3 4 5 6 7 8
|
4atexlemtlw |
⊢ ( 𝜑 → 𝑇 ≤ 𝑊 ) |
10 |
1
|
4atexlemkc |
⊢ ( 𝜑 → 𝐾 ∈ CvLat ) |
11 |
1 2 3 4 5 6 7
|
4atexlemu |
⊢ ( 𝜑 → 𝑈 ∈ 𝐴 ) |
12 |
1 2 3 4 5 6 7 8
|
4atexlemv |
⊢ ( 𝜑 → 𝑉 ∈ 𝐴 ) |
13 |
1
|
4atexlemt |
⊢ ( 𝜑 → 𝑇 ∈ 𝐴 ) |
14 |
1 2 3 4 5 6 7 8
|
4atexlemunv |
⊢ ( 𝜑 → 𝑈 ≠ 𝑉 ) |
15 |
1
|
4atexlemutvt |
⊢ ( 𝜑 → ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) |
16 |
5 3
|
cvlsupr5 |
⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ≠ 𝑉 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) → 𝑇 ≠ 𝑈 ) |
17 |
10 11 12 13 14 15 16
|
syl132anc |
⊢ ( 𝜑 → 𝑇 ≠ 𝑈 ) |
18 |
17
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑇 ≠ 𝑈 ) |
19 |
1
|
4atexlemk |
⊢ ( 𝜑 → 𝐾 ∈ HL ) |
20 |
1
|
4atexlemw |
⊢ ( 𝜑 → 𝑊 ∈ 𝐻 ) |
21 |
19 20
|
jca |
⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
22 |
21
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ) |
23 |
1
|
4atexlempw |
⊢ ( 𝜑 → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) |
24 |
23
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) |
25 |
1
|
4atexlemq |
⊢ ( 𝜑 → 𝑄 ∈ 𝐴 ) |
26 |
25
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑄 ∈ 𝐴 ) |
27 |
13
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑇 ∈ 𝐴 ) |
28 |
1
|
4atexlempnq |
⊢ ( 𝜑 → 𝑃 ≠ 𝑄 ) |
29 |
28
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑃 ≠ 𝑄 ) |
30 |
|
simpr |
⊢ ( ( 𝜑 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) |
31 |
2 3 4 5 6 7
|
lhpat3 |
⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ) ∧ ( 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑄 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) ) → ( ¬ 𝑇 ≤ 𝑊 ↔ 𝑇 ≠ 𝑈 ) ) |
32 |
22 24 26 27 29 30 31
|
syl222anc |
⊢ ( ( 𝜑 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → ( ¬ 𝑇 ≤ 𝑊 ↔ 𝑇 ≠ 𝑈 ) ) |
33 |
18 32
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) → ¬ 𝑇 ≤ 𝑊 ) |
34 |
33
|
ex |
⊢ ( 𝜑 → ( 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) → ¬ 𝑇 ≤ 𝑊 ) ) |
35 |
9 34
|
mt2d |
⊢ ( 𝜑 → ¬ 𝑇 ≤ ( 𝑃 ∨ 𝑄 ) ) |