mapxpen

Description: Equinumerosity law for double set exponentiation. Proposition 10.45 of TakeutiZaring p. 96. (Contributed by NM, 21-Feb-2004) (Revised by Mario Carneiro, 24-Jun-2015)

		Ref	Expression
	Assertion	mapxpen	$⊢ (A \in V \land B \in W \land C \in X) \to ({(A^{B})}^{C}) \approx (A^{(B \times C)})$

Proof

Step	Hyp	Ref	Expression
1		ovexd	$⊢ (A \in V \land B \in W \land C \in X) \to {(A^{B})}^{C} \in V$
2		ovexd	$⊢ (A \in V \land B \in W \land C \in X) \to A^{(B \times C)} \in V$
3		elmapi	$⊢ f \in ({(A^{B})}^{C}) \to f : C ⟶ A^{B}$
4	3	ffvelrnda	$⊢ (f \in ({(A^{B})}^{C}) \land y \in C) \to f (y) \in (A^{B})$
5		elmapi	$⊢ f (y) \in (A^{B}) \to f (y) : B ⟶ A$
6	4 5	syl	$⊢ (f \in ({(A^{B})}^{C}) \land y \in C) \to f (y) : B ⟶ A$
7	6	ffvelrnda	$⊢ ((f \in ({(A^{B})}^{C}) \land y \in C) \land x \in B) \to f (y) (x) \in A$
8	7	an32s	$⊢ ((f \in ({(A^{B})}^{C}) \land x \in B) \land y \in C) \to f (y) (x) \in A$
9	8	ralrimiva	$⊢ (f \in ({(A^{B})}^{C}) \land x \in B) \to \forall y \in C f (y) (x) \in A$
10	9	ralrimiva	$⊢ f \in ({(A^{B})}^{C}) \to \forall x \in B \forall y \in C f (y) (x) \in A$
11		eqid	$⊢ (x \in B, y \in C ⟼ f (y) (x)) = (x \in B, y \in C ⟼ f (y) (x))$
12	11	fmpo	$⊢ \forall x \in B \forall y \in C f (y) (x) \in A \leftrightarrow (x \in B, y \in C ⟼ f (y) (x)) : B \times C ⟶ A$
13	10 12	sylib	$⊢ f \in ({(A^{B})}^{C}) \to (x \in B, y \in C ⟼ f (y) (x)) : B \times C ⟶ A$
14		simp1	$⊢ (A \in V \land B \in W \land C \in X) \to A \in V$
15		xpexg	$⊢ (B \in W \land C \in X) \to B \times C \in V$
16	15	3adant1	$⊢ (A \in V \land B \in W \land C \in X) \to B \times C \in V$
17		elmapg	$⊢ (A \in V \land B \times C \in V) \to ((x \in B, y \in C ⟼ f (y) (x)) \in (A^{(B \times C)}) \leftrightarrow (x \in B, y \in C ⟼ f (y) (x)) : B \times C ⟶ A)$
18	14 16 17	syl2anc	$⊢ (A \in V \land B \in W \land C \in X) \to ((x \in B, y \in C ⟼ f (y) (x)) \in (A^{(B \times C)}) \leftrightarrow (x \in B, y \in C ⟼ f (y) (x)) : B \times C ⟶ A)$
19	13 18	syl5ibr	$⊢ (A \in V \land B \in W \land C \in X) \to (f \in ({(A^{B})}^{C}) \to (x \in B, y \in C ⟼ f (y) (x)) \in (A^{(B \times C)}))$
20		elmapi	$⊢ g \in (A^{(B \times C)}) \to g : B \times C ⟶ A$
21	20	adantl	$⊢ ((A \in V \land B \in W \land C \in X) \land g \in (A^{(B \times C)})) \to g : B \times C ⟶ A$
22		fovrn	$⊢ (g : B \times C ⟶ A \land x \in B \land y \in C) \to x g y \in A$
23	22	3expa	$⊢ ((g : B \times C ⟶ A \land x \in B) \land y \in C) \to x g y \in A$
24	23	an32s	$⊢ ((g : B \times C ⟶ A \land y \in C) \land x \in B) \to x g y \in A$
25	21 24	sylanl1	$⊢ ((((A \in V \land B \in W \land C \in X) \land g \in (A^{(B \times C)})) \land y \in C) \land x \in B) \to x g y \in A$
26	25	fmpttd	$⊢ (((A \in V \land B \in W \land C \in X) \land g \in (A^{(B \times C)})) \land y \in C) \to (x \in B ⟼ x g y) : B ⟶ A$
27		elmapg	$⊢ (A \in V \land B \in W) \to ((x \in B ⟼ x g y) \in (A^{B}) \leftrightarrow (x \in B ⟼ x g y) : B ⟶ A)$
28	27	3adant3	$⊢ (A \in V \land B \in W \land C \in X) \to ((x \in B ⟼ x g y) \in (A^{B}) \leftrightarrow (x \in B ⟼ x g y) : B ⟶ A)$
29	28	ad2antrr	$⊢ (((A \in V \land B \in W \land C \in X) \land g \in (A^{(B \times C)})) \land y \in C) \to ((x \in B ⟼ x g y) \in (A^{B}) \leftrightarrow (x \in B ⟼ x g y) : B ⟶ A)$
30	26 29	mpbird	$⊢ (((A \in V \land B \in W \land C \in X) \land g \in (A^{(B \times C)})) \land y \in C) \to (x \in B ⟼ x g y) \in (A^{B})$
31	30	fmpttd	$⊢ ((A \in V \land B \in W \land C \in X) \land g \in (A^{(B \times C)})) \to (y \in C ⟼ (x \in B ⟼ x g y)) : C ⟶ A^{B}$
32	31	ex	$⊢ (A \in V \land B \in W \land C \in X) \to (g \in (A^{(B \times C)}) \to (y \in C ⟼ (x \in B ⟼ x g y)) : C ⟶ A^{B})$
33		ovex	$⊢ A^{B} \in V$
34		simp3	$⊢ (A \in V \land B \in W \land C \in X) \to C \in X$
35		elmapg	$⊢ (A^{B} \in V \land C \in X) \to ((y \in C ⟼ (x \in B ⟼ x g y)) \in ({(A^{B})}^{C}) \leftrightarrow (y \in C ⟼ (x \in B ⟼ x g y)) : C ⟶ A^{B})$
36	33 34 35	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to ((y \in C ⟼ (x \in B ⟼ x g y)) \in ({(A^{B})}^{C}) \leftrightarrow (y \in C ⟼ (x \in B ⟼ x g y)) : C ⟶ A^{B})$
37	32 36	sylibrd	$⊢ (A \in V \land B \in W \land C \in X) \to (g \in (A^{(B \times C)}) \to (y \in C ⟼ (x \in B ⟼ x g y)) \in ({(A^{B})}^{C}))$
38		elmapfn	$⊢ g \in (A^{(B \times C)}) \to g Fn (B \times C)$
39	38	ad2antll	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to g Fn (B \times C)$
40		fnov	$⊢ g Fn (B \times C) \leftrightarrow g = (x \in B, y \in C ⟼ x g y)$
41	39 40	sylib	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to g = (x \in B, y \in C ⟼ x g y)$
42		simp3	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land x \in B \land y \in C) \to y \in C$
43	26	adantlrl	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land y \in C) \to (x \in B ⟼ x g y) : B ⟶ A$
44	43	3adant2	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land x \in B \land y \in C) \to (x \in B ⟼ x g y) : B ⟶ A$
45		simp1l2	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land x \in B \land y \in C) \to B \in W$
46		simp1l1	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land x \in B \land y \in C) \to A \in V$
47		fex2	$⊢ ((x \in B ⟼ x g y) : B ⟶ A \land B \in W \land A \in V) \to (x \in B ⟼ x g y) \in V$
48	44 45 46 47	syl3anc	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land x \in B \land y \in C) \to (x \in B ⟼ x g y) \in V$
49		eqid	$⊢ (y \in C ⟼ (x \in B ⟼ x g y)) = (y \in C ⟼ (x \in B ⟼ x g y))$
50	49	fvmpt2	$⊢ (y \in C \land (x \in B ⟼ x g y) \in V) \to (y \in C ⟼ (x \in B ⟼ x g y)) (y) = (x \in B ⟼ x g y)$
51	42 48 50	syl2anc	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land x \in B \land y \in C) \to (y \in C ⟼ (x \in B ⟼ x g y)) (y) = (x \in B ⟼ x g y)$
52	51	fveq1d	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land x \in B \land y \in C) \to (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x) = (x \in B ⟼ x g y) (x)$
53		simp2	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land x \in B \land y \in C) \to x \in B$
54		ovex	$⊢ x g y \in V$
55		eqid	$⊢ (x \in B ⟼ x g y) = (x \in B ⟼ x g y)$
56	55	fvmpt2	$⊢ (x \in B \land x g y \in V) \to (x \in B ⟼ x g y) (x) = x g y$
57	53 54 56	sylancl	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land x \in B \land y \in C) \to (x \in B ⟼ x g y) (x) = x g y$
58	52 57	eqtrd	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land x \in B \land y \in C) \to (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x) = x g y$
59	58	mpoeq3dva	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to (x \in B, y \in C ⟼ (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x)) = (x \in B, y \in C ⟼ x g y)$
60	41 59	eqtr4d	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to g = (x \in B, y \in C ⟼ (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x))$
61		eqid	$⊢ B = B$
62		nfcv	$⊢ \underline{Ⅎ} x C$
63		nfmpt1	$⊢ \underline{Ⅎ} x (x \in B ⟼ x g y)$
64	62 63	nfmpt	$⊢ \underline{Ⅎ} x (y \in C ⟼ (x \in B ⟼ x g y))$
65	64	nfeq2	$⊢ Ⅎ x f = (y \in C ⟼ (x \in B ⟼ x g y))$
66		nfmpt1	$⊢ \underline{Ⅎ} y (y \in C ⟼ (x \in B ⟼ x g y))$
67	66	nfeq2	$⊢ Ⅎ y f = (y \in C ⟼ (x \in B ⟼ x g y))$
68		fveq1	$⊢ f = (y \in C ⟼ (x \in B ⟼ x g y)) \to f (y) = (y \in C ⟼ (x \in B ⟼ x g y)) (y)$
69	68	fveq1d	$⊢ f = (y \in C ⟼ (x \in B ⟼ x g y)) \to f (y) (x) = (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x)$
70	69	a1d	$⊢ f = (y \in C ⟼ (x \in B ⟼ x g y)) \to (y \in C \to f (y) (x) = (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x))$
71	67 70	ralrimi	$⊢ f = (y \in C ⟼ (x \in B ⟼ x g y)) \to \forall y \in C f (y) (x) = (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x)$
72		eqid	$⊢ C = C$
73	71 72	jctil	$⊢ f = (y \in C ⟼ (x \in B ⟼ x g y)) \to (C = C \land \forall y \in C f (y) (x) = (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x))$
74	73	a1d	$⊢ f = (y \in C ⟼ (x \in B ⟼ x g y)) \to (x \in B \to (C = C \land \forall y \in C f (y) (x) = (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x)))$
75	65 74	ralrimi	$⊢ f = (y \in C ⟼ (x \in B ⟼ x g y)) \to \forall x \in B (C = C \land \forall y \in C f (y) (x) = (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x))$
76		mpoeq123	$⊢ (B = B \land \forall x \in B (C = C \land \forall y \in C f (y) (x) = (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x))) \to (x \in B, y \in C ⟼ f (y) (x)) = (x \in B, y \in C ⟼ (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x))$
77	61 75 76	sylancr	$⊢ f = (y \in C ⟼ (x \in B ⟼ x g y)) \to (x \in B, y \in C ⟼ f (y) (x)) = (x \in B, y \in C ⟼ (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x))$
78	77	eqeq2d	$⊢ f = (y \in C ⟼ (x \in B ⟼ x g y)) \to (g = (x \in B, y \in C ⟼ f (y) (x)) \leftrightarrow g = (x \in B, y \in C ⟼ (y \in C ⟼ (x \in B ⟼ x g y)) (y) (x)))$
79	60 78	syl5ibrcom	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to (f = (y \in C ⟼ (x \in B ⟼ x g y)) \to g = (x \in B, y \in C ⟼ f (y) (x)))$
80	3	ad2antrl	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to f : C ⟶ A^{B}$
81	80	feqmptd	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to f = (y \in C ⟼ f (y))$
82		simprl	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to f \in ({(A^{B})}^{C})$
83	82 6	sylan	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land y \in C) \to f (y) : B ⟶ A$
84	83	feqmptd	$⊢ (((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \land y \in C) \to f (y) = (x \in B ⟼ f (y) (x))$
85	84	mpteq2dva	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to (y \in C ⟼ f (y)) = (y \in C ⟼ (x \in B ⟼ f (y) (x)))$
86	81 85	eqtrd	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to f = (y \in C ⟼ (x \in B ⟼ f (y) (x)))$
87		nfmpo2	$⊢ \underline{Ⅎ} y (x \in B, y \in C ⟼ f (y) (x))$
88	87	nfeq2	$⊢ Ⅎ y g = (x \in B, y \in C ⟼ f (y) (x))$
89		eqidd	$⊢ g = (x \in B, y \in C ⟼ f (y) (x)) \to B = B$
90		nfmpo1	$⊢ \underline{Ⅎ} x (x \in B, y \in C ⟼ f (y) (x))$
91	90	nfeq2	$⊢ Ⅎ x g = (x \in B, y \in C ⟼ f (y) (x))$
92		nfv	$⊢ Ⅎ x y \in C$
93		fvex	$⊢ f (y) (x) \in V$
94	11	ovmpt4g	$⊢ (x \in B \land y \in C \land f (y) (x) \in V) \to x (x \in B, y \in C ⟼ f (y) (x)) y = f (y) (x)$
95	93 94	mp3an3	$⊢ (x \in B \land y \in C) \to x (x \in B, y \in C ⟼ f (y) (x)) y = f (y) (x)$
96		oveq	$⊢ g = (x \in B, y \in C ⟼ f (y) (x)) \to x g y = x (x \in B, y \in C ⟼ f (y) (x)) y$
97	96	eqeq1d	$⊢ g = (x \in B, y \in C ⟼ f (y) (x)) \to (x g y = f (y) (x) \leftrightarrow x (x \in B, y \in C ⟼ f (y) (x)) y = f (y) (x))$
98	95 97	syl5ibr	$⊢ g = (x \in B, y \in C ⟼ f (y) (x)) \to ((x \in B \land y \in C) \to x g y = f (y) (x))$
99	98	expcomd	$⊢ g = (x \in B, y \in C ⟼ f (y) (x)) \to (y \in C \to (x \in B \to x g y = f (y) (x)))$
100	91 92 99	ralrimd	$⊢ g = (x \in B, y \in C ⟼ f (y) (x)) \to (y \in C \to \forall x \in B x g y = f (y) (x))$
101		mpteq12	$⊢ (B = B \land \forall x \in B x g y = f (y) (x)) \to (x \in B ⟼ x g y) = (x \in B ⟼ f (y) (x))$
102	89 100 101	syl6an	$⊢ g = (x \in B, y \in C ⟼ f (y) (x)) \to (y \in C \to (x \in B ⟼ x g y) = (x \in B ⟼ f (y) (x)))$
103	88 102	ralrimi	$⊢ g = (x \in B, y \in C ⟼ f (y) (x)) \to \forall y \in C (x \in B ⟼ x g y) = (x \in B ⟼ f (y) (x))$
104		mpteq12	$⊢ (C = C \land \forall y \in C (x \in B ⟼ x g y) = (x \in B ⟼ f (y) (x))) \to (y \in C ⟼ (x \in B ⟼ x g y)) = (y \in C ⟼ (x \in B ⟼ f (y) (x)))$
105	72 103 104	sylancr	$⊢ g = (x \in B, y \in C ⟼ f (y) (x)) \to (y \in C ⟼ (x \in B ⟼ x g y)) = (y \in C ⟼ (x \in B ⟼ f (y) (x)))$
106	105	eqeq2d	$⊢ g = (x \in B, y \in C ⟼ f (y) (x)) \to (f = (y \in C ⟼ (x \in B ⟼ x g y)) \leftrightarrow f = (y \in C ⟼ (x \in B ⟼ f (y) (x))))$
107	86 106	syl5ibrcom	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to (g = (x \in B, y \in C ⟼ f (y) (x)) \to f = (y \in C ⟼ (x \in B ⟼ x g y)))$
108	79 107	impbid	$⊢ ((A \in V \land B \in W \land C \in X) \land (f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)}))) \to (f = (y \in C ⟼ (x \in B ⟼ x g y)) \leftrightarrow g = (x \in B, y \in C ⟼ f (y) (x)))$
109	108	ex	$⊢ (A \in V \land B \in W \land C \in X) \to ((f \in ({(A^{B})}^{C}) \land g \in (A^{(B \times C)})) \to (f = (y \in C ⟼ (x \in B ⟼ x g y)) \leftrightarrow g = (x \in B, y \in C ⟼ f (y) (x))))$
110	1 2 19 37 109	en3d	$⊢ (A \in V \land B \in W \land C \in X) \to ({(A^{B})}^{C}) \approx (A^{(B \times C)})$

Metamath Proof Explorer

Theorem mapxpen

Proof