Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Function transposition
tposfn2
Next ⟩
tposfo2
Metamath Proof Explorer
Ascii
Unicode
Theorem
tposfn2
Description:
The domain of a transposition.
(Contributed by
NM
, 10-Sep-2015)
Ref
Expression
Assertion
tposfn2
⊢
Rel
⁡
A
→
F
Fn
A
→
tpos
F
Fn
A
-1
Proof
Step
Hyp
Ref
Expression
1
tposfun
⊢
Fun
⁡
F
→
Fun
⁡
tpos
F
2
1
a1i
⊢
Rel
⁡
A
→
Fun
⁡
F
→
Fun
⁡
tpos
F
3
dmtpos
⊢
Rel
⁡
dom
⁡
F
→
dom
⁡
tpos
F
=
dom
⁡
F
-1
4
3
a1i
⊢
dom
⁡
F
=
A
→
Rel
⁡
dom
⁡
F
→
dom
⁡
tpos
F
=
dom
⁡
F
-1
5
releq
⊢
dom
⁡
F
=
A
→
Rel
⁡
dom
⁡
F
↔
Rel
⁡
A
6
cnveq
⊢
dom
⁡
F
=
A
→
dom
⁡
F
-1
=
A
-1
7
6
eqeq2d
⊢
dom
⁡
F
=
A
→
dom
⁡
tpos
F
=
dom
⁡
F
-1
↔
dom
⁡
tpos
F
=
A
-1
8
4
5
7
3imtr3d
⊢
dom
⁡
F
=
A
→
Rel
⁡
A
→
dom
⁡
tpos
F
=
A
-1
9
8
com12
⊢
Rel
⁡
A
→
dom
⁡
F
=
A
→
dom
⁡
tpos
F
=
A
-1
10
2
9
anim12d
⊢
Rel
⁡
A
→
Fun
⁡
F
∧
dom
⁡
F
=
A
→
Fun
⁡
tpos
F
∧
dom
⁡
tpos
F
=
A
-1
11
df-fn
⊢
F
Fn
A
↔
Fun
⁡
F
∧
dom
⁡
F
=
A
12
df-fn
⊢
tpos
F
Fn
A
-1
↔
Fun
⁡
tpos
F
∧
dom
⁡
tpos
F
=
A
-1
13
10
11
12
3imtr4g
⊢
Rel
⁡
A
→
F
Fn
A
→
tpos
F
Fn
A
-1