Metamath Proof Explorer


Theorem mpofun

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 𝐹

Proof

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 𝐹