This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database ZF (ZERMELO-FRAENKEL) SET THEORY ZF Set Theory - add the Axiom of Power Sets Functions mptexgf
Description: If the domain of a function given by maps-to notation is a set, the
function is a set. (Contributed by FL , 6-Jun-2011) (Revised by Mario
Carneiro , 31-Aug-2015) (Revised by Thierry Arnoux , 17-May-2020)
Ref
Expression
Hypothesis
mptexgf.a ⊢ Ⅎ _ x A
Assertion
mptexgf ⊢ A ∈ V → x ∈ A ⟼ B ∈ V
Proof
Step
Hyp
Ref
Expression
1
mptexgf.a ⊢ Ⅎ _ x A
2
funmpt ⊢ Fun x ∈ A ⟼ B
3
eqid ⊢ x ∈ A ⟼ B = x ∈ A ⟼ B
4
3
dmmpt ⊢ dom x ∈ A ⟼ B = x ∈ A | B ∈ V
5
tru ⊢ ⊤
6
5
2a1i ⊢ x ∈ A → B ∈ V → ⊤
7
6
ss2rabi ⊢ x ∈ A | B ∈ V ⊆ x ∈ A | ⊤
8
1
rabtru ⊢ x ∈ A | ⊤ = A
9
7 8
sseqtri ⊢ x ∈ A | B ∈ V ⊆ A
10
4 9
eqsstri ⊢ dom x ∈ A ⟼ B ⊆ A
11
ssexg ⊢ dom x ∈ A ⟼ B ⊆ A ∧ A ∈ V → dom x ∈ A ⟼ B ∈ V
12
10 11
mpan ⊢ A ∈ V → dom x ∈ A ⟼ B ∈ V
13
funex ⊢ Fun x ∈ A ⟼ B ∧ dom x ∈ A ⟼ B ∈ V → x ∈ A ⟼ B ∈ V
14
2 12 13
sylancr ⊢ A ∈ V → x ∈ A ⟼ B ∈ V