Theorem eroprf 15735

Description: Functionality of an operation defined on equivalence classes.

Hypotheses

Ref	Expression
eropr.1	|- J = (A/.R)
eropr.2	|- K = (B/.S)
eropr.3	|- (ph -> T e. Z)
eropr.4	|- (ph -> Er R)
eropr.5	|- (ph -> Er S)
eropr.6	|- (ph -> Er T)
eropr.7	|- (ph -> A C_ dom R)
eropr.8	|- (ph -> B C_ dom S)
eropr.9	|- (ph -> C C_ dom T)
eropr.10	|- (ph -> F:(A X. B)-->C)
eropr.11	|- ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> ((rRs /\ tSu) -> (rFt)T(sFu)))
eropr.12	|- G = {<.<.x, y>., z>. | E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T)}
eropr.13	|- (ph -> R e. X)
eropr.14	|- (ph -> S e. Y)
eropr.15	|- L = (C/.T)

Assertion

Ref	Expression
eroprf	|- (ph -> G:(J X. K)-->L)

Distinct variable groups:   A,p,q,r,s,t,u,x,z   B,p,q,r,s,t,u,y,z   R,p,q,r,s,t,u,x,z   S,p,q,r,s,t,u,y,z   T,p,q,r,s,t,u,z   F,p,q,r,s,t,u,z   ph,p,q,r,s,t,u,z   J,p,q,z   K,p,q,z   x,y,A   x,B   y,R   x,S   x,T,y   x,F,y   ph,x,y   x,J,y   x,K,y

Proof of Theorem eroprf

Step	Hyp	Ref	Expression
1		ffnoprv 4943	. 2 |- (G:(J X. K)-->L <-> (G Fn (J X. K) /\ A.j e. J A.k e. K (jGk) e. L))
2		eropr.1	. . . . . . 7 |- J = (A/.R)
3		eropr.2	. . . . . . 7 |- K = (B/.S)
4		eropr.3	. . . . . . 7 |- (ph -> T e. Z)
5		eropr.4	. . . . . . 7 |- (ph -> Er R)
6		eropr.5	. . . . . . 7 |- (ph -> Er S)
7		eropr.6	. . . . . . 7 |- (ph -> Er T)
8		eropr.7	. . . . . . 7 |- (ph -> A C_ dom R)
9		eropr.8	. . . . . . 7 |- (ph -> B C_ dom S)
10		eropr.9	. . . . . . 7 |- (ph -> C C_ dom T)
11		eropr.10	. . . . . . 7 |- (ph -> F:(A X. B)-->C)
12		eropr.11	. . . . . . 7 |- ((ph /\ ((r e. A /\ s e. A) /\ (t e. B /\ u e. B))) -> ((rRs /\ tSu) -> (rFt)T(sFu)))
13	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12	eropreu 15733	. . . . . 6 |- ((ph /\ (x e. J /\ y e. K)) -> E!zE.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T))
14	13	ex 402	. . . . 5 |- (ph -> ((x e. J /\ y e. K) -> E!zE.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T)))
15	14	19.21aivv 1665	. . . 4 |- (ph -> A.xA.y((x e. J /\ y e. K) -> E!zE.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T)))
16		fnoprabg 4941	. . . 4 |- (A.xA.y((x e. J /\ y e. K) -> E!zE.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))} Fn {<.x, y>. | (x e. J /\ y e. K)})
17	15, 16	syl 12	. . 3 |- (ph -> {<.<.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))} Fn {<.x, y>. | (x e. J /\ y e. K)})
18		eropr.12	. . . . . 6 |- G = {<.<.x, y>., z>. | E.p e. A E.q e. B ((x = [p]R /\ y = [q]S) /\ z = [(pFq)]T)}
19	2, 3, 18	eroprlem 15732	. . . . 5 |- 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))}
20	19	fneq1i 4507	. . . 4 |- (G Fn (J X. K) <-> {<.<.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))} Fn (J X. K))
21		df-xp 4000	. . . . 5 |- (J X. K) = {<.x, y>. | (x e. J /\ y e. K)}
22	21	fneq2i 4508	. . . 4 |- ({<.<.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))} Fn (J X. K) <-> {<.<.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))} Fn {<.x, y>. | (x e. J /\ y e. K)})
23	20, 22	bitri 190	. . 3 |- (G Fn (J X. K) <-> {<.<.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))} Fn {<.x, y>. | (x e. J /\ y e. K)})
24	17, 23	sylibr 217	. 2 |- (ph -> G Fn (J X. K))
25		opreq12 4891	. . . . . . . . 9 |- ((j = [m]R /\ k = [n]S) -> (jGk) = ([m]RG[n]S))
26	25	eleq1d 1963	. . . . . . . 8 |- ((j = [m]R /\ k = [n]S) -> ((jGk) e. L <-> ([m]RG[n]S) e. L))
27		eropr.13	. . . . . . . . . . 11 |- (ph -> R e. X)
28		eropr.14	. . . . . . . . . . 11 |- (ph -> S e. Y)
29	2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 18, 27, 28	eroprv 15734	. . . . . . . . . 10 |- ((ph /\ m e. A /\ n e. B) -> ([m]RG[n]S) = [(mFn)]T)
30	29	3expb 1068	. . . . . . . . 9 |- ((ph /\ (m e. A /\ n e. B)) -> ([m]RG[n]S) = [(mFn)]T)
31		foprrn 4965	. . . . . . . . . . . . 13 |- ((F:(A X. B)-->C /\ m e. A /\ n e. B) -> (mFn) e. C)
32	31	3expb 1068	. . . . . . . . . . . 12 |- ((F:(A X. B)-->C /\ (m e. A /\ n e. B)) -> (mFn) e. C)
33	32, 11	sylan 497	. . . . . . . . . . 11 |- ((ph /\ (m e. A /\ n e. B)) -> (mFn) e. C)
34		ecelqsg 15731	. . . . . . . . . . . 12 |- ((T e. Z /\ (mFn) e. C) -> [(mFn)]T e. (C/.T))
35	34, 4	sylan 497	. . . . . . . . . . 11 |- ((ph /\ (mFn) e. C) -> [(mFn)]T e. (C/.T))
36	33, 35	syldan 516	. . . . . . . . . 10 |- ((ph /\ (m e. A /\ n e. B)) -> [(mFn)]T e. (C/.T))
37		eropr.15	. . . . . . . . . 10 |- L = (C/.T)
38	36, 37	syl6eleqr 1982	. . . . . . . . 9 |- ((ph /\ (m e. A /\ n e. B)) -> [(mFn)]T e. L)
39	30, 38	eqeltrd 1971	. . . . . . . 8 |- ((ph /\ (m e. A /\ n e. B)) -> ([m]RG[n]S) e. L)
40	26, 39	syl5cbir 228	. . . . . . 7 |- ((ph /\ (m e. A /\ n e. B)) -> ((j = [m]R /\ k = [n]S) -> (jGk) e. L))
41	40	ex 402	. . . . . 6 |- (ph -> ((m e. A /\ n e. B) -> ((j = [m]R /\ k = [n]S) -> (jGk) e. L)))
42	41	r19.23advv 2218	. . . . 5 |- (ph -> (E.m e. A E.n e. B (j = [m]R /\ k = [n]S) -> (jGk) e. L))
43		reeanv 2249	. . . . 5 |- (E.m e. A E.n e. B (j = [m]R /\ k = [n]S) <-> (E.m e. A j = [m]R /\ E.n e. B k = [n]S))
44	42, 43	syl5ibr 224	. . . 4 |- (ph -> ((E.m e. A j = [m]R /\ E.n e. B k = [n]S) -> (jGk) e. L))
45	2	eleq2i 1961	. . . . . 6 |- (j e. J <-> j e. (A/.R))
46		visset 2295	. . . . . . 7 |- j e. _V
47	46	elqs 5348	. . . . . 6 |- (j e. (A/.R) <-> E.m e. A j = [m]R)
48	45, 47	bitri 190	. . . . 5 |- (j e. J <-> E.m e. A j = [m]R)
49	3	eleq2i 1961	. . . . . 6 |- (k e. K <-> k e. (B/.S))
50		visset 2295	. . . . . . 7 |- k e. _V
51	50	elqs 5348	. . . . . 6 |- (k e. (B/.S) <-> E.n e. B k = [n]S)
52	49, 51	bitri 190	. . . . 5 |- (k e. K <-> E.n e. B k = [n]S)
53	48, 52	anbi12i 540	. . . 4 |- ((j e. J /\ k e. K) <-> (E.m e. A j = [m]R /\ E.n e. B k = [n]S))
54	44, 53	syl5ib 223	. . 3 |- (ph -> ((j e. J /\ k e. K) -> (jGk) e. L))
55	54	r19.21aivv 2183	. 2 |- (ph -> A.j e. J A.k e. K (jGk) e. L)
56	1, 24, 55	sylanbrc 527	1 |- (ph -> G:(J X. K)-->L)

Syntax hints:   -> wi 3   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E!weu 1771  A.wral 2105  E.wrex 2106   C_ wss 2593   class class class wbr 3338  {copab 3395   X. cxp 3984  dom cdm 3986   Fn wfn 3993  -->wf 3994  (class class class)co 4884  {copab2 4885  Er wer 5315  [cec 5316  /.cqs 5317

This theorem is referenced by:  eroprf2 15737

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-13 1311  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  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  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-if 2983  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fv 4014  df-opr 4886  df-oprab 4887  df-er 5318  df-ec 5320  df-qs 5323

Copyright terms: Public domain