Step |
Hyp |
Ref |
Expression |
1 |
|
3dim0.j |
⊢ ∨ = ( join ‘ 𝐾 ) |
2 |
|
3dim0.l |
⊢ ≤ = ( le ‘ 𝐾 ) |
3 |
|
3dim0.a |
⊢ 𝐴 = ( Atoms ‘ 𝐾 ) |
4 |
|
neeq2 |
⊢ ( 𝑞 = 𝑢 → ( 𝑃 ≠ 𝑞 ↔ 𝑃 ≠ 𝑢 ) ) |
5 |
|
oveq2 |
⊢ ( 𝑞 = 𝑢 → ( 𝑃 ∨ 𝑞 ) = ( 𝑃 ∨ 𝑢 ) ) |
6 |
5
|
breq2d |
⊢ ( 𝑞 = 𝑢 → ( 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ↔ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) |
7 |
6
|
notbid |
⊢ ( 𝑞 = 𝑢 → ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ↔ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ) ) |
8 |
5
|
oveq1d |
⊢ ( 𝑞 = 𝑢 → ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) = ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ) |
9 |
8
|
breq2d |
⊢ ( 𝑞 = 𝑢 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ↔ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ) ) |
10 |
9
|
notbid |
⊢ ( 𝑞 = 𝑢 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ↔ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ) ) |
11 |
4 7 10
|
3anbi123d |
⊢ ( 𝑞 = 𝑢 → ( ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ↔ ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ) ) ) |
12 |
|
breq1 |
⊢ ( 𝑟 = 𝑣 → ( 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ↔ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ) ) |
13 |
12
|
notbid |
⊢ ( 𝑟 = 𝑣 → ( ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ↔ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ) ) |
14 |
|
oveq2 |
⊢ ( 𝑟 = 𝑣 → ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) = ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) |
15 |
14
|
breq2d |
⊢ ( 𝑟 = 𝑣 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ↔ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) |
16 |
15
|
notbid |
⊢ ( 𝑟 = 𝑣 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ↔ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) |
17 |
13 16
|
3anbi23d |
⊢ ( 𝑟 = 𝑣 → ( ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑟 ) ) ↔ ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ) |
18 |
|
breq1 |
⊢ ( 𝑠 = 𝑤 → ( 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ↔ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) |
19 |
18
|
notbid |
⊢ ( 𝑠 = 𝑤 → ( ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ↔ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) |
20 |
19
|
3anbi3d |
⊢ ( 𝑠 = 𝑤 → ( ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ↔ ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) ) |
21 |
11 17 20
|
rspc3ev |
⊢ ( ( ( 𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴 ) ∧ ( 𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ ( 𝑃 ∨ 𝑢 ) ∧ ¬ 𝑤 ≤ ( ( 𝑃 ∨ 𝑢 ) ∨ 𝑣 ) ) ) → ∃ 𝑞 ∈ 𝐴 ∃ 𝑟 ∈ 𝐴 ∃ 𝑠 ∈ 𝐴 ( 𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ ( 𝑃 ∨ 𝑞 ) ∧ ¬ 𝑠 ≤ ( ( 𝑃 ∨ 𝑞 ) ∨ 𝑟 ) ) ) |