Theorem pwnss

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

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

Proof

Step	Hyp	Ref	Expression
1		rru	⊢ ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴
2		ssel	⊢ ( 𝒫 𝐴 ⊆ 𝐴 → ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝒫 𝐴 → { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝐴 ) )
3	1 2	mtoi	⊢ ( 𝒫 𝐴 ⊆ 𝐴 → ¬ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝒫 𝐴 )
4		ssrab2	⊢ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ⊆ 𝐴
5		elpw2g	⊢ ( 𝐴 ∈ 𝑉 → ( { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝒫 𝐴 ↔ { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ⊆ 𝐴 ) )
6	4 5	mpbiri	⊢ ( 𝐴 ∈ 𝑉 → { 𝑥 ∈ 𝐴 ∣ ¬ 𝑥 ∈ 𝑥 } ∈ 𝒫 𝐴 )
7	3 6	nsyl3	⊢ ( 𝐴 ∈ 𝑉 → ¬ 𝒫 𝐴 ⊆ 𝐴 )