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 C A = A

Proof

Step Hyp Ref Expression
1 snssi A C A C
2 chsupval2 A C A = x C | A x
3 1 2 syl A C A = x C | A x
4 unisng A C A = A
5 eqimss A = A A A
6 4 5 syl A C A A
7 6 ancli A C A C A A
8 sseq2 x = A A x A A
9 8 elrab A x C | A x A C A A
10 7 9 sylibr A C A x C | A x
11 intss1 A x C | A x x C | A x A
12 10 11 syl A C x C | A x A
13 ssintub A x C | A x
14 4 13 eqsstrrdi A C A x C | A x
15 12 14 eqssd A C x C | A x = A
16 3 15 eqtrd A C A = A