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