Metamath Proof Explorer


Theorem tposf1o2

Description: Condition of a bijective transposition. (Contributed by NM, 10-Sep-2015)

Ref Expression
Assertion tposf1o2 Rel A F : A 1-1 onto B tpos F : A -1 1-1 onto B

Proof

Step Hyp Ref Expression
1 tposf12 Rel A F : A 1-1 B tpos F : A -1 1-1 B
2 tposfo2 Rel A F : A onto B tpos F : A -1 onto B
3 1 2 anim12d Rel A F : A 1-1 B F : A onto B tpos F : A -1 1-1 B tpos F : A -1 onto B
4 df-f1o F : A 1-1 onto B F : A 1-1 B F : A onto B
5 df-f1o tpos F : A -1 1-1 onto B tpos F : A -1 1-1 B tpos F : A -1 onto B
6 3 4 5 3imtr4g Rel A F : A 1-1 onto B tpos F : A -1 1-1 onto B