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 
|- ( A = { 3 , 5 , 7 } -> ~P A = ( ( { (/) } u. { { 3 } , { 5 } , { 7 } } ) u. ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } u. { { 3 , 5 , 7 } } ) ) )

Proof

Step Hyp Ref Expression
1 pweq 
 |-  ( A = { 3 , 5 , 7 } -> ~P A = ~P { 3 , 5 , 7 } )
2 qdass 
 |-  ( { (/) , { 3 } } u. { { 5 } , { 3 , 5 } } ) = ( { (/) , { 3 } , { 5 } } u. { { 3 , 5 } } )
3 qdassr 
 |-  ( { { 7 } , { 3 , 7 } } u. { { 5 , 7 } , { 3 , 5 , 7 } } ) = ( { { 7 } } u. { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } )
4 2 3 uneq12i 
 |-  ( ( { (/) , { 3 } } u. { { 5 } , { 3 , 5 } } ) u. ( { { 7 } , { 3 , 7 } } u. { { 5 , 7 } , { 3 , 5 , 7 } } ) ) = ( ( { (/) , { 3 } , { 5 } } u. { { 3 , 5 } } ) u. ( { { 7 } } u. { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) )
5 pwtp 
 |-  ~P { 3 , 5 , 7 } = ( ( { (/) , { 3 } } u. { { 5 } , { 3 , 5 } } ) u. ( { { 7 } , { 3 , 7 } } u. { { 5 , 7 } , { 3 , 5 , 7 } } ) )
6 df-tp 
 |-  { { 3 } , { 5 } , { 7 } } = ( { { 3 } , { 5 } } u. { { 7 } } )
7 6 uneq2i 
 |-  ( { (/) } u. { { 3 } , { 5 } , { 7 } } ) = ( { (/) } u. ( { { 3 } , { 5 } } u. { { 7 } } ) )
8 unass 
 |-  ( ( { (/) } u. { { 3 } , { 5 } } ) u. { { 7 } } ) = ( { (/) } u. ( { { 3 } , { 5 } } u. { { 7 } } ) )
9 7 8 eqtr4i 
 |-  ( { (/) } u. { { 3 } , { 5 } , { 7 } } ) = ( ( { (/) } u. { { 3 } , { 5 } } ) u. { { 7 } } )
10 tpass 
 |-  { (/) , { 3 } , { 5 } } = ( { (/) } u. { { 3 } , { 5 } } )
11 10 uneq1i 
 |-  ( { (/) , { 3 } , { 5 } } u. { { 7 } } ) = ( ( { (/) } u. { { 3 } , { 5 } } ) u. { { 7 } } )
12 9 11 eqtr4i 
 |-  ( { (/) } u. { { 3 } , { 5 } , { 7 } } ) = ( { (/) , { 3 } , { 5 } } u. { { 7 } } )
13 unass 
 |-  ( ( { { 3 , 5 } } u. { { 3 , 7 } , { 5 , 7 } } ) u. { { 3 , 5 , 7 } } ) = ( { { 3 , 5 } } u. ( { { 3 , 7 } , { 5 , 7 } } u. { { 3 , 5 , 7 } } ) )
14 tpass 
 |-  { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } = ( { { 3 , 5 } } u. { { 3 , 7 } , { 5 , 7 } } )
15 14 uneq1i 
 |-  ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } u. { { 3 , 5 , 7 } } ) = ( ( { { 3 , 5 } } u. { { 3 , 7 } , { 5 , 7 } } ) u. { { 3 , 5 , 7 } } )
16 df-tp 
 |-  { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } = ( { { 3 , 7 } , { 5 , 7 } } u. { { 3 , 5 , 7 } } )
17 16 uneq2i 
 |-  ( { { 3 , 5 } } u. { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) = ( { { 3 , 5 } } u. ( { { 3 , 7 } , { 5 , 7 } } u. { { 3 , 5 , 7 } } ) )
18 13 15 17 3eqtr4i 
 |-  ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } u. { { 3 , 5 , 7 } } ) = ( { { 3 , 5 } } u. { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } )
19 12 18 uneq12i 
 |-  ( ( { (/) } u. { { 3 } , { 5 } , { 7 } } ) u. ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } u. { { 3 , 5 , 7 } } ) ) = ( ( { (/) , { 3 } , { 5 } } u. { { 7 } } ) u. ( { { 3 , 5 } } u. { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) )
20 un4 
 |-  ( ( { (/) , { 3 } , { 5 } } u. { { 3 , 5 } } ) u. ( { { 7 } } u. { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) ) = ( ( { (/) , { 3 } , { 5 } } u. { { 7 } } ) u. ( { { 3 , 5 } } u. { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) )
21 19 20 eqtr4i 
 |-  ( ( { (/) } u. { { 3 } , { 5 } , { 7 } } ) u. ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } u. { { 3 , 5 , 7 } } ) ) = ( ( { (/) , { 3 } , { 5 } } u. { { 3 , 5 } } ) u. ( { { 7 } } u. { { 3 , 7 } , { 5 , 7 } , { 3 , 5 , 7 } } ) )
22 4 5 21 3eqtr4i 
 |-  ~P { 3 , 5 , 7 } = ( ( { (/) } u. { { 3 } , { 5 } , { 7 } } ) u. ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } u. { { 3 , 5 , 7 } } ) )
23 1 22 syl6eq 
 |-  ( A = { 3 , 5 , 7 } -> ~P A = ( ( { (/) } u. { { 3 } , { 5 } , { 7 } } ) u. ( { { 3 , 5 } , { 3 , 7 } , { 5 , 7 } } u. { { 3 , 5 , 7 } } ) ) )