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 FVtposFV

Proof

Step Hyp Ref Expression
1 tposssxp tposFdomF-1×ranF
2 dmexg FVdomFV
3 cnvexg domFVdomF-1V
4 2 3 syl FVdomF-1V
5 p0ex V
6 unexg domF-1VVdomF-1V
7 4 5 6 sylancl FVdomF-1V
8 rnexg FVranFV
9 7 8 xpexd FVdomF-1×ranFV
10 ssexg tposFdomF-1×ranFdomF-1×ranFVtposFV
11 1 9 10 sylancr FVtposFV