Theorem pwnss

Description: The power set of a set is never a subset. (Contributed by Stefan O'Rear, 22-Feb-2015) (Proof shortened by BJ, 24-Jul-2025)

	Ref	Expression
Assertion	pwnss	⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝒫 𝐴 ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		rru	⊢ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴
2		ssel	⊢ ( 𝒫 𝐴 ⊆ 𝐴 → ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝒫 𝐴 → { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ) )
3	1 2	mtoi	⊢ ( 𝒫 𝐴 ⊆ 𝐴 → ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝒫 𝐴 )
4		rabelpw	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝒫 𝐴 )
5	3 4	nsyl3	⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝒫 𝐴 ⊆ 𝐴 )