Metamath Proof Explorer

Theorem ex-pw

Description: Example for df-pw . Example by David A. Wheeler. (Contributed by Mario Carneiro, 2-Jul-2016)

Ref Expression
Assertion ex-pw ( 𝐴 = { 3 , 5 , 7 } → 𝒫 𝐴 = ( ( { ∅ } ∪ { { 3 } , { 5 } , { 7 } } ) ∪ ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } ∪ { { 3 , 5 , 7 } } ) ) )

Proof

Step Hyp Ref Expression
1 pweq ⊢ ( 𝐴 = { 3 , 5 , 7 } → 𝒫 𝐴 = 𝒫 { 3 , 5 , 7 } )
2 qdass ⊢ ( { ∅ , { 3 } } ∪ { { 5 } , { 3 , 5 } } ) = ( { ∅ , { 3 } , { 5 } } ∪ { { 3 , 5 } } )
3 qdassr ⊢ ( { { 7 } , { 3 , 7 } } ∪ { { 5 , 7 } , { 3 , 5 , 7 } } ) = ( { { 7 } } ∪ { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } )
4 2 3 uneq12i ⊢ ( ( { ∅ , { 3 } } ∪ { { 5 } , { 3 , 5 } } ) ∪ ( { { 7 } , { 3 , 7 } } ∪ { { 5 , 7 } , { 3 , 5 , 7 } } ) ) = ( ( { ∅ , { 3 } , { 5 } } ∪ { { 3 , 5 } } ) ∪ ( { { 7 } } ∪ { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) )
5 pwtp ⊢ 𝒫 { 3 , 5 , 7 } = ( ( { ∅ , { 3 } } ∪ { { 5 } , { 3 , 5 } } ) ∪ ( { { 7 } , { 3 , 7 } } ∪ { { 5 , 7 } , { 3 , 5 , 7 } } ) )
6 df-tp ⊢ { { 3 } , { 5 } , { 7 } } = ( { { 3 } , { 5 } } ∪ { { 7 } } )
7 6 uneq2i ⊢ ( { ∅ } ∪ { { 3 } , { 5 } , { 7 } } ) = ( { ∅ } ∪ ( { { 3 } , { 5 } } ∪ { { 7 } } ) )
8 unass ⊢ ( ( { ∅ } ∪ { { 3 } , { 5 } } ) ∪ { { 7 } } ) = ( { ∅ } ∪ ( { { 3 } , { 5 } } ∪ { { 7 } } ) )
9 7 8 eqtr4i ⊢ ( { ∅ } ∪ { { 3 } , { 5 } , { 7 } } ) = ( ( { ∅ } ∪ { { 3 } , { 5 } } ) ∪ { { 7 } } )
10 tpass ⊢ { ∅ , { 3 } , { 5 } } = ( { ∅ } ∪ { { 3 } , { 5 } } )
11 10 uneq1i ⊢ ( { ∅ , { 3 } , { 5 } } ∪ { { 7 } } ) = ( ( { ∅ } ∪ { { 3 } , { 5 } } ) ∪ { { 7 } } )
12 9 11 eqtr4i ⊢ ( { ∅ } ∪ { { 3 } , { 5 } , { 7 } } ) = ( { ∅ , { 3 } , { 5 } } ∪ { { 7 } } )
13 unass ⊢ ( ( { { 3 , 5 } } ∪ { { 3 , 7 } , { 5 , 7 } } ) ∪ { { 3 , 5 , 7 } } ) = ( { { 3 , 5 } } ∪ ( { { 3 , 7 } , { 5 , 7 } } ∪ { { 3 , 5 , 7 } } ) )
14 tpass ⊢ { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } = ( { { 3 , 5 } } ∪ { { 3 , 7 } , { 5 , 7 } } )
15 14 uneq1i ⊢ ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } ∪ { { 3 , 5 , 7 } } ) = ( ( { { 3 , 5 } } ∪ { { 3 , 7 } , { 5 , 7 } } ) ∪ { { 3 , 5 , 7 } } )
16 df-tp ⊢ { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } = ( { { 3 , 7 } , { 5 , 7 } } ∪ { { 3 , 5 , 7 } } )
17 16 uneq2i ⊢ ( { { 3 , 5 } } ∪ { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) = ( { { 3 , 5 } } ∪ ( { { 3 , 7 } , { 5 , 7 } } ∪ { { 3 , 5 , 7 } } ) )
18 13 15 17 3eqtr4i ⊢ ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } ∪ { { 3 , 5 , 7 } } ) = ( { { 3 , 5 } } ∪ { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } )
19 12 18 uneq12i ⊢ ( ( { ∅ } ∪ { { 3 } , { 5 } , { 7 } } ) ∪ ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } ∪ { { 3 , 5 , 7 } } ) ) = ( ( { ∅ , { 3 } , { 5 } } ∪ { { 7 } } ) ∪ ( { { 3 , 5 } } ∪ { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) )
20 un4 ⊢ ( ( { ∅ , { 3 } , { 5 } } ∪ { { 3 , 5 } } ) ∪ ( { { 7 } } ∪ { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) ) = ( ( { ∅ , { 3 } , { 5 } } ∪ { { 7 } } ) ∪ ( { { 3 , 5 } } ∪ { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) )
21 19 20 eqtr4i ⊢ ( ( { ∅ } ∪ { { 3 } , { 5 } , { 7 } } ) ∪ ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } ∪ { { 3 , 5 , 7 } } ) ) = ( ( { ∅ , { 3 } , { 5 } } ∪ { { 3 , 5 } } ) ∪ ( { { 7 } } ∪ { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) )
22 4 5 21 3eqtr4i ⊢ 𝒫 { 3 , 5 , 7 } = ( ( { ∅ } ∪ { { 3 } , { 5 } , { 7 } } ) ∪ ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } ∪ { { 3 , 5 , 7 } } ) )
23 1 22 syl6eq ⊢ ( 𝐴 = { 3 , 5 , 7 } → 𝒫 𝐴 = ( ( { ∅ } ∪ { { 3 } , { 5 } , { 7 } } ) ∪ ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } ∪ { { 3 , 5 , 7 } } ) ) )