Metamath Proof Explorer


Theorem pwtp

Description: The power set of an unordered triple. (Contributed by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion pwtp 𝒫ABC=ABABCACBCABC

Proof

Step Hyp Ref Expression
1 velpw x𝒫ABCxABC
2 elun xABABxAxBAB
3 vex xV
4 3 elpr xAx=x=A
5 3 elpr xBABx=Bx=AB
6 4 5 orbi12i xAxBABx=x=Ax=Bx=AB
7 2 6 bitri xABABx=x=Ax=Bx=AB
8 elun xCACBCABCxCACxBCABC
9 3 elpr xCACx=Cx=AC
10 3 elpr xBCABCx=BCx=ABC
11 9 10 orbi12i xCACxBCABCx=Cx=ACx=BCx=ABC
12 8 11 bitri xCACBCABCx=Cx=ACx=BCx=ABC
13 7 12 orbi12i xABABxCACBCABCx=x=Ax=Bx=ABx=Cx=ACx=BCx=ABC
14 elun xABABCACBCABCxABABxCACBCABC
15 sstp xABCx=x=Ax=Bx=ABx=Cx=ACx=BCx=ABC
16 13 14 15 3bitr4ri xABCxABABCACBCABC
17 1 16 bitri x𝒫ABCxABABCACBCABC
18 17 eqriv 𝒫ABC=ABABCACBCABC