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

Metamath Proof Explorer

Theorem pwpr

Description: The power set of an unordered pair. (Contributed by NM, 1-May-2009)

Ref Expression
Assertion pwpr 𝒫 { 𝐴 , 𝐵 } = ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } )

Proof

Step Hyp Ref Expression
1 sspr ⊢ ( 𝑥 ⊆ { 𝐴 , 𝐵 } ↔ ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) )
2 vex ⊢ 𝑥 ∈ V
3 2 elpr ⊢ ( 𝑥 ∈ { ∅ , { 𝐴 } } ↔ ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) )
4 2 elpr ⊢ ( 𝑥 ∈ { { 𝐵 } , { 𝐴 , 𝐵 } } ↔ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) )
5 3 4 orbi12i ⊢ ( ( 𝑥 ∈ { ∅ , { 𝐴 } } ∨ 𝑥 ∈ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ↔ ( ( 𝑥 = ∅ ∨ 𝑥 = { 𝐴 } ) ∨ ( 𝑥 = { 𝐵 } ∨ 𝑥 = { 𝐴 , 𝐵 } ) ) )
6 1 5 bitr4i ⊢ ( 𝑥 ⊆ { 𝐴 , 𝐵 } ↔ ( 𝑥 ∈ { ∅ , { 𝐴 } } ∨ 𝑥 ∈ { { 𝐵 } , { 𝐴 , 𝐵 } } ) )
7 velpw ⊢ ( 𝑥 ∈ 𝒫 { 𝐴 , 𝐵 } ↔ 𝑥 ⊆ { 𝐴 , 𝐵 } )
8 elun ⊢ ( 𝑥 ∈ ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) ↔ ( 𝑥 ∈ { ∅ , { 𝐴 } } ∨ 𝑥 ∈ { { 𝐵 } , { 𝐴 , 𝐵 } } ) )
9 6 7 8 3bitr4i ⊢ ( 𝑥 ∈ 𝒫 { 𝐴 , 𝐵 } ↔ 𝑥 ∈ ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } ) )
10 9 eqriv ⊢ 𝒫 { 𝐴 , 𝐵 } = ( { ∅ , { 𝐴 } } ∪ { { 𝐵 } , { 𝐴 , 𝐵 } } )