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 V tpos F V

Proof

Step Hyp Ref Expression
1 tposssxp tpos F dom F -1 × ran F
2 dmexg F V dom F V
3 cnvexg dom F V dom F -1 V
4 2 3 syl F V dom F -1 V
5 p0ex V
6 unexg dom F -1 V V dom F -1 V
7 4 5 6 sylancl F V dom F -1 V
8 rnexg F V ran F V
9 7 8 xpexd F V dom F -1 × ran F V
10 ssexg tpos F dom F -1 × ran F dom F -1 × ran F V tpos F V
11 1 9 10 sylancr F V tpos F V