Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Norm Megill
Hilbert lattices
hlatcon2
Next ⟩
4noncolr3
Metamath Proof Explorer
Ascii
Unicode
Theorem
hlatcon2
Description:
Atom exchange combined with contraposition.
(Contributed by
NM
, 13-Jun-2012)
Ref
Expression
Hypotheses
3noncol.l
⊢
≤
˙
=
≤
K
3noncol.j
⊢
∨
˙
=
join
⁡
K
3noncol.a
⊢
A
=
Atoms
⁡
K
Assertion
hlatcon2
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
→
¬
P
≤
˙
R
∨
˙
Q
Proof
Step
Hyp
Ref
Expression
1
3noncol.l
⊢
≤
˙
=
≤
K
2
3noncol.j
⊢
∨
˙
=
join
⁡
K
3
3noncol.a
⊢
A
=
Atoms
⁡
K
4
1
2
3
hlatcon3
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
→
¬
P
≤
˙
Q
∨
˙
R
5
simp1
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
→
K
∈
HL
6
simp22
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
→
Q
∈
A
7
simp23
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
→
R
∈
A
8
2
3
hlatjcom
⊢
K
∈
HL
∧
Q
∈
A
∧
R
∈
A
→
Q
∨
˙
R
=
R
∨
˙
Q
9
5
6
7
8
syl3anc
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
→
Q
∨
˙
R
=
R
∨
˙
Q
10
9
breq2d
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
→
P
≤
˙
Q
∨
˙
R
↔
P
≤
˙
R
∨
˙
Q
11
4
10
mtbid
⊢
K
∈
HL
∧
P
∈
A
∧
Q
∈
A
∧
R
∈
A
∧
P
≠
Q
∧
¬
R
≤
˙
P
∨
˙
Q
→
¬
P
≤
˙
R
∨
˙
Q