Description: The maps-to notation for an operation is always a function. (Contributed by Scott Fenton, 21-Mar-2012) (Proof shortened by SN, 23-Jul-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | mpofun.1 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) | |
Assertion | mpofun | ⊢ Fun 𝐹 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mpofun.1 | ⊢ 𝐹 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) | |
2 | moeq | ⊢ ∃* 𝑧 𝑧 = 𝐶 | |
3 | 2 | moani | ⊢ ∃* 𝑧 ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) |
4 | 3 | funoprab | ⊢ Fun { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } |
5 | df-mpo | ⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } | |
6 | 1 5 | eqtri | ⊢ 𝐹 = { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } |
7 | 6 | funeqi | ⊢ ( Fun 𝐹 ↔ Fun { 〈 〈 𝑥 , 𝑦 〉 , 𝑧 〉 ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } ) |
8 | 4 7 | mpbir | ⊢ Fun 𝐹 |