Theorem eroprlem 15732

Description: Lemma for eroprv 15734 and eroprf 15735.

Hypotheses

Ref	Expression
eroprlem.1	|- J = (A/.R)
eroprlem.2	|- K = (B/.S)
eroprlem.3	|- G = {<.<.x, y>., z>. | E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T)}

Assertion

Ref	Expression
eroprlem	|- G = {<.<.x, y>., z>. | ((x e. J /\ y e. K) /\ E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))}

Distinct variable groups:   A,p,q,x   B,p,q,y   R,p,q,x   S,p,q,y   x,y,z

Proof of Theorem eroprlem

Step	Hyp	Ref	Expression
1		eroprlem.3	. 2 |- G = {<.<.x, y>., z>. | E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T)}
2		simpl 346	. . . . . . 7 |- (((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) -> (x = [p]R /\ y = [q]S))
3	2	reximi 2198	. . . . . 6 |- (E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) -> E.q e. B (x = [p]R /\ y = [q]S))
4	3	reximi 2198	. . . . 5 |- (E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) -> E.p e. A E.q e. B (x = [p]R /\ y = [q]S))
5		eroprlem.1	. . . . . . . . 9 |- J = (A/.R)
6	5	eleq2i 1961	. . . . . . . 8 |- (x e. J <-> x e. (A/.R))
7		df-qs 5323	. . . . . . . . 9 |- (A/.R) = {x | E.p e. A x = [p]R}
8	7	abeq2i 2001	. . . . . . . 8 |- (x e. (A/.R) <-> E.p e. A x = [p]R)
9	6, 8	bitri 190	. . . . . . 7 |- (x e. J <-> E.p e. A x = [p]R)
10		eroprlem.2	. . . . . . . . 9 |- K = (B/.S)
11	10	eleq2i 1961	. . . . . . . 8 |- (y e. K <-> y e. (B/.S))
12		df-qs 5323	. . . . . . . . 9 |- (B/.S) = {y | E.q e. B y = [q]S}
13	12	abeq2i 2001	. . . . . . . 8 |- (y e. (B/.S) <-> E.q e. B y = [q]S)
14	11, 13	bitri 190	. . . . . . 7 |- (y e. K <-> E.q e. B y = [q]S)
15	9, 14	anbi12i 540	. . . . . 6 |- ((x e. J /\ y e. K) <-> (E.p e. A x = [p]R /\ E.q e. B y = [q]S))
16		reeanv 2249	. . . . . 6 |- (E.p e. A E.q e. B (x = [p]R /\ y = [q]S) <-> (E.p e. A x = [p]R /\ E.q e. B y = [q]S))
17	15, 16	bitr4i 193	. . . . 5 |- ((x e. J /\ y e. K) <-> E.p e. A E.q e. B (x = [p]R /\ y = [q]S))
18	4, 17	sylibr 217	. . . 4 |- (E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) -> (x e. J /\ y e. K))
19	18	pm4.71ri 700	. . 3 |- (E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T) <-> ((x e. J /\ y e. K) /\ E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T)))
20	19	oprabbii 4923	. 2 |- {<.<.x, y>., z>. | E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T)} = {<.<.x, y>., z>. | ((x e. J /\ y e. K) /\ E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))}
21	1, 20	eqtri 1908	1 |- G = {<.<.x, y>., z>. | ((x e. J /\ y e. K) /\ E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))}

Syntax hints:   /\ wa 240   = wceq 1298   e. wcel 1300  E.wrex 2106  (class class class)co 4884  {copab2 4885  [cec 5316  /.cqs 5317

This theorem is referenced by:  eroprv 15734  eroprf 15735

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-ex 1327  df-sb 1536  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-opab 3396  df-oprab 4887  df-qs 5323

Copyright terms: Public domain