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