Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Function transposition
tposf1o2
Next ⟩
tposfo
Metamath Proof Explorer
Ascii
Unicode
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