This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem tposexg

Description: The transposition of a set is a set. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion tposexg 
|- ( F e. V -> tpos F e. _V )

Proof

Step Hyp Ref Expression
1 tposssxp 
 |-  tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F )
2 dmexg 
 |-  ( F e. V -> dom F e. _V )
3 cnvexg 
 |-  ( dom F e. _V -> `' dom F e. _V )
4 2 3 syl 
 |-  ( F e. V -> `' dom F e. _V )
5 p0ex 
 |-  { (/) } e. _V
6 unexg 
 |-  ( ( `' dom F e. _V /\ { (/) } e. _V ) -> ( `' dom F u. { (/) } ) e. _V )
7 4 5 6 sylancl 
 |-  ( F e. V -> ( `' dom F u. { (/) } ) e. _V )
8 rnexg 
 |-  ( F e. V -> ran F e. _V )
9 7 8 xpexd 
 |-  ( F e. V -> ( ( `' dom F u. { (/) } ) X. ran F ) e. _V )
10 ssexg 
 |-  ( ( tpos F C_ ( ( `' dom F u. { (/) } ) X. ran F ) /\ ( ( `' dom F u. { (/) } ) X. ran F ) e. _V ) -> tpos F e. _V )
11 1 9 10 sylancr 
 |-  ( F e. V -> tpos F e. _V )