Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Function transposition
tposexg
Next ⟩
ovtpos
Metamath Proof Explorer
Ascii
Unicode
Theorem
tposexg
Description:
The transposition of a set is a set.
(Contributed by
Mario Carneiro
, 10-Sep-2015)
Ref
Expression
Assertion
tposexg
⊢
F
∈
V
→
tpos
F
∈
V
Proof
Step
Hyp
Ref
Expression
1
tposssxp
⊢
tpos
F
⊆
dom
⁡
F
-1
∪
∅
×
ran
⁡
F
2
dmexg
⊢
F
∈
V
→
dom
⁡
F
∈
V
3
cnvexg
⊢
dom
⁡
F
∈
V
→
dom
⁡
F
-1
∈
V
4
2
3
syl
⊢
F
∈
V
→
dom
⁡
F
-1
∈
V
5
p0ex
⊢
∅
∈
V
6
unexg
⊢
dom
⁡
F
-1
∈
V
∧
∅
∈
V
→
dom
⁡
F
-1
∪
∅
∈
V
7
4
5
6
sylancl
⊢
F
∈
V
→
dom
⁡
F
-1
∪
∅
∈
V
8
rnexg
⊢
F
∈
V
→
ran
⁡
F
∈
V
9
7
8
xpexd
⊢
F
∈
V
→
dom
⁡
F
-1
∪
∅
×
ran
⁡
F
∈
V
10
ssexg
⊢
tpos
F
⊆
dom
⁡
F
-1
∪
∅
×
ran
⁡
F
∧
dom
⁡
F
-1
∪
∅
×
ran
⁡
F
∈
V
→
tpos
F
∈
V
11
1
9
10
sylancr
⊢
F
∈
V
→
tpos
F
∈
V