Theorem pwtp

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

	Ref	Expression
Assertion	pwtp	⊢ 𝒫 { 𝐴 , 𝐵 , 𝐶 } = ( ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ∪ ( { { 𝐶 } , { 𝐴 , 𝐶 } } ∪ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) )

Proof

Step	Hyp	Ref	Expression
1		velpw	⊢ ( 𝑥 ∈ 𝒫 { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑥 ⊆ { 𝐴 , 𝐵 , 𝐶 } )
2		elun	⊢ ( 𝑥 ∈ ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ↔ ( 𝑥 ∈ { ∅ , { 𝐴 } } ∨ 𝑥 ∈ { { 𝐵 } , { 𝐴 , 𝐵 } } ) )
3		vex	⊢ 𝑥 ∈ V
4	3	elpr	⊢ ( 𝑥 ∈ { ∅ , { 𝐴 } } ↔ ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) )
5	3	elpr	⊢ ( 𝑥 ∈ { { 𝐵 } , { 𝐴 , 𝐵 } } ↔ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) )
6	4 5	orbi12i	⊢ ( ( 𝑥 ∈ { ∅ , { 𝐴 } } ∨ 𝑥 ∈ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ↔ ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) )
7	2 6	bitri	⊢ ( 𝑥 ∈ ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ↔ ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) )
8		elun	⊢ ( 𝑥 ∈ ( { { 𝐶 } , { 𝐴 , 𝐶 } } ∪ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) ↔ ( 𝑥 ∈ { { 𝐶 } , { 𝐴 , 𝐶 } } ∨ 𝑥 ∈ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) )
9	3	elpr	⊢ ( 𝑥 ∈ { { 𝐶 } , { 𝐴 , 𝐶 } } ↔ ( 𝑥 = { 𝐶 } ∨ 𝑥 = { 𝐴 , 𝐶 } ) )
10	3	elpr	⊢ ( 𝑥 ∈ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ↔ ( 𝑥 = { 𝐵 , 𝐶 } ∨ 𝑥 = { 𝐴 , 𝐵 , 𝐶 } ) )
11	9 10	orbi12i	⊢ ( ( 𝑥 ∈ { { 𝐶 } , { 𝐴 , 𝐶 } } ∨ 𝑥 ∈ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) ↔ ( ( 𝑥 = { 𝐶 } ∨ 𝑥 = { 𝐴 , 𝐶 } ) ∨ ( 𝑥 = { 𝐵 , 𝐶 } ∨ 𝑥 = { 𝐴 , 𝐵 , 𝐶 } ) ) )
12	8 11	bitri	⊢ ( 𝑥 ∈ ( { { 𝐶 } , { 𝐴 , 𝐶 } } ∪ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) ↔ ( ( 𝑥 = { 𝐶 } ∨ 𝑥 = { 𝐴 , 𝐶 } ) ∨ ( 𝑥 = { 𝐵 , 𝐶 } ∨ 𝑥 = { 𝐴 , 𝐵 , 𝐶 } ) ) )
13	7 12	orbi12i	⊢ ( ( 𝑥 ∈ ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ∨ 𝑥 ∈ ( { { 𝐶 } , { 𝐴 , 𝐶 } } ∪ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) ) ↔ ( ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) ∨ ( ( 𝑥 = { 𝐶 } ∨ 𝑥 = { 𝐴 , 𝐶 } ) ∨ ( 𝑥 = { 𝐵 , 𝐶 } ∨ 𝑥 = { 𝐴 , 𝐵 , 𝐶 } ) ) ) )
14		elun	⊢ ( 𝑥 ∈ ( ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ∪ ( { { 𝐶 } , { 𝐴 , 𝐶 } } ∪ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) ) ↔ ( 𝑥 ∈ ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ∨ 𝑥 ∈ ( { { 𝐶 } , { 𝐴 , 𝐶 } } ∪ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) ) )
15		sstp	⊢ ( 𝑥 ⊆ { 𝐴 , 𝐵 , 𝐶 } ↔ ( ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) ∨ ( ( 𝑥 = { 𝐶 } ∨ 𝑥 = { 𝐴 , 𝐶 } ) ∨ ( 𝑥 = { 𝐵 , 𝐶 } ∨ 𝑥 = { 𝐴 , 𝐵 , 𝐶 } ) ) ) )
16	13 14 15	3bitr4ri	⊢ ( 𝑥 ⊆ { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑥 ∈ ( ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ∪ ( { { 𝐶 } , { 𝐴 , 𝐶 } } ∪ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) ) )
17	1 16	bitri	⊢ ( 𝑥 ∈ 𝒫 { 𝐴 , 𝐵 , 𝐶 } ↔ 𝑥 ∈ ( ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ∪ ( { { 𝐶 } , { 𝐴 , 𝐶 } } ∪ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) ) )
18	17	eqriv	⊢ 𝒫 { 𝐴 , 𝐵 , 𝐶 } = ( ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ∪ ( { { 𝐶 } , { 𝐴 , 𝐶 } } ∪ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) )