Metamath Proof Explorer


Theorem atcvat2

Description: A Hilbert lattice element covered by the join of two distinct atoms is an atom. (Contributed by NM, 29-Jun-2004) (New usage is discouraged.)

Ref Expression
Assertion atcvat2 A C B HAtoms C HAtoms ¬ B = C A B C A HAtoms

Proof

Step Hyp Ref Expression
1 breq1 A = if A C A 0 A B C if A C A 0 B C
2 1 anbi2d A = if A C A 0 ¬ B = C A B C ¬ B = C if A C A 0 B C
3 eleq1 A = if A C A 0 A HAtoms if A C A 0 HAtoms
4 2 3 imbi12d A = if A C A 0 ¬ B = C A B C A HAtoms ¬ B = C if A C A 0 B C if A C A 0 HAtoms
5 4 imbi2d A = if A C A 0 B HAtoms C HAtoms ¬ B = C A B C A HAtoms B HAtoms C HAtoms ¬ B = C if A C A 0 B C if A C A 0 HAtoms
6 h0elch 0 C
7 6 elimel if A C A 0 C
8 7 atcvat2i B HAtoms C HAtoms ¬ B = C if A C A 0 B C if A C A 0 HAtoms
9 5 8 dedth A C B HAtoms C HAtoms ¬ B = C A B C A HAtoms
10 9 3impib A C B HAtoms C HAtoms ¬ B = C A B C A HAtoms