exfo

Description: A relation equivalent to the existence of an onto mapping. The right-hand f is not necessarily a function. (Contributed by NM, 20-Mar-2007)

		Ref	Expression
	Assertion	exfo	$⊢ \exists f f : A \underset{onto}{⟶} B \leftrightarrow \exists f (\forall x \in A \exists! y \in B x f y \land \forall x \in B \exists y \in A y f x)$

Proof

Step	Hyp	Ref	Expression
1		dffo4	$⊢ f : A \underset{onto}{⟶} B \leftrightarrow (f : A ⟶ B \land \forall x \in B \exists y \in A y f x)$
2		dff4	$⊢ f : A ⟶ B \leftrightarrow (f \subseteq A \times B \land \forall x \in A \exists! y \in B x f y)$
3	2	simprbi	$⊢ f : A ⟶ B \to \forall x \in A \exists! y \in B x f y$
4	3	anim1i	$⊢ (f : A ⟶ B \land \forall x \in B \exists y \in A y f x) \to (\forall x \in A \exists! y \in B x f y \land \forall x \in B \exists y \in A y f x)$
5	1 4	sylbi	$⊢ f : A \underset{onto}{⟶} B \to (\forall x \in A \exists! y \in B x f y \land \forall x \in B \exists y \in A y f x)$
6	5	eximi	$⊢ \exists f f : A \underset{onto}{⟶} B \to \exists f (\forall x \in A \exists! y \in B x f y \land \forall x \in B \exists y \in A y f x)$
7		brinxp	$⊢ (x \in A \land y \in B) \to (x f y \leftrightarrow x (f \cap (A \times B)) y)$
8	7	reubidva	$⊢ x \in A \to (\exists! y \in B x f y \leftrightarrow \exists! y \in B x (f \cap (A \times B)) y)$
9	8	biimpd	$⊢ x \in A \to (\exists! y \in B x f y \to \exists! y \in B x (f \cap (A \times B)) y)$
10	9	ralimia	$⊢ \forall x \in A \exists! y \in B x f y \to \forall x \in A \exists! y \in B x (f \cap (A \times B)) y$
11		inss2	$⊢ f \cap (A \times B) \subseteq A \times B$
12	10 11	jctil	$⊢ \forall x \in A \exists! y \in B x f y \to (f \cap (A \times B) \subseteq A \times B \land \forall x \in A \exists! y \in B x (f \cap (A \times B)) y)$
13		dff4	$⊢ (f \cap (A \times B)) : A ⟶ B \leftrightarrow (f \cap (A \times B) \subseteq A \times B \land \forall x \in A \exists! y \in B x (f \cap (A \times B)) y)$
14	12 13	sylibr	$⊢ \forall x \in A \exists! y \in B x f y \to (f \cap (A \times B)) : A ⟶ B$
15		rninxp	$⊢ ran (f \cap (A \times B)) = B \leftrightarrow \forall x \in B \exists y \in A y f x$
16	15	biimpri	$⊢ \forall x \in B \exists y \in A y f x \to ran (f \cap (A \times B)) = B$
17	14 16	anim12i	$⊢ (\forall x \in A \exists! y \in B x f y \land \forall x \in B \exists y \in A y f x) \to ((f \cap (A \times B)) : A ⟶ B \land ran (f \cap (A \times B)) = B)$
18		dffo2	$⊢ (f \cap (A \times B)) : A \underset{onto}{⟶} B \leftrightarrow ((f \cap (A \times B)) : A ⟶ B \land ran (f \cap (A \times B)) = B)$
19	17 18	sylibr	$⊢ (\forall x \in A \exists! y \in B x f y \land \forall x \in B \exists y \in A y f x) \to (f \cap (A \times B)) : A \underset{onto}{⟶} B$
20		vex	$⊢ f \in V$
21	20	inex1	$⊢ f \cap (A \times B) \in V$
22		foeq1	$⊢ g = f \cap (A \times B) \to (g : A \underset{onto}{⟶} B \leftrightarrow (f \cap (A \times B)) : A \underset{onto}{⟶} B)$
23	21 22	spcev	$⊢ (f \cap (A \times B)) : A \underset{onto}{⟶} B \to \exists g g : A \underset{onto}{⟶} B$
24	19 23	syl	$⊢ (\forall x \in A \exists! y \in B x f y \land \forall x \in B \exists y \in A y f x) \to \exists g g : A \underset{onto}{⟶} B$
25	24	exlimiv	$⊢ \exists f (\forall x \in A \exists! y \in B x f y \land \forall x \in B \exists y \in A y f x) \to \exists g g : A \underset{onto}{⟶} B$
26		foeq1	$⊢ g = f \to (g : A \underset{onto}{⟶} B \leftrightarrow f : A \underset{onto}{⟶} B)$
27	26	cbvexvw	$⊢ \exists g g : A \underset{onto}{⟶} B \leftrightarrow \exists f f : A \underset{onto}{⟶} B$
28	25 27	sylib	$⊢ \exists f (\forall x \in A \exists! y \in B x f y \land \forall x \in B \exists y \in A y f x) \to \exists f f : A \underset{onto}{⟶} B$
29	6 28	impbii	$⊢ \exists f f : A \underset{onto}{⟶} B \leftrightarrow \exists f (\forall x \in A \exists! y \in B x f y \land \forall x \in B \exists y \in A y f x)$

Metamath Proof Explorer

Theorem exfo

Proof