Metamath Proof Explorer


Theorem tposf2

Description: The domain and range of a transposition. (Contributed by NM, 10-Sep-2015)

Ref Expression
Assertion tposf2 Rel A F : A B tpos F : A -1 B

Proof

Step Hyp Ref Expression
1 tposfo2 Rel A F : A onto ran F tpos F : A -1 onto ran F
2 ffn F : A B F Fn A
3 dffn4 F Fn A F : A onto ran F
4 2 3 sylib F : A B F : A onto ran F
5 1 4 impel Rel A F : A B tpos F : A -1 onto ran F
6 fof tpos F : A -1 onto ran F tpos F : A -1 ran F
7 5 6 syl Rel A F : A B tpos F : A -1 ran F
8 frn F : A B ran F B
9 8 adantl Rel A F : A B ran F B
10 7 9 fssd Rel A F : A B tpos F : A -1 B
11 10 ex Rel A F : A B tpos F : A -1 B