This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 } } ) )