brdom4

Description: An equivalence to a dominance relation. (Contributed by NM, 28-Mar-2007) (Revised by NM, 16-Jun-2017)

		Ref	Expression
	Hypothesis	brdom3.2	$⊢ B \in V$
	Assertion	brdom4	$⊢ A ≼ B \leftrightarrow \exists f (\forall x \in B \exists^{*} y \in A x f y \land \forall x \in A \exists y \in B y f x)$

Proof

Step	Hyp	Ref	Expression
1		brdom3.2	$⊢ B \in V$
2	1	brdom3	$⊢ A ≼ B \leftrightarrow \exists f (\forall x \exists^{*} y x f y \land \forall x \in A \exists y \in B y f x)$
3		mormo	$⊢ \exists^{} y x f y \to \exists^{} y \in A x f y$
4	3	alimi	$⊢ \forall x \exists^{} y x f y \to \forall x \exists^{} y \in A x f y$
5		alral	$⊢ \forall x \exists^{} y \in A x f y \to \forall x \in B \exists^{} y \in A x f y$
6	4 5	syl	$⊢ \forall x \exists^{} y x f y \to \forall x \in B \exists^{} y \in A x f y$
7	6	anim1i	$⊢ (\forall x \exists^{} y x f y \land \forall x \in A \exists y \in B y f x) \to (\forall x \in B \exists^{} y \in A x f y \land \forall x \in A \exists y \in B y f x)$
8	7	eximi	$⊢ \exists f (\forall x \exists^{} y x f y \land \forall x \in A \exists y \in B y f x) \to \exists f (\forall x \in B \exists^{} y \in A x f y \land \forall x \in A \exists y \in B y f x)$
9	2 8	sylbi	$⊢ A ≼ B \to \exists f (\forall x \in B \exists^{*} y \in A x f y \land \forall x \in A \exists y \in B y f x)$
10		inss2	$⊢ f \cap (B \times A) \subseteq B \times A$
11		dmss	$⊢ f \cap (B \times A) \subseteq B \times A \to dom (f \cap (B \times A)) \subseteq dom (B \times A)$
12	10 11	ax-mp	$⊢ dom (f \cap (B \times A)) \subseteq dom (B \times A)$
13		dmxpss	$⊢ dom (B \times A) \subseteq B$
14	12 13	sstri	$⊢ dom (f \cap (B \times A)) \subseteq B$
15	14	sseli	$⊢ x \in dom (f \cap (B \times A)) \to x \in B$
16	10	rnssi	$⊢ ran (f \cap (B \times A)) \subseteq ran (B \times A)$
17		rnxpss	$⊢ ran (B \times A) \subseteq A$
18	16 17	sstri	$⊢ ran (f \cap (B \times A)) \subseteq A$
19	18	sseli	$⊢ y \in ran (f \cap (B \times A)) \to y \in A$
20		inss1	$⊢ f \cap (B \times A) \subseteq f$
21	20	ssbri	$⊢ x (f \cap (B \times A)) y \to x f y$
22	19 21	anim12i	$⊢ (y \in ran (f \cap (B \times A)) \land x (f \cap (B \times A)) y) \to (y \in A \land x f y)$
23	22	moimi	$⊢ \exists^{} y (y \in A \land x f y) \to \exists^{} y (y \in ran (f \cap (B \times A)) \land x (f \cap (B \times A)) y)$
24		df-rmo	$⊢ \exists^{} y \in A x f y \leftrightarrow \exists^{} y (y \in A \land x f y)$
25		df-rmo	$⊢ \exists^{} y \in ran (f \cap (B \times A)) x (f \cap (B \times A)) y \leftrightarrow \exists^{} y (y \in ran (f \cap (B \times A)) \land x (f \cap (B \times A)) y)$
26	23 24 25	3imtr4i	$⊢ \exists^{} y \in A x f y \to \exists^{} y \in ran (f \cap (B \times A)) x (f \cap (B \times A)) y$
27	15 26	imim12i	$⊢ (x \in B \to \exists^{} y \in A x f y) \to (x \in dom (f \cap (B \times A)) \to \exists^{} y \in ran (f \cap (B \times A)) x (f \cap (B \times A)) y)$
28	27	ralimi2	$⊢ \forall x \in B \exists^{} y \in A x f y \to \forall x \in dom (f \cap (B \times A)) \exists^{} y \in ran (f \cap (B \times A)) x (f \cap (B \times A)) y$
29		relinxp	$⊢ Rel (f \cap (B \times A))$
30	28 29	jctil	$⊢ \forall x \in B \exists^{} y \in A x f y \to (Rel (f \cap (B \times A)) \land \forall x \in dom (f \cap (B \times A)) \exists^{} y \in ran (f \cap (B \times A)) x (f \cap (B \times A)) y)$
31		dffun9	$⊢ Fun (f \cap (B \times A)) \leftrightarrow (Rel (f \cap (B \times A)) \land \forall x \in dom (f \cap (B \times A)) \exists^{*} y \in ran (f \cap (B \times A)) x (f \cap (B \times A)) y)$
32	30 31	sylibr	$⊢ \forall x \in B \exists^{*} y \in A x f y \to Fun (f \cap (B \times A))$
33	32	funfnd	$⊢ \forall x \in B \exists^{*} y \in A x f y \to (f \cap (B \times A)) Fn dom (f \cap (B \times A))$
34		rninxp	$⊢ ran (f \cap (B \times A)) = A \leftrightarrow \forall x \in A \exists y \in B y f x$
35	34	biimpri	$⊢ \forall x \in A \exists y \in B y f x \to ran (f \cap (B \times A)) = A$
36	33 35	anim12i	$⊢ (\forall x \in B \exists^{*} y \in A x f y \land \forall x \in A \exists y \in B y f x) \to ((f \cap (B \times A)) Fn dom (f \cap (B \times A)) \land ran (f \cap (B \times A)) = A)$
37		df-fo	$⊢ (f \cap (B \times A)) : dom (f \cap (B \times A)) \underset{onto}{⟶} A \leftrightarrow ((f \cap (B \times A)) Fn dom (f \cap (B \times A)) \land ran (f \cap (B \times A)) = A)$
38	36 37	sylibr	$⊢ (\forall x \in B \exists^{*} y \in A x f y \land \forall x \in A \exists y \in B y f x) \to (f \cap (B \times A)) : dom (f \cap (B \times A)) \underset{onto}{⟶} A$
39		vex	$⊢ f \in V$
40	39	inex1	$⊢ f \cap (B \times A) \in V$
41	40	dmex	$⊢ dom (f \cap (B \times A)) \in V$
42	41	fodom	$⊢ (f \cap (B \times A)) : dom (f \cap (B \times A)) \underset{onto}{⟶} A \to A ≼ dom (f \cap (B \times A))$
43	38 42	syl	$⊢ (\forall x \in B \exists^{*} y \in A x f y \land \forall x \in A \exists y \in B y f x) \to A ≼ dom (f \cap (B \times A))$
44		ssdomg	$⊢ B \in V \to (dom (f \cap (B \times A)) \subseteq B \to dom (f \cap (B \times A)) ≼ B)$
45	1 14 44	mp2	$⊢ dom (f \cap (B \times A)) ≼ B$
46		domtr	$⊢ (A ≼ dom (f \cap (B \times A)) \land dom (f \cap (B \times A)) ≼ B) \to A ≼ B$
47	43 45 46	sylancl	$⊢ (\forall x \in B \exists^{*} y \in A x f y \land \forall x \in A \exists y \in B y f x) \to A ≼ B$
48	47	exlimiv	$⊢ \exists f (\forall x \in B \exists^{*} y \in A x f y \land \forall x \in A \exists y \in B y f x) \to A ≼ B$
49	9 48	impbii	$⊢ A ≼ B \leftrightarrow \exists f (\forall x \in B \exists^{*} y \in A x f y \land \forall x \in A \exists y \in B y f x)$

Metamath Proof Explorer

Theorem brdom4

Proof