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 ( 𝐴C → ( ‘ { 𝐴 } ) = 𝐴 )

Proof

Step Hyp Ref Expression
1 snssi ( 𝐴C → { 𝐴 } ⊆ C )
2 chsupval2 ( { 𝐴 } ⊆ C → ( ‘ { 𝐴 } ) = { 𝑥C { 𝐴 } ⊆ 𝑥 } )
3 1 2 syl ( 𝐴C → ( ‘ { 𝐴 } ) = { 𝑥C { 𝐴 } ⊆ 𝑥 } )
4 unisng ( 𝐴C { 𝐴 } = 𝐴 )
5 eqimss ( { 𝐴 } = 𝐴 { 𝐴 } ⊆ 𝐴 )
6 4 5 syl ( 𝐴C { 𝐴 } ⊆ 𝐴 )
7 6 ancli ( 𝐴C → ( 𝐴C { 𝐴 } ⊆ 𝐴 ) )
8 sseq2 ( 𝑥 = 𝐴 → ( { 𝐴 } ⊆ 𝑥 { 𝐴 } ⊆ 𝐴 ) )
9 8 elrab ( 𝐴 ∈ { 𝑥C { 𝐴 } ⊆ 𝑥 } ↔ ( 𝐴C { 𝐴 } ⊆ 𝐴 ) )
10 7 9 sylibr ( 𝐴C𝐴 ∈ { 𝑥C { 𝐴 } ⊆ 𝑥 } )
11 intss1 ( 𝐴 ∈ { 𝑥C { 𝐴 } ⊆ 𝑥 } → { 𝑥C { 𝐴 } ⊆ 𝑥 } ⊆ 𝐴 )
12 10 11 syl ( 𝐴C { 𝑥C { 𝐴 } ⊆ 𝑥 } ⊆ 𝐴 )
13 ssintub { 𝐴 } ⊆ { 𝑥C { 𝐴 } ⊆ 𝑥 }
14 4 13 eqsstrrdi ( 𝐴C𝐴 { 𝑥C { 𝐴 } ⊆ 𝑥 } )
15 12 14 eqssd ( 𝐴C { 𝑥C { 𝐴 } ⊆ 𝑥 } = 𝐴 )
16 3 15 eqtrd ( 𝐴C → ( ‘ { 𝐴 } ) = 𝐴 )