brdom7disj

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

	Ref	Expression
Hypotheses	brdom7disj.1	$⊢ A \in V$
	brdom7disj.2	$⊢ B \in V$
	brdom7disj.3	$⊢ A \cap B = \emptyset$
Assertion	brdom7disj	$⊢ A ≼ B \leftrightarrow \exists f (\forall x \in B \exists^{*} y \in A \{x, y\} \in f \land \forall x \in A \exists y \in B \{y, x\} \in f)$

Proof

Step	Hyp	Ref	Expression
1		brdom7disj.1	$⊢ A \in V$
2		brdom7disj.2	$⊢ B \in V$
3		brdom7disj.3	$⊢ A \cap B = \emptyset$
4	2	brdom4	$⊢ A ≼ B \leftrightarrow \exists g (\forall x \in B \exists^{*} y \in A x g y \land \forall x \in A \exists y \in B y g x)$
5		incom	$⊢ B \cap A = A \cap B$
6	5 3	eqtri	$⊢ B \cap A = \emptyset$
7		disjne	$⊢ (B \cap A = \emptyset \land x \in B \land w \in A) \to x \neq w$
8	6 7	mp3an1	$⊢ (x \in B \land w \in A) \to x \neq w$
9		vex	$⊢ x \in V$
10		vex	$⊢ y \in V$
11		vex	$⊢ z \in V$
12		vex	$⊢ w \in V$
13	9 10 11 12	opthpr	$⊢ x \neq w \to (\{x, y\} = \{z, w\} \leftrightarrow (x = z \land y = w))$
14	8 13	syl	$⊢ (x \in B \land w \in A) \to (\{x, y\} = \{z, w\} \leftrightarrow (x = z \land y = w))$
15		equcom	$⊢ x = z \leftrightarrow z = x$
16		equcom	$⊢ y = w \leftrightarrow w = y$
17	15 16	anbi12i	$⊢ (x = z \land y = w) \leftrightarrow (z = x \land w = y)$
18	14 17	syl6rbb	$⊢ (x \in B \land w \in A) \to ((z = x \land w = y) \leftrightarrow \{x, y\} = \{z, w\})$
19		df-br	$⊢ z g w \leftrightarrow ⟨z, w⟩ \in g$
20	19	a1i	$⊢ (x \in B \land w \in A) \to (z g w \leftrightarrow ⟨z, w⟩ \in g)$
21	18 20	anbi12d	$⊢ (x \in B \land w \in A) \to (((z = x \land w = y) \land z g w) \leftrightarrow (\{x, y\} = \{z, w\} \land ⟨z, w⟩ \in g))$
22	21	rexbidva	$⊢ x \in B \to (\exists w \in A ((z = x \land w = y) \land z g w) \leftrightarrow \exists w \in A (\{x, y\} = \{z, w\} \land ⟨z, w⟩ \in g))$
23	22	rexbidv	$⊢ x \in B \to (\exists z \in B \exists w \in A ((z = x \land w = y) \land z g w) \leftrightarrow \exists z \in B \exists w \in A (\{x, y\} = \{z, w\} \land ⟨z, w⟩ \in g))$
24		rexcom	$⊢ \exists z \in B \exists w \in A (\{x, y\} = \{z, w\} \land ⟨z, w⟩ \in g) \leftrightarrow \exists w \in A \exists z \in B (\{x, y\} = \{z, w\} \land ⟨z, w⟩ \in g)$
25		zfpair2	$⊢ \{x, y\} \in V$
26		eqeq1	$⊢ v = \{x, y\} \to (v = \{z, w\} \leftrightarrow \{x, y\} = \{z, w\})$
27	26	anbi1d	$⊢ v = \{x, y\} \to ((v = \{z, w\} \land ⟨z, w⟩ \in g) \leftrightarrow (\{x, y\} = \{z, w\} \land ⟨z, w⟩ \in g))$
28	27	2rexbidv	$⊢ v = \{x, y\} \to (\exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g) \leftrightarrow \exists w \in A \exists z \in B (\{x, y\} = \{z, w\} \land ⟨z, w⟩ \in g))$
29	25 28	elab	$⊢ \{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow \exists w \in A \exists z \in B (\{x, y\} = \{z, w\} \land ⟨z, w⟩ \in g)$
30	24 29	bitr4i	$⊢ \exists z \in B \exists w \in A (\{x, y\} = \{z, w\} \land ⟨z, w⟩ \in g) \leftrightarrow \{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\}$
31	23 30	syl6rbb	$⊢ x \in B \to (\{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow \exists z \in B \exists w \in A ((z = x \land w = y) \land z g w))$
32	31	adantr	$⊢ (x \in B \land y \in A) \to (\{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow \exists z \in B \exists w \in A ((z = x \land w = y) \land z g w))$
33		breq1	$⊢ z = x \to (z g w \leftrightarrow x g w)$
34		breq2	$⊢ w = y \to (x g w \leftrightarrow x g y)$
35	33 34	ceqsrex2v	$⊢ (x \in B \land y \in A) \to (\exists z \in B \exists w \in A ((z = x \land w = y) \land z g w) \leftrightarrow x g y)$
36	32 35	bitrd	$⊢ (x \in B \land y \in A) \to (\{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow x g y)$
37	36	rmobidva	$⊢ x \in B \to (\exists^{} y \in A \{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow \exists^{} y \in A x g y)$
38	37	ralbiia	$⊢ \forall x \in B \exists^{} y \in A \{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow \forall x \in B \exists^{} y \in A x g y$
39		zfpair2	$⊢ \{y, x\} \in V$
40		eqeq1	$⊢ v = \{y, x\} \to (v = \{z, w\} \leftrightarrow \{y, x\} = \{z, w\})$
41	40	anbi1d	$⊢ v = \{y, x\} \to ((v = \{z, w\} \land ⟨z, w⟩ \in g) \leftrightarrow (\{y, x\} = \{z, w\} \land ⟨z, w⟩ \in g))$
42	41	2rexbidv	$⊢ v = \{y, x\} \to (\exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g) \leftrightarrow \exists w \in A \exists z \in B (\{y, x\} = \{z, w\} \land ⟨z, w⟩ \in g))$
43	39 42	elab	$⊢ \{y, x\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow \exists w \in A \exists z \in B (\{y, x\} = \{z, w\} \land ⟨z, w⟩ \in g)$
44		disjne	$⊢ (B \cap A = \emptyset \land z \in B \land x \in A) \to z \neq x$
45	6 44	mp3an1	$⊢ (z \in B \land x \in A) \to z \neq x$
46	45	ancoms	$⊢ (x \in A \land z \in B) \to z \neq x$
47	11 12 10 9	opthpr	$⊢ z \neq x \to (\{z, w\} = \{y, x\} \leftrightarrow (z = y \land w = x))$
48	46 47	syl	$⊢ (x \in A \land z \in B) \to (\{z, w\} = \{y, x\} \leftrightarrow (z = y \land w = x))$
49		eqcom	$⊢ \{y, x\} = \{z, w\} \leftrightarrow \{z, w\} = \{y, x\}$
50		ancom	$⊢ (w = x \land z = y) \leftrightarrow (z = y \land w = x)$
51	48 49 50	3bitr4g	$⊢ (x \in A \land z \in B) \to (\{y, x\} = \{z, w\} \leftrightarrow (w = x \land z = y))$
52	19	bicomi	$⊢ ⟨z, w⟩ \in g \leftrightarrow z g w$
53	52	a1i	$⊢ (x \in A \land z \in B) \to (⟨z, w⟩ \in g \leftrightarrow z g w)$
54	51 53	anbi12d	$⊢ (x \in A \land z \in B) \to ((\{y, x\} = \{z, w\} \land ⟨z, w⟩ \in g) \leftrightarrow ((w = x \land z = y) \land z g w))$
55	54	rexbidva	$⊢ x \in A \to (\exists z \in B (\{y, x\} = \{z, w\} \land ⟨z, w⟩ \in g) \leftrightarrow \exists z \in B ((w = x \land z = y) \land z g w))$
56	55	rexbidv	$⊢ x \in A \to (\exists w \in A \exists z \in B (\{y, x\} = \{z, w\} \land ⟨z, w⟩ \in g) \leftrightarrow \exists w \in A \exists z \in B ((w = x \land z = y) \land z g w))$
57	43 56	syl5bb	$⊢ x \in A \to (\{y, x\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow \exists w \in A \exists z \in B ((w = x \land z = y) \land z g w))$
58	57	adantr	$⊢ (x \in A \land y \in B) \to (\{y, x\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow \exists w \in A \exists z \in B ((w = x \land z = y) \land z g w))$
59		breq2	$⊢ w = x \to (z g w \leftrightarrow z g x)$
60		breq1	$⊢ z = y \to (z g x \leftrightarrow y g x)$
61	59 60	ceqsrex2v	$⊢ (x \in A \land y \in B) \to (\exists w \in A \exists z \in B ((w = x \land z = y) \land z g w) \leftrightarrow y g x)$
62	58 61	bitrd	$⊢ (x \in A \land y \in B) \to (\{y, x\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow y g x)$
63	62	rexbidva	$⊢ x \in A \to (\exists y \in B \{y, x\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow \exists y \in B y g x)$
64	63	ralbiia	$⊢ \forall x \in A \exists y \in B \{y, x\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \leftrightarrow \forall x \in A \exists y \in B y g x$
65		snex	$⊢ \{\{z, w\}\} \in V$
66		simpl	$⊢ (v = \{z, w\} \land ⟨z, w⟩ \in g) \to v = \{z, w\}$
67	66	ss2abi	$⊢ \{v \| (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \subseteq \{v \| v = \{z, w\}\}$
68		df-sn	$⊢ \{\{z, w\}\} = \{v \| v = \{z, w\}\}$
69	67 68	sseqtrri	$⊢ \{v \| (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \subseteq \{\{z, w\}\}$
70	65 69	ssexi	$⊢ \{v \| (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \in V$
71	1 2 70	ab2rexex2	$⊢ \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \in V$
72		eleq2	$⊢ f = \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \to (\{x, y\} \in f \leftrightarrow \{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\})$
73	72	rmobidv	$⊢ f = \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \to (\exists^{} y \in A \{x, y\} \in f \leftrightarrow \exists^{} y \in A \{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\})$
74	73	ralbidv	$⊢ f = \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \to (\forall x \in B \exists^{} y \in A \{x, y\} \in f \leftrightarrow \forall x \in B \exists^{} y \in A \{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\})$
75		eleq2	$⊢ f = \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \to (\{y, x\} \in f \leftrightarrow \{y, x\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\})$
76	75	rexbidv	$⊢ f = \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \to (\exists y \in B \{y, x\} \in f \leftrightarrow \exists y \in B \{y, x\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\})$
77	76	ralbidv	$⊢ f = \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \to (\forall x \in A \exists y \in B \{y, x\} \in f \leftrightarrow \forall x \in A \exists y \in B \{y, x\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\})$
78	74 77	anbi12d	$⊢ f = \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \to ((\forall x \in B \exists^{} y \in A \{x, y\} \in f \land \forall x \in A \exists y \in B \{y, x\} \in f) \leftrightarrow (\forall x \in B \exists^{} y \in A \{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \land \forall x \in A \exists y \in B \{y, x\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\}))$
79	71 78	spcev	$⊢ (\forall x \in B \exists^{} y \in A \{x, y\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\} \land \forall x \in A \exists y \in B \{y, x\} \in \{v \| \exists w \in A \exists z \in B (v = \{z, w\} \land ⟨z, w⟩ \in g)\}) \to \exists f (\forall x \in B \exists^{} y \in A \{x, y\} \in f \land \forall x \in A \exists y \in B \{y, x\} \in f)$
80	38 64 79	syl2anbr	$⊢ (\forall x \in B \exists^{} y \in A x g y \land \forall x \in A \exists y \in B y g x) \to \exists f (\forall x \in B \exists^{} y \in A \{x, y\} \in f \land \forall x \in A \exists y \in B \{y, x\} \in f)$
81	80	exlimiv	$⊢ \exists g (\forall x \in B \exists^{} y \in A x g y \land \forall x \in A \exists y \in B y g x) \to \exists f (\forall x \in B \exists^{} y \in A \{x, y\} \in f \land \forall x \in A \exists y \in B \{y, x\} \in f)$
82		preq1	$⊢ w = x \to \{w, z\} = \{x, z\}$
83	82	eleq1d	$⊢ w = x \to (\{w, z\} \in f \leftrightarrow \{x, z\} \in f)$
84		preq2	$⊢ z = y \to \{x, z\} = \{x, y\}$
85	84	eleq1d	$⊢ z = y \to (\{x, z\} \in f \leftrightarrow \{x, y\} \in f)$
86		eqid	$⊢ \{⟨w, z⟩ \| \{w, z\} \in f\} = \{⟨w, z⟩ \| \{w, z\} \in f\}$
87	9 10 83 85 86	brab	$⊢ x \{⟨w, z⟩ \| \{w, z\} \in f\} y \leftrightarrow \{x, y\} \in f$
88	87	rmobii	$⊢ \exists^{} y \in A x \{⟨w, z⟩ \| \{w, z\} \in f\} y \leftrightarrow \exists^{} y \in A \{x, y\} \in f$
89	88	ralbii	$⊢ \forall x \in B \exists^{} y \in A x \{⟨w, z⟩ \| \{w, z\} \in f\} y \leftrightarrow \forall x \in B \exists^{} y \in A \{x, y\} \in f$
90		preq1	$⊢ w = y \to \{w, z\} = \{y, z\}$
91	90	eleq1d	$⊢ w = y \to (\{w, z\} \in f \leftrightarrow \{y, z\} \in f)$
92		preq2	$⊢ z = x \to \{y, z\} = \{y, x\}$
93	92	eleq1d	$⊢ z = x \to (\{y, z\} \in f \leftrightarrow \{y, x\} \in f)$
94	10 9 91 93 86	brab	$⊢ y \{⟨w, z⟩ \| \{w, z\} \in f\} x \leftrightarrow \{y, x\} \in f$
95	94	rexbii	$⊢ \exists y \in B y \{⟨w, z⟩ \| \{w, z\} \in f\} x \leftrightarrow \exists y \in B \{y, x\} \in f$
96	95	ralbii	$⊢ \forall x \in A \exists y \in B y \{⟨w, z⟩ \| \{w, z\} \in f\} x \leftrightarrow \forall x \in A \exists y \in B \{y, x\} \in f$
97		df-opab	$⊢ \{⟨w, z⟩ \| \{w, z\} \in f\} = \{v \| \exists w \exists z (v = ⟨w, z⟩ \land \{w, z\} \in f)\}$
98		vuniex	$⊢ ⋃ f \in V$
99	12	prid1	$⊢ w \in \{w, z\}$
100		elunii	$⊢ (w \in \{w, z\} \land \{w, z\} \in f) \to w \in ⋃ f$
101	99 100	mpan	$⊢ \{w, z\} \in f \to w \in ⋃ f$
102	101	adantl	$⊢ (v = ⟨w, z⟩ \land \{w, z\} \in f) \to w \in ⋃ f$
103	102	exlimiv	$⊢ \exists z (v = ⟨w, z⟩ \land \{w, z\} \in f) \to w \in ⋃ f$
104	11	prid2	$⊢ z \in \{w, z\}$
105		elunii	$⊢ (z \in \{w, z\} \land \{w, z\} \in f) \to z \in ⋃ f$
106	104 105	mpan	$⊢ \{w, z\} \in f \to z \in ⋃ f$
107	106	adantl	$⊢ (v = ⟨w, z⟩ \land \{w, z\} \in f) \to z \in ⋃ f$
108		df-sn	$⊢ \{⟨w, z⟩\} = \{v \| v = ⟨w, z⟩\}$
109		snex	$⊢ \{⟨w, z⟩\} \in V$
110	108 109	eqeltrri	$⊢ \{v \| v = ⟨w, z⟩\} \in V$
111		simpl	$⊢ (v = ⟨w, z⟩ \land \{w, z\} \in f) \to v = ⟨w, z⟩$
112	111	ss2abi	$⊢ \{v \| (v = ⟨w, z⟩ \land \{w, z\} \in f)\} \subseteq \{v \| v = ⟨w, z⟩\}$
113	110 112	ssexi	$⊢ \{v \| (v = ⟨w, z⟩ \land \{w, z\} \in f)\} \in V$
114	98 107 113	abexex	$⊢ \{v \| \exists z (v = ⟨w, z⟩ \land \{w, z\} \in f)\} \in V$
115	98 103 114	abexex	$⊢ \{v \| \exists w \exists z (v = ⟨w, z⟩ \land \{w, z\} \in f)\} \in V$
116	97 115	eqeltri	$⊢ \{⟨w, z⟩ \| \{w, z\} \in f\} \in V$
117		breq	$⊢ g = \{⟨w, z⟩ \| \{w, z\} \in f\} \to (x g y \leftrightarrow x \{⟨w, z⟩ \| \{w, z\} \in f\} y)$
118	117	rmobidv	$⊢ g = \{⟨w, z⟩ \| \{w, z\} \in f\} \to (\exists^{} y \in A x g y \leftrightarrow \exists^{} y \in A x \{⟨w, z⟩ \| \{w, z\} \in f\} y)$
119	118	ralbidv	$⊢ g = \{⟨w, z⟩ \| \{w, z\} \in f\} \to (\forall x \in B \exists^{} y \in A x g y \leftrightarrow \forall x \in B \exists^{} y \in A x \{⟨w, z⟩ \| \{w, z\} \in f\} y)$
120		breq	$⊢ g = \{⟨w, z⟩ \| \{w, z\} \in f\} \to (y g x \leftrightarrow y \{⟨w, z⟩ \| \{w, z\} \in f\} x)$
121	120	rexbidv	$⊢ g = \{⟨w, z⟩ \| \{w, z\} \in f\} \to (\exists y \in B y g x \leftrightarrow \exists y \in B y \{⟨w, z⟩ \| \{w, z\} \in f\} x)$
122	121	ralbidv	$⊢ g = \{⟨w, z⟩ \| \{w, z\} \in f\} \to (\forall x \in A \exists y \in B y g x \leftrightarrow \forall x \in A \exists y \in B y \{⟨w, z⟩ \| \{w, z\} \in f\} x)$
123	119 122	anbi12d	$⊢ g = \{⟨w, z⟩ \| \{w, z\} \in f\} \to ((\forall x \in B \exists^{} y \in A x g y \land \forall x \in A \exists y \in B y g x) \leftrightarrow (\forall x \in B \exists^{} y \in A x \{⟨w, z⟩ \| \{w, z\} \in f\} y \land \forall x \in A \exists y \in B y \{⟨w, z⟩ \| \{w, z\} \in f\} x))$
124	116 123	spcev	$⊢ (\forall x \in B \exists^{} y \in A x \{⟨w, z⟩ \| \{w, z\} \in f\} y \land \forall x \in A \exists y \in B y \{⟨w, z⟩ \| \{w, z\} \in f\} x) \to \exists g (\forall x \in B \exists^{} y \in A x g y \land \forall x \in A \exists y \in B y g x)$
125	89 96 124	syl2anbr	$⊢ (\forall x \in B \exists^{} y \in A \{x, y\} \in f \land \forall x \in A \exists y \in B \{y, x\} \in f) \to \exists g (\forall x \in B \exists^{} y \in A x g y \land \forall x \in A \exists y \in B y g x)$
126	125	exlimiv	$⊢ \exists f (\forall x \in B \exists^{} y \in A \{x, y\} \in f \land \forall x \in A \exists y \in B \{y, x\} \in f) \to \exists g (\forall x \in B \exists^{} y \in A x g y \land \forall x \in A \exists y \in B y g x)$
127	81 126	impbii	$⊢ \exists g (\forall x \in B \exists^{} y \in A x g y \land \forall x \in A \exists y \in B y g x) \leftrightarrow \exists f (\forall x \in B \exists^{} y \in A \{x, y\} \in f \land \forall x \in A \exists y \in B \{y, x\} \in f)$
128	4 127	bitri	$⊢ A ≼ B \leftrightarrow \exists f (\forall x \in B \exists^{*} y \in A \{x, y\} \in f \land \forall x \in A \exists y \in B \{y, x\} \in f)$

Metamath Proof Explorer

Theorem brdom7disj

Proof