brdom3

Description: Equivalence to a dominance relation. (Contributed by NM, 27-Mar-2007)

		Ref	Expression
	Hypothesis	brdom3.2	$⊢ B \in V$
	Assertion	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)$

Proof

Step	Hyp	Ref	Expression
1		brdom3.2	$⊢ B \in V$
2		reldom	$⊢ Rel ≼$
3	2	brrelex1i	$⊢ A ≼ B \to A \in V$
4		0sdomg	$⊢ A \in V \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
5	3 4	syl	$⊢ A ≼ B \to (\emptyset ≺ A \leftrightarrow A \neq \emptyset)$
6		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
7	5 6	bitrdi	$⊢ A ≼ B \to (\emptyset ≺ A \leftrightarrow \neg A = \emptyset)$
8	7	biimpar	$⊢ (A ≼ B \land \neg A = \emptyset) \to \emptyset ≺ A$
9		fodomr	$⊢ (\emptyset ≺ A \land A ≼ B) \to \exists f f : B \underset{onto}{⟶} A$
10	9	ancoms	$⊢ (A ≼ B \land \emptyset ≺ A) \to \exists f f : B \underset{onto}{⟶} A$
11	8 10	syldan	$⊢ (A ≼ B \land \neg A = \emptyset) \to \exists f f : B \underset{onto}{⟶} A$
12		pm5.6	$⊢ ((A ≼ B \land \neg A = \emptyset) \to \exists f f : B \underset{onto}{⟶} A) \leftrightarrow (A ≼ B \to (A = \emptyset \lor \exists f f : B \underset{onto}{⟶} A))$
13	11 12	mpbi	$⊢ A ≼ B \to (A = \emptyset \lor \exists f f : B \underset{onto}{⟶} A)$
14		br0	$⊢ \neg x \emptyset y$
15	14	nex	$⊢ \neg \exists y x \emptyset y$
16		exmo	$⊢ (\exists y x \emptyset y \lor \exists^{*} y x \emptyset y)$
17	15 16	mtpor	$⊢ \exists^{*} y x \emptyset y$
18	17	ax-gen	$⊢ \forall x \exists^{*} y x \emptyset y$
19		rzal	$⊢ A = \emptyset \to \forall x \in A \exists y \in B y \emptyset x$
20		0ex	$⊢ \emptyset \in V$
21		breq	$⊢ f = \emptyset \to (x f y \leftrightarrow x \emptyset y)$
22	21	mobidv	$⊢ f = \emptyset \to (\exists^{} y x f y \leftrightarrow \exists^{} y x \emptyset y)$
23	22	albidv	$⊢ f = \emptyset \to (\forall x \exists^{} y x f y \leftrightarrow \forall x \exists^{} y x \emptyset y)$
24		breq	$⊢ f = \emptyset \to (y f x \leftrightarrow y \emptyset x)$
25	24	rexbidv	$⊢ f = \emptyset \to (\exists y \in B y f x \leftrightarrow \exists y \in B y \emptyset x)$
26	25	ralbidv	$⊢ f = \emptyset \to (\forall x \in A \exists y \in B y f x \leftrightarrow \forall x \in A \exists y \in B y \emptyset x)$
27	23 26	anbi12d	$⊢ f = \emptyset \to ((\forall x \exists^{} y x f y \land \forall x \in A \exists y \in B y f x) \leftrightarrow (\forall x \exists^{} y x \emptyset y \land \forall x \in A \exists y \in B y \emptyset x))$
28	20 27	spcev	$⊢ (\forall x \exists^{} y x \emptyset y \land \forall x \in A \exists y \in B y \emptyset x) \to \exists f (\forall x \exists^{} y x f y \land \forall x \in A \exists y \in B y f x)$
29	18 19 28	sylancr	$⊢ A = \emptyset \to \exists f (\forall x \exists^{*} y x f y \land \forall x \in A \exists y \in B y f x)$
30		fofun	$⊢ f : B \underset{onto}{⟶} A \to Fun f$
31		dffun6	$⊢ Fun f \leftrightarrow (Rel f \land \forall x \exists^{*} y x f y)$
32	31	simprbi	$⊢ Fun f \to \forall x \exists^{*} y x f y$
33	30 32	syl	$⊢ f : B \underset{onto}{⟶} A \to \forall x \exists^{*} y x f y$
34		dffo4	$⊢ f : B \underset{onto}{⟶} A \leftrightarrow (f : B ⟶ A \land \forall x \in A \exists y \in B y f x)$
35	34	simprbi	$⊢ f : B \underset{onto}{⟶} A \to \forall x \in A \exists y \in B y f x$
36	33 35	jca	$⊢ f : B \underset{onto}{⟶} A \to (\forall x \exists^{*} y x f y \land \forall x \in A \exists y \in B y f x)$
37	36	eximi	$⊢ \exists f f : B \underset{onto}{⟶} A \to \exists f (\forall x \exists^{*} y x f y \land \forall x \in A \exists y \in B y f x)$
38	29 37	jaoi	$⊢ (A = \emptyset \lor \exists f f : B \underset{onto}{⟶} A) \to \exists f (\forall x \exists^{*} y x f y \land \forall x \in A \exists y \in B y f x)$
39	13 38	syl	$⊢ A ≼ B \to \exists f (\forall x \exists^{*} y x f y \land \forall x \in A \exists y \in B y f x)$
40		inss1	$⊢ f \cap (B \times A) \subseteq f$
41	40	ssbri	$⊢ x (f \cap (B \times A)) y \to x f y$
42	41	moimi	$⊢ \exists^{} y x f y \to \exists^{} y x (f \cap (B \times A)) y$
43	42	alimi	$⊢ \forall x \exists^{} y x f y \to \forall x \exists^{} y x (f \cap (B \times A)) y$
44		relinxp	$⊢ Rel (f \cap (B \times A))$
45		dffun6	$⊢ Fun (f \cap (B \times A)) \leftrightarrow (Rel (f \cap (B \times A)) \land \forall x \exists^{*} y x (f \cap (B \times A)) y)$
46	44 45	mpbiran	$⊢ Fun (f \cap (B \times A)) \leftrightarrow \forall x \exists^{*} y x (f \cap (B \times A)) y$
47	43 46	sylibr	$⊢ \forall x \exists^{*} y x f y \to Fun (f \cap (B \times A))$
48	47	funfnd	$⊢ \forall x \exists^{*} y x f y \to (f \cap (B \times A)) Fn dom (f \cap (B \times A))$
49		rninxp	$⊢ ran (f \cap (B \times A)) = A \leftrightarrow \forall x \in A \exists y \in B y f x$
50	49	biimpri	$⊢ \forall x \in A \exists y \in B y f x \to ran (f \cap (B \times A)) = A$
51	48 50	anim12i	$⊢ (\forall x \exists^{*} y 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)$
52		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)$
53	51 52	sylibr	$⊢ (\forall x \exists^{*} y 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$
54		vex	$⊢ f \in V$
55	54	inex1	$⊢ f \cap (B \times A) \in V$
56	55	dmex	$⊢ dom (f \cap (B \times A)) \in V$
57	56	fodom	$⊢ (f \cap (B \times A)) : dom (f \cap (B \times A)) \underset{onto}{⟶} A \to A ≼ dom (f \cap (B \times A))$
58		inss2	$⊢ f \cap (B \times A) \subseteq B \times A$
59		dmss	$⊢ f \cap (B \times A) \subseteq B \times A \to dom (f \cap (B \times A)) \subseteq dom (B \times A)$
60	58 59	ax-mp	$⊢ dom (f \cap (B \times A)) \subseteq dom (B \times A)$
61		dmxpss	$⊢ dom (B \times A) \subseteq B$
62	60 61	sstri	$⊢ dom (f \cap (B \times A)) \subseteq B$
63		ssdomg	$⊢ B \in V \to (dom (f \cap (B \times A)) \subseteq B \to dom (f \cap (B \times A)) ≼ B)$
64	1 62 63	mp2	$⊢ dom (f \cap (B \times A)) ≼ B$
65		domtr	$⊢ (A ≼ dom (f \cap (B \times A)) \land dom (f \cap (B \times A)) ≼ B) \to A ≼ B$
66	64 65	mpan2	$⊢ A ≼ dom (f \cap (B \times A)) \to A ≼ B$
67	53 57 66	3syl	$⊢ (\forall x \exists^{*} y x f y \land \forall x \in A \exists y \in B y f x) \to A ≼ B$
68	67	exlimiv	$⊢ \exists f (\forall x \exists^{*} y x f y \land \forall x \in A \exists y \in B y f x) \to A ≼ B$
69	39 68	impbii	$⊢ A ≼ B \leftrightarrow \exists f (\forall x \exists^{*} y x f y \land \forall x \in A \exists y \in B y f x)$

Metamath Proof Explorer

Theorem brdom3

Proof