Metamath Proof Explorer


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 A V ¬ 𝒫 A A

Proof

Step Hyp Ref Expression
1 rru ¬ x A | ¬ x x A
2 ssel 𝒫 A A x A | ¬ x x 𝒫 A x A | ¬ x x A
3 1 2 mtoi 𝒫 A A ¬ x A | ¬ x x 𝒫 A
4 ssrab2 x A | ¬ x x A
5 elpw2g A V x A | ¬ x x 𝒫 A x A | ¬ x x A
6 4 5 mpbiri A V x A | ¬ x x 𝒫 A
7 3 6 nsyl3 A V ¬ 𝒫 A A