Metamath Proof Explorer

Theorem pmtrsn

Description: The value of the transposition generator function for a singleton is empty, i.e. there is no transposition for a singleton. This also holds for A e/ _V , i.e. for the empty set { A } = (/) resulting in ( pmTrsp(/) ) = (/) . (Contributed by AV, 6-Aug-2019)

Ref Expression
Assertion pmtrsn 
|- ( pmTrsp ` { A } ) = (/)

Proof

Step Hyp Ref Expression
1 snex 
 |-  { A } e. _V
2 eqid 
 |-  ( pmTrsp ` { A } ) = ( pmTrsp ` { A } )
3 2 pmtrfval 
 |-  ( { A } e. _V -> ( pmTrsp ` { A } ) = ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) )
4 1 3 ax-mp 
 |-  ( pmTrsp ` { A } ) = ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
5 eqid 
 |-  ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
6 5 dmmpt 
 |-  dom ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = { p e. { y e. ~P { A } | y ~~ 2o } | ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) e. _V }
7 2on0 
 |-  2o =/= (/)
8 ensymb 
 |-  ( (/) ~~ 2o <-> 2o ~~ (/) )
9 en0 
 |-  ( 2o ~~ (/) <-> 2o = (/) )
10 8 9 bitri 
 |-  ( (/) ~~ 2o <-> 2o = (/) )
11 7 10 nemtbir 
 |-  -. (/) ~~ 2o
12 snnen2o 
 |-  -. { A } ~~ 2o
13 0ex 
 |-  (/) e. _V
14 breq1 
 |-  ( y = (/) -> ( y ~~ 2o <-> (/) ~~ 2o ) )
15 14 notbid 
 |-  ( y = (/) -> ( -. y ~~ 2o <-> -. (/) ~~ 2o ) )
16 breq1 
 |-  ( y = { A } -> ( y ~~ 2o <-> { A } ~~ 2o ) )
17 16 notbid 
 |-  ( y = { A } -> ( -. y ~~ 2o <-> -. { A } ~~ 2o ) )
18 13 1 15 17 ralpr 
 |-  ( A. y e. { (/) , { A } } -. y ~~ 2o <-> ( -. (/) ~~ 2o /\ -. { A } ~~ 2o ) )
19 11 12 18 mpbir2an 
 |-  A. y e. { (/) , { A } } -. y ~~ 2o
20 pwsn 
 |-  ~P { A } = { (/) , { A } }
21 20 raleqi 
 |-  ( A. y e. ~P { A } -. y ~~ 2o <-> A. y e. { (/) , { A } } -. y ~~ 2o )
22 19 21 mpbir 
 |-  A. y e. ~P { A } -. y ~~ 2o
23 rabeq0 
 |-  ( { y e. ~P { A } | y ~~ 2o } = (/) <-> A. y e. ~P { A } -. y ~~ 2o )
24 22 23 mpbir 
 |-  { y e. ~P { A } | y ~~ 2o } = (/)
25 24 rabeqi 
 |-  { p e. { y e. ~P { A } | y ~~ 2o } | ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) e. _V } = { p e. (/) | ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) e. _V }
26 rab0 
 |-  { p e. (/) | ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) e. _V } = (/)
27 6 25 26 3eqtri 
 |-  dom ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = (/)
28 mptrel 
 |-  Rel ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) )
29 reldm0 
 |-  ( Rel ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) -> ( ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = (/) <-> dom ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = (/) ) )
30 28 29 ax-mp 
 |-  ( ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = (/) <-> dom ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = (/) )
31 27 30 mpbir 
 |-  ( p e. { y e. ~P { A } | y ~~ 2o } |-> ( z e. { A } |-> if ( z e. p , U. ( p \ { z } ) , z ) ) ) = (/)
32 4 31 eqtri 
 |-  ( pmTrsp ` { A } ) = (/)