Theorem bj-snglss

Description: The singletonization of a class is included in its powerclass. (Contributed by BJ, 6-Oct-2018)

	Ref	Expression
Assertion	bj-snglss	⊢ sngl 𝐴 ⊆ 𝒫 𝐴

Proof

Step	Hyp	Ref	Expression
1		bj-elsngl	⊢ ( 𝑥 ∈ sngl 𝐴 ↔ ∃ 𝑦 ∈ 𝐴 𝑥 = { 𝑦 } )
2		df-rex	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 = { 𝑦 } ↔ ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑥 = { 𝑦 } ) )
3		snssi	⊢ ( 𝑦 ∈ 𝐴 → { 𝑦 } ⊆ 𝐴 )
4		sseq1	⊢ ( 𝑥 = { 𝑦 } → ( 𝑥 ⊆ 𝐴 ↔ { 𝑦 } ⊆ 𝐴 ) )
5	4	biimparc	⊢ ( ( { 𝑦 } ⊆ 𝐴 ∧ 𝑥 = { 𝑦 } ) → 𝑥 ⊆ 𝐴 )
6	3 5	sylan	⊢ ( ( 𝑦 ∈ 𝐴 ∧ 𝑥 = { 𝑦 } ) → 𝑥 ⊆ 𝐴 )
7	6	eximi	⊢ ( ∃ 𝑦 ( 𝑦 ∈ 𝐴 ∧ 𝑥 = { 𝑦 } ) → ∃ 𝑦 𝑥 ⊆ 𝐴 )
8	2 7	sylbi	⊢ ( ∃ 𝑦 ∈ 𝐴 𝑥 = { 𝑦 } → ∃ 𝑦 𝑥 ⊆ 𝐴 )
9	1 8	sylbi	⊢ ( 𝑥 ∈ sngl 𝐴 → ∃ 𝑦 𝑥 ⊆ 𝐴 )
10		ax5e	⊢ ( ∃ 𝑦 𝑥 ⊆ 𝐴 → 𝑥 ⊆ 𝐴 )
11	9 10	syl	⊢ ( 𝑥 ∈ sngl 𝐴 → 𝑥 ⊆ 𝐴 )
12		velpw	⊢ ( 𝑥 ∈ 𝒫 𝐴 ↔ 𝑥 ⊆ 𝐴 )
13	11 12	sylibr	⊢ ( 𝑥 ∈ sngl 𝐴 → 𝑥 ∈ 𝒫 𝐴 )
14	13	ssriv	⊢ sngl 𝐴 ⊆ 𝒫 𝐴