Theorem mapxpen 4481

Description: Equinumerosity law for double set exponentiation. Proposition 10.45 of [TakeutiZaring] p. 96.

Hypotheses

Ref	Expression
mapxpen.1	|- A e. V
mapxpen.2	|- B e. V
mapxpen.3	|- C e. V

Assertion

Ref	Expression
mapxpen	|- ((A ^m B) ^m C) ~~ (A ^m (B X. C))

Proof of Theorem mapxpen

Step	Hyp	Ref	Expression
1		oprex 3974	. 2 |- ((A ^m B) ^m C) e. V
2		mapxpen.2	. . . 4 |- B e. V
3		mapxpen.3	. . . 4 |- C e. V
4		eqid 1473	. . . 4 |- {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}
5	2, 3, 4	oprabex2 4012	. . 3 |- {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} e. V
6	5	a1i 8	. 2 |- (x e. ((A ^m B) ^m C) -> {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} e. V)
7	3	opabex2 3602	. . 3 |- {<.w, f>. | (w e. C /\ f = {<.z, g>. | (z e. B /\ g = (zyw))})} e. V
8	7	a1i 8	. 2 |- (y e. (A ^m (B X. C)) -> {<.w, f>. | (w e. C /\ f = {<.z, g>. | (z e. B /\ g = (zyw))})} e. V)
9		fvex 3723	. . . . . . . . 9 |- ((x` w)` z) e. V
10	9, 4	fnoprab2 4112	. . . . . . . 8 |- {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} Fn (B X. C)
11		fneq1 3574	. . . . . . . 8 |- (y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} -> (y Fn (B X. C) <-> {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} Fn (B X. C)))
12	10, 11	mpbiri 194	. . . . . . 7 |- (y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} -> y Fn (B X. C))
13	12	adantl 388	. . . . . 6 |- ((x e. ((A ^m B) ^m C) /\ y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}) -> y Fn (B X. C))
14		ax-17 969	. . . . . . . 8 |- (x e. ((A ^m B) ^m C) -> A.z x e. ((A ^m B) ^m C))
15		hboprab1 3984	. . . . . . . . 9 |- (y e. {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} -> A.z y e. {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))})
16	15	hbeleq 1564	. . . . . . . 8 |- (y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} -> A.z y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))})
17	14, 16	hban 1007	. . . . . . 7 |- ((x e. ((A ^m B) ^m C) /\ y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}) -> A.z(x e. ((A ^m B) ^m C) /\ y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}))
18		ax-17 969	. . . . . . . . 9 |- (x e. ((A ^m B) ^m C) -> A.w x e. ((A ^m B) ^m C))
19		hboprab2 3985	. . . . . . . . . 10 |- (y e. {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} -> A.w y e. {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))})
20	19	hbeleq 1564	. . . . . . . . 9 |- (y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} -> A.w y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))})
21	18, 20	hban 1007	. . . . . . . 8 |- ((x e. ((A ^m B) ^m C) /\ y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}) -> A.w(x e. ((A ^m B) ^m C) /\ y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}))
22		ax-17 969	. . . . . . . 8 |- (z e. B -> A.w z e. B)
23		ffvelrn 3805	. . . . . . . . . . . . . . 15 |- (((x` w):B-->A /\ z e. B) -> ((x` w)` z) e. A)
24		mapxpen.1	. . . . . . . . . . . . . . . 16 |- A e. V
25	24, 2	elmap 4324	. . . . . . . . . . . . . . 15 |- ((x` w) e. (A ^m B) <-> (x` w):B-->A)
26	23, 25	sylanb 449	. . . . . . . . . . . . . 14 |- (((x` w) e. (A ^m B) /\ z e. B) -> ((x` w)` z) e. A)
27		ffvelrn 3805	. . . . . . . . . . . . . . 15 |- ((x:C-->(A ^m B) /\ w e. C) -> (x` w) e. (A ^m B))
28		oprex 3974	. . . . . . . . . . . . . . . 16 |- (A ^m B) e. V
29	28, 3	elmap 4324	. . . . . . . . . . . . . . 15 |- (x e. ((A ^m B) ^m C) <-> x:C-->(A ^m B))
30	27, 29	sylanb 449	. . . . . . . . . . . . . 14 |- ((x e. ((A ^m B) ^m C) /\ w e. C) -> (x` w) e. (A ^m B))
31	26, 30	sylan 448	. . . . . . . . . . . . 13 |- (((x e. ((A ^m B) ^m C) /\ w e. C) /\ z e. B) -> ((x` w)` z) e. A)
32	31	an1rs 489	. . . . . . . . . . . 12 |- (((x e. ((A ^m B) ^m C) /\ z e. B) /\ w e. C) -> ((x` w)` z) e. A)
33	32	anasss 440	. . . . . . . . . . 11 |- ((x e. ((A ^m B) ^m C) /\ (z e. B /\ w e. C)) -> ((x` w)` z) e. A)
34	33	adantlr 393	. . . . . . . . . 10 |- (((x e. ((A ^m B) ^m C) /\ y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}) /\ (z e. B /\ w e. C)) -> ((x` w)` z) e. A)
35		opreq 3958	. . . . . . . . . . . . 13 |- (y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} -> (zyw) = (z{<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}w))
36	4	oprabval4g 4022	. . . . . . . . . . . . . 14 |- ((z e. B /\ w e. C /\ ((x` w)` z) e. V) -> (z{<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}w) = ((x` w)` z))
37	9, 36	mp3an3 903	. . . . . . . . . . . . 13 |- ((z e. B /\ w e. C) -> (z{<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}w) = ((x` w)` z))
38	35, 37	sylan9eq 1524	. . . . . . . . . . . 12 |- ((y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} /\ (z e. B /\ w e. C)) -> (zyw) = ((x` w)` z))
39	38	eleq1d 1537	. . . . . . . . . . 11 |- ((y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} /\ (z e. B /\ w e. C)) -> ((zyw) e. A <-> ((x` w)` z) e. A))
40	39	adantll 392	. . . . . . . . . 10 |- (((x e. ((A ^m B) ^m C) /\ y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}) /\ (z e. B /\ w e. C)) -> ((zyw) e. A <-> ((x` w)` z) e. A))
41	34, 40	mpbird 196	. . . . . . . . 9 |- (((x e. ((A ^m B) ^m C) /\ y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))}) /\ (z e. B /\ w e. C)) -> (zyw) e. A)
42	41	exp32 377	. . . . . . . 8 |- ((x e. ((A ^m B) ^m