Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Function transposition
tposf
Next ⟩
tposfn
Metamath Proof Explorer
Ascii
Unicode
Theorem
tposf
Description:
The domain and range of a transposition.
(Contributed by
NM
, 10-Sep-2015)
Ref
Expression
Assertion
tposf
⊢
F
:
A
×
B
⟶
C
→
tpos
F
:
B
×
A
⟶
C
Proof
Step
Hyp
Ref
Expression
1
relxp
⊢
Rel
⁡
A
×
B
2
tposf2
⊢
Rel
⁡
A
×
B
→
F
:
A
×
B
⟶
C
→
tpos
F
:
A
×
B
-1
⟶
C
3
1
2
ax-mp
⊢
F
:
A
×
B
⟶
C
→
tpos
F
:
A
×
B
-1
⟶
C
4
cnvxp
⊢
A
×
B
-1
=
B
×
A
5
4
feq2i
⊢
tpos
F
:
A
×
B
-1
⟶
C
↔
tpos
F
:
B
×
A
⟶
C
6
3
5
sylib
⊢
F
:
A
×
B
⟶
C
→
tpos
F
:
B
×
A
⟶
C