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 ⊢ F : A ⟶ B → F = a b | a ∈ A ∧ b ∈ B ∧ F ⁡ a = b

Proof

Step Hyp Ref Expression
1 fssxp ⊢ F : A ⟶ B → F ⊆ A × B
2 df-ss ⊢ F ⊆ A × B ↔ F ∩ A × B = F
3 1 2 sylib ⊢ F : A ⟶ B → F ∩ A × B = F
4 ffn ⊢ F : A ⟶ B → F Fn A
5 dffn5 ⊢ F Fn A ↔ F = a ∈ A ⟼ F ⁡ a
6 4 5 sylib ⊢ F : A ⟶ B → F = a ∈ A ⟼ F ⁡ a
7 6 ineq1d ⊢ F : A ⟶ B → F ∩ A × B = a ∈ A ⟼ F ⁡ a ∩ A × B
8 3 7 eqtr3d ⊢ F : A ⟶ B → F = a ∈ A ⟼ F ⁡ a ∩ A × B
9 df-mpt ⊢ a ∈ A ⟼ F ⁡ a = a b | a ∈ A ∧ b = F ⁡ a
10 df-xp ⊢ A × B = a b | a ∈ A ∧ b ∈ B
11 9 10 ineq12i ⊢ a ∈ A ⟼ F ⁡ a ∩ A × B = a b | a ∈ A ∧ b = F ⁡ a ∩ a b | a ∈ A ∧ b ∈ B
12 inopab ⊢ a b | a ∈ A ∧ b = F ⁡ a ∩ a b | a ∈ A ∧ b ∈ B = a b | a ∈ A ∧ b = F ⁡ a ∧ a ∈ A ∧ b ∈ B
13 anandi ⊢ a ∈ A ∧ b = F ⁡ a ∧ b ∈ B ↔ a ∈ A ∧ b = F ⁡ a ∧ a ∈ A ∧ b ∈ B
14 ancom ⊢ b = F ⁡ a ∧ b ∈ B ↔ b ∈ B ∧ b = F ⁡ a
15 14 anbi2i ⊢ a ∈ A ∧ b = F ⁡ a ∧ b ∈ B ↔ a ∈ A ∧ b ∈ B ∧ b = F ⁡ a
16 anass ⊢ a ∈ A ∧ b ∈ B ∧ b = F ⁡ a ↔ a ∈ A ∧ b ∈ B ∧ b = F ⁡ a
17 eqcom ⊢ b = F ⁡ a ↔ F ⁡ a = b
18 17 anbi2i ⊢ a ∈ A ∧ b ∈ B ∧ b = F ⁡ a ↔ a ∈ A ∧ b ∈ B ∧ F ⁡ a = b
19 15 16 18 3bitr2i ⊢ a ∈ A ∧ b = F ⁡ a ∧ b ∈ B ↔ a ∈ A ∧ b ∈ B ∧ F ⁡ a = b
20 13 19 bitr3i ⊢ a ∈ A ∧ b = F ⁡ a ∧ a ∈ A ∧ b ∈ B ↔ a ∈ A ∧ b ∈ B ∧ F ⁡ a = b
21 20 opabbii ⊢ a b | a ∈ A ∧ b = F ⁡ a ∧ a ∈ A ∧ b ∈ B = a b | a ∈ A ∧ b ∈ B ∧ F ⁡ a = b
22 11 12 21 3eqtri ⊢ a ∈ A ⟼ F ⁡ a ∩ A × B = a b | a ∈ A ∧ b ∈ B ∧ F ⁡ a = b
23 8 22 eqtrdi ⊢ F : A ⟶ B → F = a b | a ∈ A ∧ b ∈ B ∧ F ⁡ a = b