Metamath Proof Explorer

Theorem chsupid

Description: A subspace is the supremum of all smaller subspaces. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

Ref Expression
Assertion chsupid 
|- ( A e. CH -> ( \/H ` { x e. CH | x C_ A } ) = A )

Proof

Step Hyp Ref Expression
1 ssrab2 
 |-  { x e. CH | x C_ A } C_ CH
2 chsupval2 
 |-  ( { x e. CH | x C_ A } C_ CH -> ( \/H ` { x e. CH | x C_ A } ) = |^| { y e. CH | U. { x e. CH | x C_ A } C_ y } )
3 1 2 ax-mp 
 |-  ( \/H ` { x e. CH | x C_ A } ) = |^| { y e. CH | U. { x e. CH | x C_ A } C_ y }
4 unimax 
 |-  ( A e. CH -> U. { x e. CH | x C_ A } = A )
5 4 sseq1d 
 |-  ( A e. CH -> ( U. { x e. CH | x C_ A } C_ y <-> A C_ y ) )
6 5 rabbidv 
 |-  ( A e. CH -> { y e. CH | U. { x e. CH | x C_ A } C_ y } = { y e. CH | A C_ y } )
7 6 inteqd 
 |-  ( A e. CH -> |^| { y e. CH | U. { x e. CH | x C_ A } C_ y } = |^| { y e. CH | A C_ y } )
8 intmin 
 |-  ( A e. CH -> |^| { y e. CH | A C_ y } = A )
9 7 8 eqtrd 
 |-  ( A e. CH -> |^| { y e. CH | U. { x e. CH | x C_ A } C_ y } = A )
10 3 9 syl5eq 
 |-  ( A e. CH -> ( \/H ` { x e. CH | x C_ A } ) = A )