Theorem mapxpen 3390

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 3018	. 2 |- ((A ^m B) ^m C) e. V
2		mapxpen.2	. . . 4 |- B e. V
3		mapxpen.3	. . . 4 |- C e. V
4		cleqid 1102	. . . 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 3045	. . 3 |- {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} e. V
6	5	a1i 7	. 2 |- (x e. ((A ^m B) ^m C) -> {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} e. V)
7		moeq 1431	. . . . 5 |- E*f f = {<.z, g>. | (z e. B /\ g = (zyw))}
8	7	a1i 7	. . . 4 |- (w e. C -> E*f f = {<.z, g>. | (z e. B /\ g = (zyw))})
9	3, 8	funopabex 2742	. . 3 |- {<.w, f>. | (w e. C /\ f = {<.z, g>. | (z e. B /\ g = (zyw))})} e. V
10	9	a1i 7	. 2 |- (y e. (A ^m (B X. C)) -> {<.w, f>. | (w e. C /\ f = {<.z, g>. | (z e. B /\ g = (zyw))})} e. V)
11		fvex 2838	. . . . . . . . 9 |- ((x` w)` z) e. V
12	11, 4	fnoprab2 3039	. . . . . . . 8 |- {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} Fn (B X. C)
13		fneq1 2718	. . . . . . . 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)))
14	12, 13	mpbiri 169	. . . . . . 7 |- (y = {<.<.z, w>., v>. | ((z e. B /\ w e. C) /\ v = ((x` w)` z))} -> y Fn (B X. C))
15	14	adantl 305	. . . . . 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))
16		ax-17 925	. . . . . . . 8 |- (x e. ((A ^m B) ^m C) -> A.z x e. ((A ^m B) ^m C))
17		hboprab1 3023	. . . . . . . . 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))})
18	17	hbeleq 1173	. . . . . . . 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))})
19	16, 18	hban 704	. . . . . . 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))}))
20		ax-17 925	. . . . . . . . 9 |- (x e. ((A ^m B) ^m C) -> A.w x e. ((A ^m B) ^m C))
21		hboprab2 3024	. . . . . . . . . 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))})
22	21	hbeleq 1173	. . . . . . . . 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))})
23	20, 22	hban 704	. . . . . . . 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))}))
24		ax-17 925	. . . . . . . 8 |- (z e. B -> A.w z e. B)
25		ffvrn 2890	. . . . . . . . . . . . . . 15 |- (((x` w):B-->A /\ z e. B) -> ((x` w)` z) e. A)
26		mapxpen.1	. . . . . . . . . . . . . . . 16 |- A e. V
27	26, 2	elmap 3265	. . . . . . . . . . . . . . 15 |- ((x` w) e. (A ^m B) <-> (x` w):B-->A)
28	25, 27	sylanb 344	. . . . . . . . . . . . . 14 |- (((x` w) e. (A ^m B) /\ z e. B) -> ((x` w)` z) e. A)
29		ffvrn 2890	. . . . . . . . . . . . . . 15 |- ((x:C-->(A ^m B) /\ w e. C) -> (x` w) e. (A ^m B))
30		oprex 3018	. . . . . . . . . . . . . . . 16 |- (A ^m B) e. V
31	30, 3	elmap 3265	. . . . . . . . . . . . . . 15 |- (x e. ((A ^m B) ^m C) <-> x:C-->(A ^m B))
32	29, 31	sylanb 344	. . . . . . . . . . . . . 14 |- ((x e. ((A ^m B) ^m C) /\ w e. C) -> (x` w) e. (A ^m B))
33	28, 32	sylan 343	. . . . . . . . . . . . 13 |- (((x e. ((A ^m B) ^m C) /\ w e. C) /\ z e. B) -> ((x` w)` z) e. A)
34	33	an1rs 373	. . . . . . . . . . . 12 |- (((x e. ((A ^m B) ^m C) /\ z e. B) /\ w e. C) -> ((x` w)` z) e. A)
35	34	anasss 337	. . . . . . . . . . 11 |- ((x e. ((A ^m B) ^m C) /\ (z e. B /\ w e. C)) -> ((x` w)` z) e. A)
36	35	adantlr 310	. . . . . . . . . 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)
37		opreq 3005	. . . . . . . . . . . . 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))
38	4	oprabval4g 3053	. . . . . . . . . . . . . 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))
39	11, 38	mp3an3 641	. . . . . . . . . . . . 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))
40	37, 39	sylan9eq 1144	. . . . . . . . . . . 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))
41	40	eleq1d 1155	. . . . . . . . . . 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))
42	41	adantll 309	. . . . . . . . . 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))
43	36, 42	mpbird 171	. . . . . . . . 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)