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 \to F = \{⟨a, b⟩ \| ((a \in A \land b \in B) \land F (a) = b)\}$

Proof

Step	Hyp	Ref	Expression
1		fssxp	$⊢ F : A ⟶ B \to F \subseteq A \times B$
2		df-ss	$⊢ F \subseteq A \times B \leftrightarrow F \cap (A \times B) = F$
3	1 2	sylib	$⊢ F : A ⟶ B \to F \cap (A \times B) = F$
4		ffn	$⊢ F : A ⟶ B \to F Fn A$
5		dffn5	$⊢ F Fn A \leftrightarrow F = (a \in A ⟼ F (a))$
6	4 5	sylib	$⊢ F : A ⟶ B \to F = (a \in A ⟼ F (a))$
7	6	ineq1d	$⊢ F : A ⟶ B \to F \cap (A \times B) = (a \in A ⟼ F (a)) \cap (A \times B)$
8	3 7	eqtr3d	$⊢ F : A ⟶ B \to F = (a \in A ⟼ F (a)) \cap (A \times B)$
9		df-mpt	$⊢ (a \in A ⟼ F (a)) = \{⟨a, b⟩ \| (a \in A \land b = F (a))\}$
10		df-xp	$⊢ A \times B = \{⟨a, b⟩ \| (a \in A \land b \in B)\}$
11	9 10	ineq12i	$⊢ (a \in A ⟼ F (a)) \cap (A \times B) = \{⟨a, b⟩ \| (a \in A \land b = F (a))\} \cap \{⟨a, b⟩ \| (a \in A \land b \in B)\}$
12		inopab	$⊢ \{⟨a, b⟩ \| (a \in A \land b = F (a))\} \cap \{⟨a, b⟩ \| (a \in A \land b \in B)\} = \{⟨a, b⟩ \| ((a \in A \land b = F (a)) \land (a \in A \land b \in B))\}$
13		anandi	$⊢ (a \in A \land (b = F (a) \land b \in B)) \leftrightarrow ((a \in A \land b = F (a)) \land (a \in A \land b \in B))$
14		ancom	$⊢ (b = F (a) \land b \in B) \leftrightarrow (b \in B \land b = F (a))$
15	14	anbi2i	$⊢ (a \in A \land (b = F (a) \land b \in B)) \leftrightarrow (a \in A \land (b \in B \land b = F (a)))$
16		anass	$⊢ ((a \in A \land b \in B) \land b = F (a)) \leftrightarrow (a \in A \land (b \in B \land b = F (a)))$
17		eqcom	$⊢ b = F (a) \leftrightarrow F (a) = b$
18	17	anbi2i	$⊢ ((a \in A \land b \in B) \land b = F (a)) \leftrightarrow ((a \in A \land b \in B) \land F (a) = b)$
19	15 16 18	3bitr2i	$⊢ (a \in A \land (b = F (a) \land b \in B)) \leftrightarrow ((a \in A \land b \in B) \land F (a) = b)$
20	13 19	bitr3i	$⊢ ((a \in A \land b = F (a)) \land (a \in A \land b \in B)) \leftrightarrow ((a \in A \land b \in B) \land F (a) = b)$
21	20	opabbii	$⊢ \{⟨a, b⟩ \| ((a \in A \land b = F (a)) \land (a \in A \land b \in B))\} = \{⟨a, b⟩ \| ((a \in A \land b \in B) \land F (a) = b)\}$
22	11 12 21	3eqtri	$⊢ (a \in A ⟼ F (a)) \cap (A \times B) = \{⟨a, b⟩ \| ((a \in A \land b \in B) \land F (a) = b)\}$
23	8 22	eqtrdi	$⊢ F : A ⟶ B \to F = \{⟨a, b⟩ \| ((a \in A \land b \in B) \land F (a) = b)\}$

Metamath Proof Explorer

Theorem fgraphopab

Proof