Database
ZF (ZERMELO-FRAENKEL) SET THEORY
ZF Set Theory - add the Axiom of Union
Relations and functions (cont.)
mptexw
Metamath Proof Explorer
Description: Weak version of mptex that holds without ax-rep . If the domain and
codomain of a function given by maps-to notation are sets, the function
is a set. (Contributed by Rohan Ridenour , 13-Aug-2023)
Ref
Expression
Hypotheses
mptexw.1
⊢ 𝐴 ∈ V
mptexw.2
⊢ 𝐶 ∈ V
mptexw.3
⊢ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶
Assertion
mptexw
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V
Proof
Step
Hyp
Ref
Expression
1
mptexw.1
⊢ 𝐴 ∈ V
2
mptexw.2
⊢ 𝐶 ∈ V
3
mptexw.3
⊢ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶
4
funmpt
⊢ Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
5
eqid
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6
5
dmmptss
⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐴
7
1 6
ssexi
⊢ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V
8
5
rnmptss
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐶 → ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐶 )
9
3 8
ax-mp
⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ⊆ 𝐶
10
2 9
ssexi
⊢ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V
11
funexw
⊢ ( ( Fun ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∧ dom ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ∧ ran ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
12
4 7 10 11
mp3an
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V