Theorem oprabopabf 10157

Description: Convert between operator and function class abstractions using 1st and 2nd. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
oprabopabf.1	|- (ps -> A.xps)
oprabopabf.2	|- (ch -> A.ych)
oprabopabf.3	|- (x = (1st` w) -> (ph <-> ps))
oprabopabf.4	|- (y = (2nd` w) -> (ps <-> ch))

Assertion

Ref	Expression
oprabopabf	|- {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)} = {<.w, z>. | (w e. (A X. B) /\ ch)}

Distinct variable groups:   w,A,x,y,z   w,B,x,y,z   ph,w

Proof of Theorem oprabopabf

Step	Hyp	Ref	Expression
1		ax-17 1317	. . . . . . . . 9 |- (u = <.w, z>. -> A.x u = <.w, z>.)
2		ax-17 1317	. . . . . . . . . 10 |- (w e. (A X. B) -> A.x w e. (A X. B))
3		fvex 4689	. . . . . . . . . . . 12 |- (2nd` w) e. _V
4	3	isseti 2297	. . . . . . . . . . 11 |- E.y y = (2nd` w)
5		oprabopabf.2	. . . . . . . . . . . . 13 |- (ch -> A.ych)
6	5	hbal 1352	. . . . . . . . . . . . 13 |- (A.xch -> A.yA.xch)
7	5, 6	hbim 1354	. . . . . . . . . . . 12 |- ((ch -> A.xch) -> A.y(ch -> A.xch))
8		oprabopabf.1	. . . . . . . . . . . . 13 |- (ps -> A.xps)
9		oprabopabf.4	. . . . . . . . . . . . . 14 |- (y = (2nd` w) -> (ps <-> ch))
10	9	albidv 1656	. . . . . . . . . . . . . 14 |- (y = (2nd` w) -> (A.xps <-> A.xch))
11	9, 10	imbi12d 688	. . . . . . . . . . . . 13 |- (y = (2nd` w) -> ((ps -> A.xps) <-> (ch -> A.xch)))
12	8, 11	mpbii 210	. . . . . . . . . . . 12 |- (y = (2nd` w) -> (ch -> A.xch))
13	7, 12	19.23ai 1412	. . . . . . . . . . 11 |- (E.y y = (2nd` w) -> (ch -> A.xch))
14	4, 13	ax-mp 7	. . . . . . . . . 10 |- (ch -> A.xch)
15	2, 14	hban 1356	. . . . . . . . 9 |- ((w e. (A X. B) /\ ch) -> A.x(w e. (A X. B) /\ ch))
16	1, 15	hban 1356	. . . . . . . 8 |- ((u = <.w, z>. /\ (w e. (A X. B) /\ ch)) -> A.x(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
17	16	hbex 1353	. . . . . . 7 |- (E.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)) -> A.xE.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
18		ax-17 1317	. . . . . . . . . 10 |- (u = <.w, z>. -> A.y u = <.w, z>.)
19		ax-17 1317	. . . . . . . . . . 11 |- (w e. (A X. B) -> A.y w e. (A X. B))
20	19, 5	hban 1356	. . . . . . . . . 10 |- ((w e. (A X. B) /\ ch) -> A.y(w e. (A X. B) /\ ch))
21	18, 20	hban 1356	. . . . . . . . 9 |- ((u = <.w, z>. /\ (w e. (A X. B) /\ ch)) -> A.y(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
22	21	hbex 1353	. . . . . . . 8 |- (E.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)) -> A.yE.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
23		opex 3527	. . . . . . . . . 10 |- <.x, y>. e. _V
24		opeq1 3158	. . . . . . . . . . . 12 |- (w = <.x, y>. -> <.w, z>. = <.<.x, y>., z>.)
25	24	eqeq2d 1895	. . . . . . . . . . 11 |- (w = <.x, y>. -> (u = <.w, z>. <-> u = <.<.x, y>., z>.))
26		eleq1 1957	. . . . . . . . . . . 12 |- (w = <.x, y>. -> (w e. (A X. B) <-> <.x, y>. e. (A X. B)))
27		fveq2 4681	. . . . . . . . . . . . . . 15 |- (w = <.x, y>. -> (1st` w) = (1st` <.x, y>.))
28		visset 2295	. . . . . . . . . . . . . . . 16 |- x e. _V
29	28	op1st 5026	. . . . . . . . . . . . . . 15 |- (1st` <.x, y>.) = x
30	27, 29	syl6req 1945	. . . . . . . . . . . . . 14 |- (w = <.x, y>. -> x = (1st` w))
31		oprabopabf.3	. . . . . . . . . . . . . 14 |- (x = (1st` w) -> (ph <-> ps))
32	30, 31	syl 12	. . . . . . . . . . . . 13 |- (w = <.x, y>. -> (ph <-> ps))
33		fveq2 4681	. . . . . . . . . . . . . . 15 |- (w = <.x, y>. -> (2nd` w) = (2nd` <.x, y>.))
34		visset 2295	. . . . . . . . . . . . . . . 16 |- y e. _V
35	28, 34	op2nd 5027	. . . . . . . . . . . . . . 15 |- (2nd` <.x, y>.) = y
36	33, 35	syl6req 1945	. . . . . . . . . . . . . 14 |- (w = <.x, y>. -> y = (2nd` w))
37	36, 9	syl 12	. . . . . . . . . . . . 13 |- (w = <.x, y>. -> (ps <-> ch))
38	32, 37	bitr2d 588	. . . . . . . . . . . 12 |- (w = <.x, y>. -> (ch <-> ph))
39	26, 38	anbi12d 690	. . . . . . . . . . 11 |- (w = <.x, y>. -> ((w e. (A X. B) /\ ch) <-> (<.x, y>. e. (A X. B) /\ ph)))
40	25, 39	anbi12d 690	. . . . . . . . . 10 |- (w = <.x, y>. -> ((u = <.w, z>. /\ (w e. (A X. B) /\ ch)) <-> (u = <.<.x, y>., z>. /\ (<.x, y>. e. (A X. B) /\ ph))))
41	23, 40	cla4ev 2371	. . . . . . . . 9 |- ((u = <.<.x, y>., z>. /\ (<.x, y>. e. (A X. B) /\ ph)) -> E.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
42		opelxpi 4040	. . . . . . . . 9 |- ((x e. A /\ y e. B) -> <.x, y>. e. (A X. B))
43	41, 42	sylanr1 511	. . . . . . . 8 |- ((u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) -> E.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
44	22, 43	19.23ai 1412	. . . . . . 7 |- (E.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) -> E.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
45	17, 44	19.23ai 1412	. . . . . 6 |- (E.xE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) -> E.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
46		relxp 4088	. . . . . . . . . . . . 13 |- Rel (A X. B)
47		1st2nd 5048	. . . . . . . . . . . . 13 |- ((Rel (A X. B) /\ w e. (A X. B)) -> w = <.(1st` w), (2nd` w)>.)
48	46, 47	mpan 759	. . . . . . . . . . . 12 |- (w e. (A X. B) -> w = <.(1st` w), (2nd` w)>.)
49	48	opeq1d 3164	. . . . . . . . . . 11 |- (w e. (A X. B) -> <.w, z>. = <.<.(1st` w), (2nd` w)>., z>.)
50	49	eqeq2d 1895	. . . . . . . . . 10 |- (w e. (A X. B) -> (u = <.w, z>. <-> u = <.<.(1st` w), (2nd` w)>., z>.))
51	50	biimpac 462	. . . . . . . . 9 |- ((u = <.w, z>. /\ w e. (A X. B)) -> u = <.<.(1st` w), (2nd` w)>., z>.)
52	51	adantrr 431	. . . . . . . 8 |- ((u = <.w, z>. /\ (w e. (A X. B) /\ ch)) -> u = <.<.(1st` w), (2nd` w)>., z>.)
53		xp1st 10155	. . . . . . . . . 10 |- (w e. (A X. B) -> (1st` w) e. A)
54		xp2nd 10156	. . . . . . . . . 10 |- (w e. (A X. B) -> (2nd` w) e. B)
55	53, 54	jca 310	. . . . . . . . 9 |- (w e. (A X. B) -> ((1st` w) e. A /\ (2nd` w) e. B))
56	55	ad2antrl 442	. . . . . . . 8 |- ((u = <.w, z>. /\ (w e. (A X. B) /\ ch)) -> ((1st` w) e. A /\ (2nd` w) e. B))
57		simprr 451	. . . . . . . 8 |- ((u = <.w, z>. /\ (w e. (A X. B) /\ ch)) -> ch)
58		ax-17 1317	. . . . . . . . . . . 12 |- (v e. (2nd` w) -> A.y v e. (2nd` w))
59		ax-17 1317	. . . . . . . . . . . . 13 |- (u = <.<.(1st` w), (2nd` w)>., z>. -> A.y u = <.<.(1st` w), (2nd` w)>., z>.)
60		ax-17 1317	. . . . . . . . . . . . . 14 |- (((1st` w) e. A /\ (2nd` w) e. B) -> A.y((1st` w) e. A /\ (2nd` w) e. B))
61	60, 5	hban 1356	. . . . . . . . . . . . 13 |- ((((1st` w) e. A /\ (2nd` w) e. B) /\ ch) -> A.y(((1st` w) e. A /\ (2nd` w) e. B) /\ ch))
62	59, 61	hban 1356	. . . . . . . . . . . 12 |- ((u = <.<.(1st` w), (2nd` w)>., z>. /\ (((1st` w) e. A /\ (2nd` w) e. B) /\ ch)) -> A.y(u = <.<.(1st` w), (2nd` w)>., z>. /\ (((1st` w) e. A /\ (2nd` w) e. B) /\ ch)))
63		opeq2 3159	. . . . . . . . . . . . . . 15 |- (y = (2nd` w) -> <.(1st` w), y>. = <.(1st` w), (2nd` w)>.)
64	63	opeq1d 3164	. . . . . . . . . . . . . 14 |- (y = (2nd` w) -> <.<.(1st` w), y>., z>. = <.<.(1st` w), (2nd` w)>., z>.)
65	64	eqeq2d 1895	. . . . . . . . . . . . 13 |- (y = (2nd` w) -> (u = <.<.(1st` w), y>., z>. <-> u = <.<.(1st` w), (2nd` w)>., z>.))
66		eleq1 1957	. . . . . . . . . . . . . . 15 |- (y = (2nd` w) -> (y e. B <-> (2nd` w) e. B))
67	66	anbi2d 678	. . . . . . . . . . . . . 14 |- (y = (2nd` w) -> (((1st` w) e. A /\ y e. B) <-> ((1st` w) e. A /\ (2nd` w) e. B)))
68	67, 9	anbi12d 690	. . . . . . . . . . . . 13 |- (y = (2nd` w) -> ((((1st` w) e. A /\ y e. B) /\ ps) <-> (((1st` w) e. A /\ (2nd` w) e. B) /\ ch)))
69	65, 68	anbi12d 690	. . . . . . . . . . . 12 |- (y = (2nd` w) -> ((u = <.<.(1st` w), y>., z>. /\ (((1st` w) e. A /\ y e. B) /\ ps)) <-> (u = <.<.(1st` w), (2nd` w)>., z>. /\ (((1st` w) e. A /\ (2nd` w) e. B) /\ ch))))
70	58, 62, 69	cla4egf 2362	. . . . . . . . . . 11 |- ((2nd` w) e. _V -> ((u = <.<.(1st` w), (2nd` w)>., z>. /\ (((1st` w) e. A /\ (2nd` w) e. B) /\ ch)) -> E.y(u = <.<.(1st` w), y>., z>. /\ (((1st` w) e. A /\ y e. B) /\ ps))))
71	3, 70	ax-mp 7	. . . . . . . . . 10 |- ((u = <.<.(1st` w), (2nd` w)>., z>. /\ (((1st` w) e. A /\ (2nd` w) e. B) /\ ch)) -> E.y(u = <.<.(1st` w), y>., z>. /\ (((1st` w) e. A /\ y e. B) /\ ps)))
72		fvex 4689	. . . . . . . . . . . 12 |- (1st` w) e. _V
73		ax-17 1317	. . . . . . . . . . . . 13 |- (v e. (1st` w) -> A.x v e. (1st` w))
74		ax-17 1317	. . . . . . . . . . . . . 14 |- (u = <.<.(1st` w), y>., z>. -> A.x u = <.<.(1st` w), y>., z>.)
75		ax-17 1317	. . . . . . . . . . . . . . 15 |- (((1st` w) e. A /\ y e. B) -> A.x((1st` w) e. A /\ y e. B))
76	75, 8	hban 1356	. . . . . . . . . . . . . 14 |- ((((1st` w) e. A /\ y e. B) /\ ps) -> A.x(((1st` w) e. A /\ y e. B) /\ ps))
77	74, 76	hban 1356	. . . . . . . . . . . . 13 |- ((u = <.<.(1st` w), y>., z>. /\ (((1st` w) e. A /\ y e. B) /\ ps)) -> A.x(u = <.<.(1st` w), y>., z>. /\ (((1st` w) e. A /\ y e. B) /\ ps)))
78		opeq1 3158	. . . . . . . . . . . . . . . 16 |- (x = (1st` w) -> <.x, y>. = <.(1st` w), y>.)
79	78	opeq1d 3164	. . . . . . . . . . . . . . 15 |- (x = (1st` w) -> <.<.x, y>., z>. = <.<.(1st` w), y>., z>.)
80	79	eqeq2d 1895	. . . . . . . . . . . . . 14 |- (x = (1st` w) -> (u = <.<.x, y>., z>. <-> u = <.<.(1st` w), y>., z>.))
81		eleq1 1957	. . . . . . . . . . . . . . . 16 |- (x = (1st` w) -> (x e. A <-> (1st` w) e. A))
82	81	anbi1d 679	. . . . . . . . . . . . . . 15 |- (x = (1st` w) -> ((x e. A /\ y e. B) <-> ((1st` w) e. A /\ y e. B)))
83	82, 31	anbi12d 690	. . . . . . . . . . . . . 14 |- (x = (1st` w) -> (((x e. A /\ y e. B) /\ ph) <-> (((1st` w) e. A /\ y e. B) /\ ps)))
84	80, 83	anbi12d 690	. . . . . . . . . . . . 13 |- (x = (1st` w) -> ((u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) <-> (u = <.<.(1st` w), y>., z>. /\ (((1st` w) e. A /\ y e. B) /\ ps))))
85	73, 77, 84	cla4egf 2362	. . . . . . . . . . . 12 |- ((1st` w) e. _V -> ((u = <.<.(1st` w), y>., z>. /\ (((1st` w) e. A /\ y e. B) /\ ps)) -> E.x(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph))))
86	72, 85	ax-mp 7	. . . . . . . . . . 11 |- ((u = <.<.(1st` w), y>., z>. /\ (((1st` w) e. A /\ y e. B) /\ ps)) -> E.x(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)))
87	86	eximi 1387	. . . . . . . . . 10 |- (E.y(u = <.<.(1st` w), y>., z>. /\ (((1st` w) e. A /\ y e. B) /\ ps)) -> E.yE.x(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)))
88	71, 87	syl 12	. . . . . . . . 9 |- ((u = <.<.(1st` w), (2nd` w)>., z>. /\ (((1st` w) e. A /\ (2nd` w) e. B) /\ ch)) -> E.yE.x(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)))
89		excom 1393	. . . . . . . . 9 |- (E.yE.x(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) <-> E.xE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)))
90	88, 89	sylib 215	. . . . . . . 8 |- ((u = <.<.(1st` w), (2nd` w)>., z>. /\ (((1st` w) e. A /\ (2nd` w) e. B) /\ ch)) -> E.xE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)))
91	52, 56, 57, 90	syl12anc 1098	. . . . . . 7 |- ((u = <.w, z>. /\ (w e. (A X. B) /\ ch)) -> E.xE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)))
92	91	19.23aiv 1674	. . . . . 6 |- (E.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)) -> E.xE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)))
93	45, 92	impbii 174	. . . . 5 |- (E.xE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) <-> E.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
94	93	exbii 1398	. . . 4 |- (E.zE.xE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) <-> E.zE.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
95		excom 1393	. . . . . 6 |- (E.yE.z(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) <-> E.zE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)))
96	95	exbii 1398	. . . . 5 |- (E.xE.yE.z(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) <-> E.xE.zE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)))
97		excom 1393	. . . . 5 |- (E.xE.zE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) <-> E.zE.xE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)))
98	96, 97	bitri 190	. . . 4 |- (E.xE.yE.z(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) <-> E.zE.xE.y(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)))
99		excom 1393	. . . 4 |- (E.wE.z(u = <.w, z>. /\ (w e. (A X. B) /\ ch)) <-> E.zE.w(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
100	94, 98, 99	3bitr4i 200	. . 3 |- (E.xE.yE.z(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph)) <-> E.wE.z(u = <.w, z>. /\ (w e. (A X. B) /\ ch)))
101	100	abbii 2006	. 2 |- {u | E.xE.yE.z(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph))} = {u | E.wE.z(u = <.w, z>. /\ (w e. (A X. B) /\ ch))}
102		df-oprab 4887	. 2 |- {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)} = {u | E.xE.yE.z(u = <.<.x, y>., z>. /\ ((x e. A /\ y e. B) /\ ph))}
103		df-opab 3396	. 2 |- {<.w, z>. | (w e. (A X. B) /\ ch)} = {u | E.wE.z(u = <.w, z>. /\ (w e. (A X. B) /\ ch))}
104	101, 102, 103	3eqtr4i 1921	1 |- {<.<.x, y>., z>. | ((x e. A /\ y e. B) /\ ph)} = {<.w, z>. | (w e. (A X. B) /\ ch)}

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240  A.wal 1296   = wceq 1298   e. wcel 1300  E.wex 1326  {cab 1871  _Vcvv 2292  <.cop 3046  {copab 3395   X. cxp 3984  Rel wrel 3991  ` cfv 3998  {copab2 4885  1stc1st 5018  2ndc2nd 5019

This theorem is referenced by:  oprabopab 10158  oprabco 10159

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-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-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-fv 4014  df-oprab 4887  df-1st 5020  df-2nd 5021

Copyright terms: Public domain