This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem atcvat2i

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

Ref Expression
Hypothesis atoml.1 
|- A e. CH
Assertion atcvat2i 
|- ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ A  A e. HAtoms ) )

Proof

Step Hyp Ref Expression
1 atoml.1 
 |-  A e. CH
2 atcv1 
 |-  ( ( ( A e. CH /\ B e. HAtoms /\ C e. HAtoms ) /\ A  ( A = 0H <-> B = C ) )
3 1 2 mp3anl1 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ A  ( A = 0H <-> B = C ) )
4 3 necon3abid 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ A  ( A =/= 0H <-> -. B = C ) )
5 atelch 
 |-  ( B e. HAtoms -> B e. CH )
6 atelch 
 |-  ( C e. HAtoms -> C e. CH )
7 chjcl 
 |-  ( ( B e. CH /\ C e. CH ) -> ( B vH C ) e. CH )
8 5 6 7 syl2an 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( B vH C ) e. CH )
9 cvpss 
 |-  ( ( A e. CH /\ ( B vH C ) e. CH ) -> ( A  A C. ( B vH C ) ) )
10 1 8 9 sylancr 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A  A C. ( B vH C ) ) )
11 1 atcvati 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( A =/= 0H /\ A C. ( B vH C ) ) -> A e. HAtoms ) )
12 11 expcomd 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A C. ( B vH C ) -> ( A =/= 0H -> A e. HAtoms ) ) )
13 10 12 syld 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A  ( A =/= 0H -> A e. HAtoms ) ) )
14 13 imp 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ A  ( A =/= 0H -> A e. HAtoms ) )
15 4 14 sylbird 
 |-  ( ( ( B e. HAtoms /\ C e. HAtoms ) /\ A  ( -. B = C -> A e. HAtoms ) )
16 15 ex 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( A  ( -. B = C -> A e. HAtoms ) ) )
17 16 com23 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( -. B = C -> ( A  A e. HAtoms ) ) )
18 17 impd 
 |-  ( ( B e. HAtoms /\ C e. HAtoms ) -> ( ( -. B = C /\ A  A e. HAtoms ) )