This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 bitrid ⊢ ( ( 𝐹 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 𝐴 ↔ 𝐹 = ( 𝑥 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑥 ) ) )