fncnv

Description: Single-rootedness (see funcnv ) of a class cut down by a Cartesian product. (Contributed by NM, 5-Mar-2007)

		Ref	Expression
	Assertion	fncnv	$⊢ {(R \cap (A \times B))}^{-1} Fn B \leftrightarrow \forall y \in B \exists! x \in A x R y$

Proof

Step	Hyp	Ref	Expression
1		df-fn	$⊢ {(R \cap (A \times B))}^{-1} Fn B \leftrightarrow (Fun {(R \cap (A \times B))}^{-1} \land dom {(R \cap (A \times B))}^{-1} = B)$
2		df-rn	$⊢ ran (R \cap (A \times B)) = dom {(R \cap (A \times B))}^{-1}$
3	2	eqeq1i	$⊢ ran (R \cap (A \times B)) = B \leftrightarrow dom {(R \cap (A \times B))}^{-1} = B$
4	3	anbi2i	$⊢ (Fun {(R \cap (A \times B))}^{-1} \land ran (R \cap (A \times B)) = B) \leftrightarrow (Fun {(R \cap (A \times B))}^{-1} \land dom {(R \cap (A \times B))}^{-1} = B)$
5		rninxp	$⊢ ran (R \cap (A \times B)) = B \leftrightarrow \forall y \in B \exists x \in A x R y$
6	5	anbi1i	$⊢ (ran (R \cap (A \times B)) = B \land \forall y \in B \exists^{} x \in A x R y) \leftrightarrow (\forall y \in B \exists x \in A x R y \land \forall y \in B \exists^{} x \in A x R y)$
7		funcnv	$⊢ Fun {(R \cap (A \times B))}^{-1} \leftrightarrow \forall y \in ran (R \cap (A \times B)) \exists^{*} x x (R \cap (A \times B)) y$
8		raleq	$⊢ ran (R \cap (A \times B)) = B \to (\forall y \in ran (R \cap (A \times B)) \exists^{} x x (R \cap (A \times B)) y \leftrightarrow \forall y \in B \exists^{} x x (R \cap (A \times B)) y)$
9		moanimv	$⊢ \exists^{} x (y \in B \land (x \in A \land x R y)) \leftrightarrow (y \in B \to \exists^{} x (x \in A \land x R y))$
10		brinxp2	$⊢ x (R \cap (A \times B)) y \leftrightarrow ((x \in A \land y \in B) \land x R y)$
11		an21	$⊢ ((x \in A \land y \in B) \land x R y) \leftrightarrow (y \in B \land (x \in A \land x R y))$
12	10 11	bitri	$⊢ x (R \cap (A \times B)) y \leftrightarrow (y \in B \land (x \in A \land x R y))$
13	12	mobii	$⊢ \exists^{} x x (R \cap (A \times B)) y \leftrightarrow \exists^{} x (y \in B \land (x \in A \land x R y))$
14		df-rmo	$⊢ \exists^{} x \in A x R y \leftrightarrow \exists^{} x (x \in A \land x R y)$
15	14	imbi2i	$⊢ (y \in B \to \exists^{} x \in A x R y) \leftrightarrow (y \in B \to \exists^{} x (x \in A \land x R y))$
16	9 13 15	3bitr4i	$⊢ \exists^{} x x (R \cap (A \times B)) y \leftrightarrow (y \in B \to \exists^{} x \in A x R y)$
17		biimt	$⊢ y \in B \to (\exists^{} x \in A x R y \leftrightarrow (y \in B \to \exists^{} x \in A x R y))$
18	16 17	bitr4id	$⊢ y \in B \to (\exists^{} x x (R \cap (A \times B)) y \leftrightarrow \exists^{} x \in A x R y)$
19	18	ralbiia	$⊢ \forall y \in B \exists^{} x x (R \cap (A \times B)) y \leftrightarrow \forall y \in B \exists^{} x \in A x R y$
20	8 19	bitrdi	$⊢ ran (R \cap (A \times B)) = B \to (\forall y \in ran (R \cap (A \times B)) \exists^{} x x (R \cap (A \times B)) y \leftrightarrow \forall y \in B \exists^{} x \in A x R y)$
21	7 20	bitrid	$⊢ ran (R \cap (A \times B)) = B \to (Fun {(R \cap (A \times B))}^{-1} \leftrightarrow \forall y \in B \exists^{*} x \in A x R y)$
22	21	pm5.32i	$⊢ (ran (R \cap (A \times B)) = B \land Fun {(R \cap (A \times B))}^{-1}) \leftrightarrow (ran (R \cap (A \times B)) = B \land \forall y \in B \exists^{*} x \in A x R y)$
23		r19.26	$⊢ \forall y \in B (\exists x \in A x R y \land \exists^{} x \in A x R y) \leftrightarrow (\forall y \in B \exists x \in A x R y \land \forall y \in B \exists^{} x \in A x R y)$
24	6 22 23	3bitr4i	$⊢ (ran (R \cap (A \times B)) = B \land Fun {(R \cap (A \times B))}^{-1}) \leftrightarrow \forall y \in B (\exists x \in A x R y \land \exists^{*} x \in A x R y)$
25		ancom	$⊢ (Fun {(R \cap (A \times B))}^{-1} \land ran (R \cap (A \times B)) = B) \leftrightarrow (ran (R \cap (A \times B)) = B \land Fun {(R \cap (A \times B))}^{-1})$
26		reu5	$⊢ \exists! x \in A x R y \leftrightarrow (\exists x \in A x R y \land \exists^{*} x \in A x R y)$
27	26	ralbii	$⊢ \forall y \in B \exists! x \in A x R y \leftrightarrow \forall y \in B (\exists x \in A x R y \land \exists^{*} x \in A x R y)$
28	24 25 27	3bitr4i	$⊢ (Fun {(R \cap (A \times B))}^{-1} \land ran (R \cap (A \times B)) = B) \leftrightarrow \forall y \in B \exists! x \in A x R y$
29	1 4 28	3bitr2i	$⊢ {(R \cap (A \times B))}^{-1} Fn B \leftrightarrow \forall y \in B \exists! x \in A x R y$

Metamath Proof Explorer

Theorem fncnv

Proof