Theorem brdom7disj 4784

Description: An equivalence to a dominance relation for disjoint sets.

Hypotheses

Ref	Expression
brdom7disj.1	|- A e. V
brdom7disj.2	|- B e. V
brdom7disj.3	|- (A i^i B) = (/)

Assertion

Ref	Expression
brdom7disj	|- (A ~<_ B <-> E.f(A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f))

Distinct variable groups:   x,f,y,A   B,f,x,y

Proof of Theorem brdom7disj

Step	Hyp	Ref	Expression
1		brdom7disj.1	. . 3 |- A e. V
2		brdom7disj.2	. . 3 |- B e. V
3	1, 2	brdom4 4783	. 2 |- (A ~<_ B <-> E.g(A.x e. B E*y(y e. A /\ xgy) /\ A.x e. A E.y e. B ygx))
4		snex 2745	. . . . . . . . 9 |- {{z, w}} e. V
5		pm3.26 319	. . . . . . . . . . 11 |- ((v = {z, w} /\ <.z, w>. e. g) -> v = {z, w})
6	5	ss2abi 2116	. . . . . . . . . 10 |- {v | (v = {z, w} /\ <.z, w>. e. g)} (_ {v | v = {z, w}}
7		df-sn 2408	. . . . . . . . . 10 |- {{z, w}} = {v | v = {z, w}}
8	6, 7	sseqtr4 2090	. . . . . . . . 9 |- {v | (v = {z, w} /\ <.z, w>. e. g)} (_ {{z, w}}
9	4, 8	ssexi 2715	. . . . . . . 8 |- {v | (v = {z, w} /\ <.z, w>. e. g)} e. V
10	2, 9	abrexex2 3862	. . . . . . 7 |- {v | E.z e. B (v = {z, w} /\ <.z, w>. e. g)} e. V
11	1, 10	abrexex2 3862	. . . . . 6 |- {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} e. V
12		ax-17 969	. . . . . . . . 9 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> A.y f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)})
13		eleq2 1532	. . . . . . . . . 10 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> ({x, y} e. f <-> {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}))
14	13	anbi2d 615	. . . . . . . . 9 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> ((y e. A /\ {x, y} e. f) <-> (y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)})))
15	12, 14	mobid 1402	. . . . . . . 8 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> (E*y(y e. A /\ {x, y} e. f) <-> E*y(y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)})))
16	15	ralbidv 1660	. . . . . . 7 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> (A.x e. B E*y(y e. A /\ {x, y} e. f) <-> A.x e. B E*y(y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)})))
17		eleq2 1532	. . . . . . . . 9 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> ({y, x} e. f <-> {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}))
18	17	rexbidv 1661	. . . . . . . 8 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> (E.y e. B {y, x} e. f <-> E.y e. B {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}))
19	18	ralbidv 1660	. . . . . . 7 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> (A.x e. A E.y e. B {y, x} e. f <-> A.x e. A E.y e. B {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}))
20	16, 19	anbi12d 627	. . . . . 6 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> ((A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f) <-> (A.x e. B E*y(y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}) /\ A.x e. A E.y e. B {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)})))
21	11, 20	cla4ev 1865	. . . . 5 |- ((A.x e. B E*y(y e. A /\ {x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}) /\ A.x e. A E.y e. B {y, x} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}) -> E.f(A.x e. B E*y(y e. A /\ {x, y} e. f) /\ A.x e. A E.y e. B {y, x} e. f))
22		ax-17 969	. . . . . . 7 |- (x e. B -> A.y x e. B)
23		incom 2204	. . . . . . . . . . . . . . . . . 18 |- (B i^i A) = (A i^i B)
24		brdom7disj.3	. . . . . . . . . . . . . . . . . 18 |- (A i^i B) = (/)
25	23, 24	eqtr 1492	. . . . . . . . . . . . . . . . 17 |- (B i^i A) = (/)
26		disjne 2311	. . . . . . . . . . . . . . . . 17 |- (((B i^i A) = (/) /\ x e. B /\ w e. A) -> x =/= w)
27	25, 26	mp3an1 901	. . . . . . . . . . . . . . . 16 |- ((x e. B /\ w e. A) -> x =/= w)
28		visset 1809	. . . . . . . . . . . . . . . . 17 |- x e. V
29		visset 1809	. . . . . . . . . . . . . . . . 17 |- y e. V
30		visset 1809	. . . . . . . . . . . . . . . . 17 |- z e. V
31		visset 1809	. . . . . . . . . . . . . . . . 17 |- w e. V
32	28, 29, 30, 31	opthpr 2481	. . . . . . . . . . . . . . . 16 |- (x =/= w -> ({x, y} = {z, w} <-> (x = z /\ y = w)))
33	27, 32	syl 10	. . . . . . . . . . . . . . 15 |- ((x e. B /\ w e. A) -> ({x, y} = {z, w} <-> (x = z /\ y = w)))
34		equcom 1127	. . . . . . . . . . . . . . . 16 |- (x = z <-> z = x)
35		equcom 1127	. . . . . . . . . . . . . . . 16 |- (y = w <-> w = y)
36	34, 35	anbi12i 482	. . . . . . . . . . . . . . 15 |- ((x = z /\ y = w) <-> (z = x /\ w = y))
37	33, 36	syl6rbb 536	. . . . . . . . . . . . . 14 |- ((x e. B /\ w e. A) -> ((z = x /\ w = y) <-> {x, y} = {z, w}))
38		df-br 2615	. . . . . . . . . . . . . . 15 |- (zgw <-> <.z, w>. e. g)
39	38	a1i 8	. . . . . . . . . . . . . 14 |- ((x e. B /\ w e. A) -> (zgw <-> <.z, w>. e. g))
40	37, 39	anbi12d 627	. . . . . . . . . . . . 13 |- ((x e. B /\ w e. A) -> (((z = x /\ w = y) /\ zgw) <-> ({x, y} = {z, w} /\ <.z, w>. e. g)))
41	40	rexbidva 1657	. . . . . . . . . . . 12 |- (x e. B -> (E.w e. A ((z = x /\ w = y) /\ zgw) <-> E.w e. A ({x, y} = {z, w} /\ <.z, w>. e. g)))
42	41	rexbidv 1661	. . . . . . . . . . 11 |- (x e. B -> (E.z e. B E.w e. A ((z = x /\ w = y) /\ zgw) <-> E.z e. B E.w e. A ({x, y} = {z, w} /\ <.z, w>. e. g)))
43		rexcom 1772	. . . . . . . . . . . 12 |- (E.z e. B E.w e. A ({x, y} = {z, w} /\ <.z, w>. e. g) <-> E.w e. A E.z e. B ({x, y} = {z, w} /\ <.z, w>. e. g))
44		zfpair2 2775	. . . . . . . . . . . . 13 |- {x, y} e. V
45		eqeq1 1478	. . . . . . . . . . . . . . 15 |- (v = {x, y} -> (v = {z, w} <-> {x, y} = {z, w}))
46	45	anbi1d 616	. . . . . . . . . . . . . 14 |- (v = {x, y} -> ((v = {z, w} /\ <.z, w>. e. g) <-> ({x, y} = {z, w} /\ <.z, w>. e. g)))
47	46	2rexbidv 1678	. . . . . . . . . . . . 13 |- (v = {x, y} -> (E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g) <-> E.w e. A E.z e. B ({x, y} = {z, w} /\ <.z, w>. e. g)))
48	44, 47	elab 1893	. . . . . . . . . . . 12 |- ({x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w