Metamath Proof Explorer

Theorem fgraphopab

Description: Express a function as a subset of the Cartesian product. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Assertion fgraphopab ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) } )

Proof

Step Hyp Ref Expression
1 fssxp ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 ⊆ ( 𝐴 × 𝐵 ) )
2 dfss2 ⊢ ( 𝐹 ⊆ ( 𝐴 × 𝐵 ) ↔ ( 𝐹 ∩ ( 𝐴 × 𝐵 ) ) = 𝐹 )
3 1 2 sylib ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ∩ ( 𝐴 × 𝐵 ) ) = 𝐹 )
4 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
5 dffn5 ⊢ ( 𝐹 Fn 𝐴 ↔ 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) )
6 4 5 sylib ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) )
7 6 ineq1d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → ( 𝐹 ∩ ( 𝐴 × 𝐵 ) ) = ( ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) ∩ ( 𝐴 × 𝐵 ) ) )
8 3 7 eqtr3d ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = ( ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) ∩ ( 𝐴 × 𝐵 ) ) )
9 df-mpt ⊢ ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ 𝐴 ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) }
10 df-xp ⊢ ( 𝐴 × 𝐵 ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) }
11 9 10 ineq12i ⊢ ( ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) ∩ ( 𝐴 × 𝐵 ) ) = ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ 𝐴 ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) } ∩ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) } )
12 inopab ⊢ ( { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ 𝐴 ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) } ∩ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) } ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) }
13 anandi ⊢ ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑏 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑏 ∈ 𝐵 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) )
14 ancom ⊢ ( ( 𝑏 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑏 ∈ 𝐵 ) ↔ ( 𝑏 ∈ 𝐵 ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) )
15 14 anbi2i ⊢ ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑏 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑏 ∈ 𝐵 ) ) ↔ ( 𝑎 ∈ 𝐴 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) ) )
16 anass ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) ↔ ( 𝑎 ∈ 𝐴 ∧ ( 𝑏 ∈ 𝐵 ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) ) )
17 eqcom ⊢ ( 𝑏 = ( 𝐹 ‘ 𝑎 ) ↔ ( 𝐹 ‘ 𝑎 ) = 𝑏 )
18 17 anbi2i ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) )
19 15 16 18 3bitr2i ⊢ ( ( 𝑎 ∈ 𝐴 ∧ ( 𝑏 = ( 𝐹 ‘ 𝑎 ) ∧ 𝑏 ∈ 𝐵 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) )
20 13 19 bitr3i ⊢ ( ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) ↔ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) )
21 20 opabbii ⊢ { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 = ( 𝐹 ‘ 𝑎 ) ) ∧ ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ) } = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) }
22 11 12 21 3eqtri ⊢ ( ( 𝑎 ∈ 𝐴 ↦ ( 𝐹 ‘ 𝑎 ) ) ∩ ( 𝐴 × 𝐵 ) ) = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) }
23 8 22 eqtrdi ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 = { ⟨ 𝑎 , 𝑏 ⟩ ∣ ( ( 𝑎 ∈ 𝐴 ∧ 𝑏 ∈ 𝐵 ) ∧ ( 𝐹 ‘ 𝑎 ) = 𝑏 ) } )