Metamath Proof Explorer


Theorem dffn5

Description: Representation of a function in terms of its values. (Contributed by FL, 14-Sep-2013) (Proof shortened by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion dffn5 ( 𝐹 Fn 𝐴𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 fnrel ( 𝐹 Fn 𝐴 → Rel 𝐹 )
2 dfrel4v ( Rel 𝐹𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝐹 𝑦 } )
3 1 2 sylib ( 𝐹 Fn 𝐴𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝐹 𝑦 } )
4 fnbr ( ( 𝐹 Fn 𝐴𝑥 𝐹 𝑦 ) → 𝑥𝐴 )
5 4 ex ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑦𝑥𝐴 ) )
6 5 pm4.71rd ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥𝐴𝑥 𝐹 𝑦 ) ) )
7 eqcom ( 𝑦 = ( 𝐹𝑥 ) ↔ ( 𝐹𝑥 ) = 𝑦 )
8 fnbrfvb ( ( 𝐹 Fn 𝐴𝑥𝐴 ) → ( ( 𝐹𝑥 ) = 𝑦𝑥 𝐹 𝑦 ) )
9 7 8 syl5bb ( ( 𝐹 Fn 𝐴𝑥𝐴 ) → ( 𝑦 = ( 𝐹𝑥 ) ↔ 𝑥 𝐹 𝑦 ) )
10 9 pm5.32da ( 𝐹 Fn 𝐴 → ( ( 𝑥𝐴𝑦 = ( 𝐹𝑥 ) ) ↔ ( 𝑥𝐴𝑥 𝐹 𝑦 ) ) )
11 6 10 bitr4d ( 𝐹 Fn 𝐴 → ( 𝑥 𝐹 𝑦 ↔ ( 𝑥𝐴𝑦 = ( 𝐹𝑥 ) ) ) )
12 11 opabbidv ( 𝐹 Fn 𝐴 → { ⟨ 𝑥 , 𝑦 ⟩ ∣ 𝑥 𝐹 𝑦 } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = ( 𝐹𝑥 ) ) } )
13 3 12 eqtrd ( 𝐹 Fn 𝐴𝐹 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = ( 𝐹𝑥 ) ) } )
14 df-mpt ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝑥𝐴𝑦 = ( 𝐹𝑥 ) ) }
15 13 14 eqtr4di ( 𝐹 Fn 𝐴𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) )
16 fvex ( 𝐹𝑥 ) ∈ V
17 eqid ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) )
18 16 17 fnmpti ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) Fn 𝐴
19 fneq1 ( 𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) → ( 𝐹 Fn 𝐴 ↔ ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) Fn 𝐴 ) )
20 18 19 mpbiri ( 𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) → 𝐹 Fn 𝐴 )
21 15 20 impbii ( 𝐹 Fn 𝐴𝐹 = ( 𝑥𝐴 ↦ ( 𝐹𝑥 ) ) )