Theorem brdom6disj 4815

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
brdom6disj	|- (A ~<_ B <-> E.f(A.x e. B E*y{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 brdom6disj

Step	Hyp	Ref	Expression
1		brdom7disj.1	. . 3 |- A e. V
2		brdom7disj.2	. . 3 |- B e. V
3	1, 2	brdom5 4812	. 2 |- (A ~<_ B <-> E.g(A.x e. B E*y xgy /\ A.x e. A E.y e. B ygx))
4		snex 2756	. . . . . . . . 9 |- {{z, w}} e. V
5		pm3.26 319	. . . . . . . . . . 11 |- ((v = {z, w} /\ <.z, w>. e. g) -> v = {z, w})
6	5	ss2abi 2123	. . . . . . . . . 10 |- {v | (v = {z, w} /\ <.z, w>. e. g)} (_ {v | v = {z, w}}
7		df-sn 2416	. . . . . . . . . 10 |- {{z, w}} = {v | v = {z, w}}
8	6, 7	sseqtr4 2097	. . . . . . . . 9 |- {v | (v = {z, w} /\ <.z, w>. e. g)} (_ {{z, w}}
9	4, 8	ssexi 2725	. . . . . . . 8 |- {v | (v = {z, w} /\ <.z, w>. e. g)} e. V
10	2, 9	abrexex2 3877	. . . . . . 7 |- {v | E.z e. B (v = {z, w} /\ <.z, w>. e. g)} e. V
11	1, 10	abrexex2 3877	. . . . . 6 |- {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} e. V
12		ax-17 973	. . . . . . . . 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 1538	. . . . . . . . 9 |- (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	12, 13	mobid 1406	. . . . . . . 8 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> (E*y{x, y} e. f <-> E*y{x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}))
15	14	ralbidv 1666	. . . . . . 7 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> (A.x e. B E*y{x, y} e. f <-> A.x e. B E*y{x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)}))
16		eleq2 1538	. . . . . . . . 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)}))
17	16	rexbidv 1667	. . . . . . . 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)}))
18	17	ralbidv 1666	. . . . . . 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)}))
19	15, 18	anbi12d 630	. . . . . 6 |- (f = {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> ((A.x e. B E*y{x, y} e. f /\ A.x e. A E.y e. B {y, x} e. f) <-> (A.x e. B E*y{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)})))
20	11, 19	cla4ev 1872	. . . . 5 |- ((A.x e. B E*y{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{x, y} e. f /\ A.x e. A E.y e. B {y, x} e. f))
21		incom 2211	. . . . . . . . . . . . . . . . 17 |- (B i^i A) = (A i^i B)
22		brdom7disj.3	. . . . . . . . . . . . . . . . 17 |- (A i^i B) = (/)
23	21, 22	eqtr 1498	. . . . . . . . . . . . . . . 16 |- (B i^i A) = (/)
24		disjne 2319	. . . . . . . . . . . . . . . 16 |- (((B i^i A) = (/) /\ x e. B /\ w e. A) -> x =/= w)
25	23, 24	mp3an1 905	. . . . . . . . . . . . . . 15 |- ((x e. B /\ w e. A) -> x =/= w)
26		visset 1816	. . . . . . . . . . . . . . . 16 |- x e. V
27		visset 1816	. . . . . . . . . . . . . . . 16 |- y e. V
28		visset 1816	. . . . . . . . . . . . . . . 16 |- z e. V
29		visset 1816	. . . . . . . . . . . . . . . 16 |- w e. V
30	26, 27, 28, 29	opthpr 2489	. . . . . . . . . . . . . . 15 |- (x =/= w -> ({x, y} = {z, w} <-> (x = z /\ y = w)))
31	25, 30	syl 10	. . . . . . . . . . . . . 14 |- ((x e. B /\ w e. A) -> ({x, y} = {z, w} <-> (x = z /\ y = w)))
32		breq12 2629	. . . . . . . . . . . . . . 15 |- ((x = z /\ y = w) -> (xgy <-> zgw))
33	32	biimprd 154	. . . . . . . . . . . . . 14 |- ((x = z /\ y = w) -> (zgw -> xgy))
34	31, 33	syl6bi 214	. . . . . . . . . . . . 13 |- ((x e. B /\ w e. A) -> ({x, y} = {z, w} -> (zgw -> xgy)))
35	34	imp3a 361	. . . . . . . . . . . 12 |- ((x e. B /\ w e. A) -> (({x, y} = {z, w} /\ zgw) -> xgy))
36	35	ex 373	. . . . . . . . . . 11 |- (x e. B -> (w e. A -> (({x, y} = {z, w} /\ zgw) -> xgy)))
37	36	adantrd 393	. . . . . . . . . 10 |- (x e. B -> ((w e. A /\ z e. B) -> (({x, y} = {z, w} /\ zgw) -> xgy)))
38	37	r19.23advv 1752	. . . . . . . . 9 |- (x e. B -> (E.w e. A E.z e. B ({x, y} = {z, w} /\ zgw) -> xgy))
39		zfpair2 2786	. . . . . . . . . 10 |- {x, y} e. V
40		eqeq1 1484	. . . . . . . . . . . . 13 |- (v = {x, y} -> (v = {z, w} <-> {x, y} = {z, w}))
41	40	anbi1d 619	. . . . . . . . . . . 12 |- (v = {x, y} -> ((v = {z, w} /\ <.z, w>. e. g) <-> ({x, y} = {z, w} /\ <.z, w>. e. g)))
42		df-br 2625	. . . . . . . . . . . . 13 |- (zgw <-> <.z, w>. e. g)
43	42	anbi2i 482	. . . . . . . . . . . 12 |- (({x, y} = {z, w} /\ zgw) <-> ({x, y} = {z, w} /\ <.z, w>. e. g))
44	41, 43	syl6bbr 540	. . . . . . . . . . 11 |- (v = {x, y} -> ((v = {z, w} /\ <.z, w>. e. g) <-> ({x, y} = {z, w} /\ zgw)))
45	44	2rexbidv 1684	. . . . . . . . . 10 |- (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} /\ zgw)))
46	39, 45	elab 1900	. . . . . . . . 9 |- ({x, y} e. {v | 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} /\ zgw))
47	38, 46	syl5ib 206	. . . . . . . 8 |- (x e. B -> ({x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> xgy))
48	47	19.21aiv 1288	. . . . . . 7 |- (x e. B -> A.y({x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> xgy))
49		immo 1419	. . . . . . 7 |- (A.y({x, y} e. {v | E.w e. A E.z e. B (v = {z, w} /\ <.z, w>. e. g)} -> xgy) -> (E*y