Metamath Proof Explorer


Theorem iscvlat2N

Description: The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012) (New usage is discouraged.)

Ref Expression
Hypotheses iscvlat2.b B = Base K
iscvlat2.l ˙ = K
iscvlat2.j ˙ = join K
iscvlat2.m ˙ = meet K
iscvlat2.z 0 ˙ = 0. K
iscvlat2.a A = Atoms K
Assertion iscvlat2N K CvLat K AtLat p A q A x B p ˙ x = 0 ˙ p ˙ x ˙ q q ˙ x ˙ p

Proof

Step Hyp Ref Expression
1 iscvlat2.b B = Base K
2 iscvlat2.l ˙ = K
3 iscvlat2.j ˙ = join K
4 iscvlat2.m ˙ = meet K
5 iscvlat2.z 0 ˙ = 0. K
6 iscvlat2.a A = Atoms K
7 1 2 3 6 iscvlat K CvLat K AtLat p A q A x B ¬ p ˙ x p ˙ x ˙ q q ˙ x ˙ p
8 simpll K AtLat p A q A x B K AtLat
9 simplrl K AtLat p A q A x B p A
10 simpr K AtLat p A q A x B x B
11 1 2 4 5 6 atnle K AtLat p A x B ¬ p ˙ x p ˙ x = 0 ˙
12 8 9 10 11 syl3anc K AtLat p A q A x B ¬ p ˙ x p ˙ x = 0 ˙
13 12 anbi1d K AtLat p A q A x B ¬ p ˙ x p ˙ x ˙ q p ˙ x = 0 ˙ p ˙ x ˙ q
14 13 imbi1d K AtLat p A q A x B ¬ p ˙ x p ˙ x ˙ q q ˙ x ˙ p p ˙ x = 0 ˙ p ˙ x ˙ q q ˙ x ˙ p
15 14 ralbidva K AtLat p A q A x B ¬ p ˙ x p ˙ x ˙ q q ˙ x ˙ p x B p ˙ x = 0 ˙ p ˙ x ˙ q q ˙ x ˙ p
16 15 2ralbidva K AtLat p A q A x B ¬ p ˙ x p ˙ x ˙ q q ˙ x ˙ p p A q A x B p ˙ x = 0 ˙ p ˙ x ˙ q q ˙ x ˙ p
17 16 pm5.32i K AtLat p A q A x B ¬ p ˙ x p ˙ x ˙ q q ˙ x ˙ p K AtLat p A q A x B p ˙ x = 0 ˙ p ˙ x ˙ q q ˙ x ˙ p
18 7 17 bitri K CvLat K AtLat p A q A x B p ˙ x = 0 ˙ p ˙ x ˙ q q ˙ x ˙ p