Theorem bj-tagss

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

	Ref	Expression
Assertion	bj-tagss	⊢ tag 𝐴 ⊆ 𝒫 𝐴

Proof

Step	Hyp	Ref	Expression
1		df-bj-tag	⊢ tag 𝐴 = ( sngl 𝐴 ∪ { ∅ } )
2		bj-snglss	⊢ sngl 𝐴 ⊆ 𝒫 𝐴
3		0elpw	⊢ ∅ ∈ 𝒫 𝐴
4		0ex	⊢ ∅ ∈ V
5	4	snss	⊢ ( ∅ ∈ 𝒫 𝐴 ↔ { ∅ } ⊆ 𝒫 𝐴 )
6	3 5	mpbi	⊢ { ∅ } ⊆ 𝒫 𝐴
7	2 6	unssi	⊢ ( sngl 𝐴 ∪ { ∅ } ) ⊆ 𝒫 𝐴
8	1 7	eqsstri	⊢ tag 𝐴 ⊆ 𝒫 𝐴