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 eqtrdi ( 𝐴 = { 3 , 5 , 7 } → 𝒫 𝐴 = ( ( { ∅ } ∪ { { 3 } , { 5 } , { 7 } } ) ∪ ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } ∪ { { 3 , 5 , 7 } } ) ) )