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 )