Theorem dmmulpq 6357

Description: Domain of multiplication on positive fractions. (Contributed by NM, 24-Aug-1995.)

Assertion

Ref	Expression
dmmulpq	|- dom .Q = ( Q. X. Q.)

Proof of Theorem dmmulpq

Dummy variables x y z v w u f are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dmoprab 5524	. . 3 |- dom { <. <.x , y >. , z >. | ((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q )) } = { <.x , y >. | E.z((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q )) }
2		df-mqqs 6327	. . . 4 |- .Q = { <. <.x , y >. , z >. | ((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q )) }
3	2	dmeqi 4478	. . 3 |- dom .Q = dom { <. <.x , y >. , z >. | ((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q )) }
4		dmaddpqlem 6354	. . . . . . . . 9 |- (x e. Q. -> E.wE.v x = [ <.w , v >.] ~Q )
5		dmaddpqlem 6354	. . . . . . . . 9 |- (y e. Q. -> E.uE.f y = [ <.u , f >.] ~Q )
6	4, 5	anim12i 321	. . . . . . . 8 |- ((x e. Q. /\ y e. Q.) -> (E.wE.v x = [ <.w , v >.] ~Q /\ E.uE.f y = [ <.u , f >.] ~Q ))
7		ee4anv 1806	. . . . . . . 8 |- (E.wE.vE.uE.f(x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) <-> (E.wE.v x = [ <.w , v >.] ~Q /\ E.uE.f y = [ <.u , f >.] ~Q ))
8	6, 7	sylibr 137	. . . . . . 7 |- ((x e. Q. /\ y e. Q.) -> E.wE.vE.uE.f(x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ))
9		enqex 6337	. . . . . . . . . . . . . 14 |- ~Q e. _V
10		ecexg 6039	. . . . . . . . . . . . . 14 |- ( ~Q e. _V -> [( <.w , v >. .pQ <.u , f >.)] ~Q e. _V)
11	9, 10	ax-mp 7	. . . . . . . . . . . . 13 |- [( <.w , v >. .pQ <.u , f >.)] ~Q e. _V
12	11	isseti 2557	. . . . . . . . . . . 12 |- E.z z = [( <.w , v >. .pQ <.u , f >.)] ~Q
13		ax-ia3 101	. . . . . . . . . . . . 13 |- ((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) -> (z = [( <.w , v >. .pQ <.u , f >.)] ~Q -> ((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q )))
14	13	eximdv 1757	. . . . . . . . . . . 12 |- ((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) -> (E.z z = [( <.w , v >. .pQ <.u , f >.)] ~Q -> E.z((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q )))
15	12, 14	mpi 15	. . . . . . . . . . 11 |- ((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) -> E.z((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q ))
16	15	2eximi 1489	. . . . . . . . . 10 |- (E.uE.f(x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) -> E.uE.fE.z((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q ))
17		exrot3 1577	. . . . . . . . . 10 |- (E.zE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q ) <-> E.uE.fE.z((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q ))
18	16, 17	sylibr 137	. . . . . . . . 9 |- (E.uE.f(x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) -> E.zE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q ))
19	18	2eximi 1489	. . . . . . . 8 |- (E.wE.vE.uE.f(x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) -> E.wE.vE.zE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q ))
20		exrot3 1577	. . . . . . . 8 |- (E.zE.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q ) <-> E.wE.vE.zE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q ))
21	19, 20	sylibr 137	. . . . . . 7 |- (E.wE.vE.uE.f(x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) -> E.zE.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q ))
22	8, 21	syl 14	. . . . . 6 |- ((x e. Q. /\ y e. Q.) -> E.zE.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q ))
23	22	pm4.71i 371	. . . . 5 |- ((x e. Q. /\ y e. Q.) <-> ((x e. Q. /\ y e. Q.) /\ E.zE.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q )))
24		19.42v 1783	. . . . 5 |- (E.z((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q )) <-> ((x e. Q. /\ y e. Q.) /\ E.zE.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q )))
25	23, 24	bitr4i 176	. . . 4 |- ((x e. Q. /\ y e. Q.) <-> E.z((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q )))
26	25	opabbii 3814	. . 3 |- { <.x , y >. | (x e. Q. /\ y e. Q.) } = { <.x , y >. | E.z((x e. Q. /\ y e. Q.) /\ E.wE.vE.uE.f((x = [ <.w , v >.] ~Q /\ y = [ <.u , f >.] ~Q ) /\ z = [( <.w , v >. .pQ <.u , f >.)] ~Q )) }
27	1, 3, 26	3eqtr4i 2067	. 2 |- dom .Q = { <.x , y >. | (x e. Q. /\ y e. Q.) }
28		df-xp 4293	. 2 |- ( Q. X. Q.) = { <.x , y >. | (x e. Q. /\ y e. Q.) }
29	27, 28	eqtr4i 2060	1 |- dom .Q = ( Q. X. Q.)

Syntax hints:   /\ wa 97   = wceq 1242  E.wex 1378   e. wcel 1390   _Vcvv 2551   <.cop 3369   {copab 3807   X. cxp 4285   dom cdm 4287  (class class class)co 5452   {coprab 5453  [cec 6033   .pQ cmpq 6254   ~Q ceq 6256   Q.cnq 6257   .Q cmq 6260

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 629  ax-5 1333  ax-7 1334  ax-gen 1335  ax-ie1 1379  ax-ie2 1380  ax-8 1392  ax-10 1393  ax-11 1394  ax-i12 1395  ax-bnd 1396  ax-4 1397  ax-13 1401  ax-14 1402  ax-17 1416  ax-i9 1420  ax-ial 1424  ax-i5r 1425  ax-ext 2019  ax-sep 3865  ax-pow 3917  ax-pr 3934  ax-un 4135  ax-iinf 4253

This theorem depends on definitions:  df-bi 110  df-3an 886  df-tru 1245  df-nf 1347  df-sb 1643  df-eu 1900  df-mo 1901  df-clab 2024  df-cleq 2030  df-clel 2033  df-nfc 2164  df-ral 2305  df-rex 2306  df-v 2553  df-dif 2914  df-un 2916  df-in 2918  df-ss 2925  df-pw 3352  df-sn 3372  df-pr 3373  df-op 3375  df-uni 3571  df-int 3606  df-br 3755  df-opab 3809  df-iom 4256  df-xp 4293  df-cnv 4295  df-dm 4297  df-rn 4298  df-res 4299  df-ima 4300  df-oprab 5456  df-ec 6037  df-qs 6041  df-ni 6281  df-enq 6324  df-nqqs 6325  df-mqqs 6327

This theorem is referenced by: (None)