Metamath Proof Explorer

Theorem chpssati

Description: Two Hilbert lattice elements in a proper subset relationship imply the existence of an atom less than or equal to one but not the other. (Contributed by NM, 10-Jun-2004) (New usage is discouraged.)

Ref Expression
Hypotheses chpssat.1 
|- A e. CH
chpssat.2 
|- B e. CH
Assertion chpssati 
|- ( A C. B -> E. x e. HAtoms ( x C_ B /\ -. x C_ A ) )

Proof

Step Hyp Ref Expression
1 chpssat.1 
 |-  A e. CH
2 chpssat.2 
 |-  B e. CH
3 dfpss3 
 |-  ( A C. B <-> ( A C_ B /\ -. B C_ A ) )
4 iman 
 |-  ( ( x C_ B -> x C_ A ) <-> -. ( x C_ B /\ -. x C_ A ) )
5 4 ralbii 
 |-  ( A. x e. HAtoms ( x C_ B -> x C_ A ) <-> A. x e. HAtoms -. ( x C_ B /\ -. x C_ A ) )
6 ss2rab 
 |-  ( { x e. HAtoms | x C_ B } C_ { x e. HAtoms | x C_ A } <-> A. x e. HAtoms ( x C_ B -> x C_ A ) )
7 ssrab2 
 |-  { x e. HAtoms | x C_ B } C_ HAtoms
8 atssch 
 |-  HAtoms C_ CH
9 7 8 sstri 
 |-  { x e. HAtoms | x C_ B } C_ CH
10 ssrab2 
 |-  { x e. HAtoms | x C_ A } C_ HAtoms
11 10 8 sstri 
 |-  { x e. HAtoms | x C_ A } C_ CH
12 chsupss 
 |-  ( ( { x e. HAtoms | x C_ B } C_ CH /\ { x e. HAtoms | x C_ A } C_ CH ) -> ( { x e. HAtoms | x C_ B } C_ { x e. HAtoms | x C_ A } -> ( \/H ` { x e. HAtoms | x C_ B } ) C_ ( \/H ` { x e. HAtoms | x C_ A } ) ) )
13 9 11 12 mp2an 
 |-  ( { x e. HAtoms | x C_ B } C_ { x e. HAtoms | x C_ A } -> ( \/H ` { x e. HAtoms | x C_ B } ) C_ ( \/H ` { x e. HAtoms | x C_ A } ) )
14 2 hatomistici 
 |-  B = ( \/H ` { x e. HAtoms | x C_ B } )
15 1 hatomistici 
 |-  A = ( \/H ` { x e. HAtoms | x C_ A } )
16 13 14 15 3sstr4g 
 |-  ( { x e. HAtoms | x C_ B } C_ { x e. HAtoms | x C_ A } -> B C_ A )
17 6 16 sylbir 
 |-  ( A. x e. HAtoms ( x C_ B -> x C_ A ) -> B C_ A )
18 5 17 sylbir 
 |-  ( A. x e. HAtoms -. ( x C_ B /\ -. x C_ A ) -> B C_ A )
19 18 con3i 
 |-  ( -. B C_ A -> -. A. x e. HAtoms -. ( x C_ B /\ -. x C_ A ) )
20 dfrex2 
 |-  ( E. x e. HAtoms ( x C_ B /\ -. x C_ A ) <-> -. A. x e. HAtoms -. ( x C_ B /\ -. x C_ A ) )
21 19 20 sylibr 
 |-  ( -. B C_ A -> E. x e. HAtoms ( x C_ B /\ -. x C_ A ) )
22 3 21 simplbiim 
 |-  ( A C. B -> E. x e. HAtoms ( x C_ B /\ -. x C_ A ) )