Description: The class of functions with a given domain and a given codomain is mapped, through evaluation at a point of the domain, into the codomain. (Contributed by AV, 15-Sep-2024)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fsetfocdm.f | ⊢ 𝐹 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } | |
| fsetfocdm.s | ⊢ 𝑆 = ( 𝑔 ∈ 𝐹 ↦ ( 𝑔 ‘ 𝑋 ) ) | ||
| Assertion | fsetfcdm | ⊢ ( 𝑋 ∈ 𝐴 → 𝑆 : 𝐹 ⟶ 𝐵 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fsetfocdm.f | ⊢ 𝐹 = { 𝑓 ∣ 𝑓 : 𝐴 ⟶ 𝐵 } | |
| 2 | fsetfocdm.s | ⊢ 𝑆 = ( 𝑔 ∈ 𝐹 ↦ ( 𝑔 ‘ 𝑋 ) ) | |
| 3 | vex | ⊢ 𝑔 ∈ V | |
| 4 | feq1 | ⊢ ( 𝑓 = 𝑔 → ( 𝑓 : 𝐴 ⟶ 𝐵 ↔ 𝑔 : 𝐴 ⟶ 𝐵 ) ) | |
| 5 | 3 4 1 | elab2 | ⊢ ( 𝑔 ∈ 𝐹 ↔ 𝑔 : 𝐴 ⟶ 𝐵 ) |
| 6 | ffvelrn | ⊢ ( ( 𝑔 : 𝐴 ⟶ 𝐵 ∧ 𝑋 ∈ 𝐴 ) → ( 𝑔 ‘ 𝑋 ) ∈ 𝐵 ) | |
| 7 | 6 | expcom | ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑔 : 𝐴 ⟶ 𝐵 → ( 𝑔 ‘ 𝑋 ) ∈ 𝐵 ) ) |
| 8 | 5 7 | syl5bi | ⊢ ( 𝑋 ∈ 𝐴 → ( 𝑔 ∈ 𝐹 → ( 𝑔 ‘ 𝑋 ) ∈ 𝐵 ) ) |
| 9 | 8 | imp | ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑔 ∈ 𝐹 ) → ( 𝑔 ‘ 𝑋 ) ∈ 𝐵 ) |
| 10 | 9 2 | fmptd | ⊢ ( 𝑋 ∈ 𝐴 → 𝑆 : 𝐹 ⟶ 𝐵 ) |