Description: Function value for a member of a set exponentiation. (Contributed by Glauco Siliprandi, 21-Nov-2020)
Ref | Expression | ||
---|---|---|---|
Hypotheses | fvmap.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | |
fvmap.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) | ||
fvmap.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) ) | ||
fvmap.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 ) | ||
Assertion | fvmap | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ 𝐴 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | fvmap.a | ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) | |
2 | fvmap.b | ⊢ ( 𝜑 → 𝐵 ∈ 𝑊 ) | |
3 | fvmap.f | ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) ) | |
4 | fvmap.c | ⊢ ( 𝜑 → 𝐶 ∈ 𝐵 ) | |
5 | id | ⊢ ( 𝜑 → 𝜑 ) | |
6 | elmapg | ⊢ ( ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝐹 : 𝐵 ⟶ 𝐴 ) ) | |
7 | 1 2 6 | syl2anc | ⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐴 ↑m 𝐵 ) ↔ 𝐹 : 𝐵 ⟶ 𝐴 ) ) |
8 | 3 7 | mpbid | ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ 𝐴 ) |
9 | 8 | ffvelrnda | ⊢ ( ( 𝜑 ∧ 𝐶 ∈ 𝐵 ) → ( 𝐹 ‘ 𝐶 ) ∈ 𝐴 ) |
10 | 5 4 9 | syl2anc | ⊢ ( 𝜑 → ( 𝐹 ‘ 𝐶 ) ∈ 𝐴 ) |