Theorem pwtp

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

	Ref	Expression
Assertion	pwtp	|- ~P { A , B , C } = ( ( { (/) , { A } } u. { { B } , { A , B } } ) u. ( { { C } , { A , C } } u. { { B , C } , { A , B , C } } ) )

Proof

Step	Hyp	Ref	Expression
1		velpw	|- ( x e. ~P { A , B , C } <-> x C_ { A , B , C } )
2		elun	|- ( x e. ( { (/) , { A } } u. { { B } , { A , B } } ) <-> ( x e. { (/) , { A } } \/ x e. { { B } , { A , B } } ) )
3		vex	|- x e. _V
4	3	elpr	|- ( x e. { (/) , { A } } <-> ( x = (/) \/ x = { A } ) )
5	3	elpr	|- ( x e. { { B } , { A , B } } <-> ( x = { B } \/ x = { A , B } ) )
6	4 5	orbi12i	|- ( ( x e. { (/) , { A } } \/ x e. { { B } , { A , B } } ) <-> ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) )
7	2 6	bitri	|- ( x e. ( { (/) , { A } } u. { { B } , { A , B } } ) <-> ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) )
8		elun	|- ( x e. ( { { C } , { A , C } } u. { { B , C } , { A , B , C } } ) <-> ( x e. { { C } , { A , C } } \/ x e. { { B , C } , { A , B , C } } ) )
9	3	elpr	|- ( x e. { { C } , { A , C } } <-> ( x = { C } \/ x = { A , C } ) )
10	3	elpr	|- ( x e. { { B , C } , { A , B , C } } <-> ( x = { B , C } \/ x = { A , B , C } ) )
11	9 10	orbi12i	|- ( ( x e. { { C } , { A , C } } \/ x e. { { B , C } , { A , B , C } } ) <-> ( ( x = { C } \/ x = { A , C } ) \/ ( x = { B , C } \/ x = { A , B , C } ) ) )
12	8 11	bitri	|- ( x e. ( { { C } , { A , C } } u. { { B , C } , { A , B , C } } ) <-> ( ( x = { C } \/ x = { A , C } ) \/ ( x = { B , C } \/ x = { A , B , C } ) ) )
13	7 12	orbi12i	|- ( ( x e. ( { (/) , { A } } u. { { B } , { A , B } } ) \/ x e. ( { { C } , { A , C } } u. { { B , C } , { A , B , C } } ) ) <-> ( ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) \/ ( ( x = { C } \/ x = { A , C } ) \/ ( x = { B , C } \/ x = { A , B , C } ) ) ) )
14		elun	|- ( x e. ( ( { (/) , { A } } u. { { B } , { A , B } } ) u. ( { { C } , { A , C } } u. { { B , C } , { A , B , C } } ) ) <-> ( x e. ( { (/) , { A } } u. { { B } , { A , B } } ) \/ x e. ( { { C } , { A , C } } u. { { B , C } , { A , B , C } } ) ) )
15		sstp	|- ( x C_ { A , B , C } <-> ( ( ( x = (/) \/ x = { A } ) \/ ( x = { B } \/ x = { A , B } ) ) \/ ( ( x = { C } \/ x = { A , C } ) \/ ( x = { B , C } \/ x = { A , B , C } ) ) ) )
16	13 14 15	3bitr4ri	|- ( x C_ { A , B , C } <-> x e. ( ( { (/) , { A } } u. { { B } , { A , B } } ) u. ( { { C } , { A , C } } u. { { B , C } , { A , B , C } } ) ) )
17	1 16	bitri	|- ( x e. ~P { A , B , C } <-> x e. ( ( { (/) , { A } } u. { { B } , { A , B } } ) u. ( { { C } , { A , C } } u. { { B , C } , { A , B , C } } ) ) )
18	17	eqriv	|- ~P { A , B , C } = ( ( { (/) , { A } } u. { { B } , { A , B } } ) u. ( { { C } , { A , C } } u. { { B , C } , { A , B , C } } ) )