brdom6disj

Description: An equivalence to a dominance relation for disjoint sets. (Contributed by NM, 5-Apr-2007)

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

Metamath Proof Explorer

Theorem brdom6disj

Proof