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 3 simprbi 
 |-  ( A C. B -> -. B C_ A )
5 iman 
 |-  ( ( x C_ B -> x C_ A ) <-> -. ( x C_ B /\ -. x C_ A ) )
6 5 ralbii 
 |-  ( A. x e. HAtoms ( x C_ B -> x C_ A ) <-> A. x e. HAtoms -. ( x C_ B /\ -. x C_ A ) )
7 ss2rab 
 |-  ( { x e. HAtoms | x C_ B } C_ { x e. HAtoms | x C_ A } <-> A. x e. HAtoms ( x C_ B -> x C_ A ) )
8 ssrab2 
 |-  { x e. HAtoms | x C_ B } C_ HAtoms
9 atssch 
 |-  HAtoms C_ CH
10 8 9 sstri 
 |-  { x e. HAtoms | x C_ B } C_ CH
11 ssrab2 
 |-  { x e. HAtoms | x C_ A } C_ HAtoms
12 11 9 sstri 
 |-  { x e. HAtoms | x C_ A } C_ CH
13 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 } ) ) )
14 10 12 13 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 } ) )
15 2 hatomistici 
 |-  B = ( \/H ` { x e. HAtoms | x C_ B } )
16 1 hatomistici 
 |-  A = ( \/H ` { x e. HAtoms | x C_ A } )
17 14 15 16 3sstr4g 
 |-  ( { x e. HAtoms | x C_ B } C_ { x e. HAtoms | x C_ A } -> B C_ A )
18 7 17 sylbir 
 |-  ( A. x e. HAtoms ( x C_ B -> x C_ A ) -> B C_ A )
19 6 18 sylbir 
 |-  ( A. x e. HAtoms -. ( x C_ B /\ -. x C_ A ) -> B C_ A )
20 19 con3i 
 |-  ( -. B C_ A -> -. A. x e. HAtoms -. ( x C_ B /\ -. x C_ A ) )
21 dfrex2 
 |-  ( E. x e. HAtoms ( x C_ B /\ -. x C_ A ) <-> -. A. x e. HAtoms -. ( x C_ B /\ -. x C_ A ) )
22 20 21 sylibr 
 |-  ( -. B C_ A -> E. x e. HAtoms ( x C_ B /\ -. x C_ A ) )
23 4 22 syl 
 |-  ( A C. B -> E. x e. HAtoms ( x C_ B /\ -. x C_ A ) )