Metamath Proof Explorer

Theorem pwtp

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

Ref Expression
Assertion pwtp ⊢ 𝒫 A B C = ∅ A ∪ B A B ∪ C A C ∪ B C A B C

Proof

Step Hyp Ref Expression
1 velpw ⊢ x ∈ 𝒫 A B C ↔ x ⊆ A B C
2 elun ⊢ x ∈ ∅ A ∪ B A B ↔ x ∈ ∅ A ∨ x ∈ B A B
3 vex ⊢ x ∈ V
4 3 elpr ⊢ x ∈ ∅ A ↔ x = ∅ ∨ x = A
5 3 elpr ⊢ x ∈ B A B ↔ x = B ∨ x = A B
6 4 5 orbi12i ⊢ x ∈ ∅ A ∨ x ∈ B A B ↔ x = ∅ ∨ x = A ∨ x = B ∨ x = A B
7 2 6 bitri ⊢ x ∈ ∅ A ∪ B A B ↔ x = ∅ ∨ x = A ∨ x = B ∨ x = A B
8 elun ⊢ x ∈ C A C ∪ B C A B C ↔ x ∈ C A C ∨ x ∈ B C A B C
9 3 elpr ⊢ x ∈ C A C ↔ x = C ∨ x = A C
10 3 elpr ⊢ x ∈ B C A B C ↔ x = B C ∨ x = A B C
11 9 10 orbi12i ⊢ x ∈ C A C ∨ x ∈ B C A B C ↔ x = C ∨ x = A C ∨ x = B C ∨ x = A B C
12 8 11 bitri ⊢ x ∈ C A C ∪ B C A B C ↔ x = C ∨ x = A C ∨ x = B C ∨ x = A B C
13 7 12 orbi12i ⊢ x ∈ ∅ A ∪ B A B ∨ x ∈ C A C ∪ 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 ∈ ∅ A ∪ B A B ∪ C A C ∪ B C A B C ↔ x ∈ ∅ A ∪ B A B ∨ x ∈ C A C ∪ B C A B C
15 sstp ⊢ x ⊆ 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 ⊆ A B C ↔ x ∈ ∅ A ∪ B A B ∪ C A C ∪ B C A B C
17 1 16 bitri ⊢ x ∈ 𝒫 A B C ↔ x ∈ ∅ A ∪ B A B ∪ C A C ∪ B C A B C
18 17 eqriv ⊢ 𝒫 A B C = ∅ A ∪ B A B ∪ C A C ∪ B C A B C