Description: Function value of an operator abstraction whose domain is a set of functions with given domain and range. (Contributed by Jeff Madsen, 1-Dec-2009) (Revised by Mario Carneiro, 12-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | fvopabf4g.1 | ⊢ 𝐶 ∈ V | |
| fvopabf4g.2 | ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) | ||
| fvopabf4g.3 | ⊢ 𝐹 = ( 𝑥 ∈ ( 𝑅 ↑m 𝐷 ) ↦ 𝐵 ) | ||
| Assertion | fvopabf4g | ⊢ ( ( 𝐷 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ∧ 𝐴 : 𝐷 ⟶ 𝑅 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | fvopabf4g.1 | ⊢ 𝐶 ∈ V | |
| 2 | fvopabf4g.2 | ⊢ ( 𝑥 = 𝐴 → 𝐵 = 𝐶 ) | |
| 3 | fvopabf4g.3 | ⊢ 𝐹 = ( 𝑥 ∈ ( 𝑅 ↑m 𝐷 ) ↦ 𝐵 ) | |
| 4 | elmapg | ⊢ ( ( 𝑅 ∈ 𝑌 ∧ 𝐷 ∈ 𝑋 ) → ( 𝐴 ∈ ( 𝑅 ↑m 𝐷 ) ↔ 𝐴 : 𝐷 ⟶ 𝑅 ) ) | |
| 5 | 4 | ancoms | ⊢ ( ( 𝐷 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ) → ( 𝐴 ∈ ( 𝑅 ↑m 𝐷 ) ↔ 𝐴 : 𝐷 ⟶ 𝑅 ) ) |
| 6 | 5 | biimp3ar | ⊢ ( ( 𝐷 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ∧ 𝐴 : 𝐷 ⟶ 𝑅 ) → 𝐴 ∈ ( 𝑅 ↑m 𝐷 ) ) |
| 7 | 2 3 1 | fvmpt | ⊢ ( 𝐴 ∈ ( 𝑅 ↑m 𝐷 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) |
| 8 | 6 7 | syl | ⊢ ( ( 𝐷 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌 ∧ 𝐴 : 𝐷 ⟶ 𝑅 ) → ( 𝐹 ‘ 𝐴 ) = 𝐶 ) |