Metamath Proof Explorer
Description: Functionality and domain of an ordered-pair class abstraction.
(Contributed by Glauco Siliprandi, 21-Dec-2024)
|
|
Ref |
Expression |
|
Hypotheses |
fnmptif.1 |
⊢ Ⅎ 𝑥 𝐴 |
|
|
fnmptif.2 |
⊢ 𝐵 ∈ V |
|
|
fnmptif.3 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
|
Assertion |
fnmptif |
⊢ 𝐹 Fn 𝐴 |
Proof
Step |
Hyp |
Ref |
Expression |
1 |
|
fnmptif.1 |
⊢ Ⅎ 𝑥 𝐴 |
2 |
|
fnmptif.2 |
⊢ 𝐵 ∈ V |
3 |
|
fnmptif.3 |
⊢ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) |
4 |
2
|
rgenw |
⊢ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V |
5 |
1
|
mptfnf |
⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ) |
6 |
4 5
|
mpbi |
⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 |
7 |
3
|
fneq1i |
⊢ ( 𝐹 Fn 𝐴 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) Fn 𝐴 ) |
8 |
6 7
|
mpbir |
⊢ 𝐹 Fn 𝐴 |