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

Metamath Proof Explorer

Theorem chsupsn

Description: Value of supremum of subset of CH on a singleton. (Contributed by NM, 13-Aug-2002) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 snssi 
 |-  ( A e. CH -> { A } C_ CH )
2 chsupval2 
 |-  ( { A } C_ CH -> ( \/H ` { A } ) = |^| { x e. CH | U. { A } C_ x } )
3 1 2 syl 
 |-  ( A e. CH -> ( \/H ` { A } ) = |^| { x e. CH | U. { A } C_ x } )
4 unisng 
 |-  ( A e. CH -> U. { A } = A )
5 eqimss 
 |-  ( U. { A } = A -> U. { A } C_ A )
6 4 5 syl 
 |-  ( A e. CH -> U. { A } C_ A )
7 6 ancli 
 |-  ( A e. CH -> ( A e. CH /\ U. { A } C_ A ) )
8 sseq2 
 |-  ( x = A -> ( U. { A } C_ x <-> U. { A } C_ A ) )
9 8 elrab 
 |-  ( A e. { x e. CH | U. { A } C_ x } <-> ( A e. CH /\ U. { A } C_ A ) )
10 7 9 sylibr 
 |-  ( A e. CH -> A e. { x e. CH | U. { A } C_ x } )
11 intss1 
 |-  ( A e. { x e. CH | U. { A } C_ x } -> |^| { x e. CH | U. { A } C_ x } C_ A )
12 10 11 syl 
 |-  ( A e. CH -> |^| { x e. CH | U. { A } C_ x } C_ A )
13 ssintub 
 |-  U. { A } C_ |^| { x e. CH | U. { A } C_ x }
14 4 13 eqsstrrdi 
 |-  ( A e. CH -> A C_ |^| { x e. CH | U. { A } C_ x } )
15 12 14 eqssd 
 |-  ( A e. CH -> |^| { x e. CH | U. { A } C_ x } = A )
16 3 15 eqtrd 
 |-  ( A e. CH -> ( \/H ` { A } ) = A )