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 Union First and second members of an ordered pair dmmpoga
Description: Domain of an operation given by the maps-to notation, closed form of
dmmpo . (Contributed by Alexander van der Vekens , 10-Feb-2019)
(Proof shortened by Lammen , 29-May-2024)
Ref
Expression
Hypothesis
dmmpog.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
Assertion
dmmpoga ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → dom 𝐹 = ( 𝐴 × 𝐵 ) )
Proof
Step
Hyp
Ref
Expression
1
dmmpog.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 )
2
1
fnmpo ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → 𝐹 Fn ( 𝐴 × 𝐵 ) )
3
2
fndmd ⊢ ( ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐵 𝐶 ∈ 𝑉 → dom 𝐹 = ( 𝐴 × 𝐵 ) )