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 𝒫 { 𝐴 , 𝐵 , 𝐶 } = ( ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ∪ ( { { 𝐶 } , { 𝐴 , 𝐶 } } ∪ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) )

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 ⊢ 𝒫 { 𝐴 , 𝐵 , 𝐶 } = ( ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ∪ ( { { 𝐶 } , { 𝐴 , 𝐶 } } ∪ { { 𝐵 , 𝐶 } , { 𝐴 , 𝐵 , 𝐶 } } ) )