mapen

Description: Two set exponentiations are equinumerous when their bases and exponents are equinumerous. Theorem 6H(c) of Enderton p. 139. (Contributed by NM, 16-Dec-2003) (Proof shortened by Mario Carneiro, 26-Apr-2015)

		Ref	Expression
	Assertion	mapen	$⊢ (A \approx B \land C \approx D) \to (A^{C}) \approx (B^{D})$

Proof

Step	Hyp	Ref	Expression
1		bren	$⊢ A \approx B \leftrightarrow \exists f f : A \underset{1-1 onto}{⟶} B$
2		bren	$⊢ C \approx D \leftrightarrow \exists g g : C \underset{1-1 onto}{⟶} D$
3		exdistrv	$⊢ \exists f \exists g (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \leftrightarrow (\exists f f : A \underset{1-1 onto}{⟶} B \land \exists g g : C \underset{1-1 onto}{⟶} D)$
4		ovexd	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to A^{C} \in V$
5		ovexd	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to B^{D} \in V$
6		elmapi	$⊢ x \in (A^{C}) \to x : C ⟶ A$
7		f1of	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A ⟶ B$
8	7	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to f : A ⟶ B$
9		fco	$⊢ (f : A ⟶ B \land x : C ⟶ A) \to (f \circ x) : C ⟶ B$
10	8 9	sylan	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land x : C ⟶ A) \to (f \circ x) : C ⟶ B$
11		f1ocnv	$⊢ g : C \underset{1-1 onto}{⟶} D \to g^{-1} : D \underset{1-1 onto}{⟶} C$
12	11	adantl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to g^{-1} : D \underset{1-1 onto}{⟶} C$
13		f1of	$⊢ g^{-1} : D \underset{1-1 onto}{⟶} C \to g^{-1} : D ⟶ C$
14	12 13	syl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to g^{-1} : D ⟶ C$
15	14	adantr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land x : C ⟶ A) \to g^{-1} : D ⟶ C$
16	10 15	fcod	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land x : C ⟶ A) \to ((f \circ x) \circ g^{-1}) : D ⟶ B$
17	16	ex	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to (x : C ⟶ A \to ((f \circ x) \circ g^{-1}) : D ⟶ B)$
18	6 17	syl5	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to (x \in (A^{C}) \to ((f \circ x) \circ g^{-1}) : D ⟶ B)$
19		f1ofo	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{onto}{⟶} B$
20	19	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to f : A \underset{onto}{⟶} B$
21		forn	$⊢ f : A \underset{onto}{⟶} B \to ran f = B$
22	20 21	syl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to ran f = B$
23		vex	$⊢ f \in V$
24	23	rnex	$⊢ ran f \in V$
25	22 24	eqeltrrdi	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to B \in V$
26		f1ofo	$⊢ g : C \underset{1-1 onto}{⟶} D \to g : C \underset{onto}{⟶} D$
27	26	adantl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to g : C \underset{onto}{⟶} D$
28		forn	$⊢ g : C \underset{onto}{⟶} D \to ran g = D$
29	27 28	syl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to ran g = D$
30		vex	$⊢ g \in V$
31	30	rnex	$⊢ ran g \in V$
32	29 31	eqeltrrdi	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to D \in V$
33	25 32	elmapd	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to ((f \circ x) \circ g^{-1} \in (B^{D}) \leftrightarrow ((f \circ x) \circ g^{-1}) : D ⟶ B)$
34	18 33	sylibrd	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to (x \in (A^{C}) \to (f \circ x) \circ g^{-1} \in (B^{D}))$
35		elmapi	$⊢ y \in (B^{D}) \to y : D ⟶ B$
36		f1ocnv	$⊢ f : A \underset{1-1 onto}{⟶} B \to f^{-1} : B \underset{1-1 onto}{⟶} A$
37	36	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to f^{-1} : B \underset{1-1 onto}{⟶} A$
38		f1of	$⊢ f^{-1} : B \underset{1-1 onto}{⟶} A \to f^{-1} : B ⟶ A$
39	37 38	syl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to f^{-1} : B ⟶ A$
40	39	adantr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land y : D ⟶ B) \to f^{-1} : B ⟶ A$
41		id	$⊢ y : D ⟶ B \to y : D ⟶ B$
42		f1of	$⊢ g : C \underset{1-1 onto}{⟶} D \to g : C ⟶ D$
43	42	adantl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to g : C ⟶ D$
44		fco	$⊢ (y : D ⟶ B \land g : C ⟶ D) \to (y \circ g) : C ⟶ B$
45	41 43 44	syl2anr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land y : D ⟶ B) \to (y \circ g) : C ⟶ B$
46	40 45	fcod	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land y : D ⟶ B) \to (f^{-1} \circ (y \circ g)) : C ⟶ A$
47	46	ex	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to (y : D ⟶ B \to (f^{-1} \circ (y \circ g)) : C ⟶ A)$
48	35 47	syl5	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to (y \in (B^{D}) \to (f^{-1} \circ (y \circ g)) : C ⟶ A)$
49		f1odm	$⊢ f : A \underset{1-1 onto}{⟶} B \to dom f = A$
50	49	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to dom f = A$
51	23	dmex	$⊢ dom f \in V$
52	50 51	eqeltrrdi	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to A \in V$
53		f1odm	$⊢ g : C \underset{1-1 onto}{⟶} D \to dom g = C$
54	53	adantl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to dom g = C$
55	30	dmex	$⊢ dom g \in V$
56	54 55	eqeltrrdi	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to C \in V$
57	52 56	elmapd	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to (f^{-1} \circ (y \circ g) \in (A^{C}) \leftrightarrow (f^{-1} \circ (y \circ g)) : C ⟶ A)$
58	48 57	sylibrd	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to (y \in (B^{D}) \to f^{-1} \circ (y \circ g) \in (A^{C}))$
59		coass	$⊢ (f \circ f^{-1}) \circ (y \circ g) = f \circ (f^{-1} \circ (y \circ g))$
60		f1ococnv2	$⊢ f : A \underset{1-1 onto}{⟶} B \to f \circ f^{-1} = {I ↾}_{B}$
61	60	ad2antrr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to f \circ f^{-1} = {I ↾}_{B}$
62	61	coeq1d	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (f \circ f^{-1}) \circ (y \circ g) = ({I ↾}_{B}) \circ (y \circ g)$
63	45	adantrl	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (y \circ g) : C ⟶ B$
64		fcoi2	$⊢ (y \circ g) : C ⟶ B \to ({I ↾}_{B}) \circ (y \circ g) = y \circ g$
65	63 64	syl	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to ({I ↾}_{B}) \circ (y \circ g) = y \circ g$
66	62 65	eqtrd	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (f \circ f^{-1}) \circ (y \circ g) = y \circ g$
67	59 66	syl5eqr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to f \circ (f^{-1} \circ (y \circ g)) = y \circ g$
68	67	eqeq2d	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (f \circ x = f \circ (f^{-1} \circ (y \circ g)) \leftrightarrow f \circ x = y \circ g)$
69		coass	$⊢ ((f \circ x) \circ g^{-1}) \circ g = (f \circ x) \circ (g^{-1} \circ g)$
70		f1ococnv1	$⊢ g : C \underset{1-1 onto}{⟶} D \to g^{-1} \circ g = {I ↾}_{C}$
71	70	ad2antlr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to g^{-1} \circ g = {I ↾}_{C}$
72	71	coeq2d	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (f \circ x) \circ (g^{-1} \circ g) = (f \circ x) \circ ({I ↾}_{C})$
73	10	adantrr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (f \circ x) : C ⟶ B$
74		fcoi1	$⊢ (f \circ x) : C ⟶ B \to (f \circ x) \circ ({I ↾}_{C}) = f \circ x$
75	73 74	syl	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (f \circ x) \circ ({I ↾}_{C}) = f \circ x$
76	72 75	eqtrd	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (f \circ x) \circ (g^{-1} \circ g) = f \circ x$
77	69 76	syl5eq	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to ((f \circ x) \circ g^{-1}) \circ g = f \circ x$
78	77	eqeq2d	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (y \circ g = ((f \circ x) \circ g^{-1}) \circ g \leftrightarrow y \circ g = f \circ x)$
79		eqcom	$⊢ y \circ g = f \circ x \leftrightarrow f \circ x = y \circ g$
80	78 79	bitrdi	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (y \circ g = ((f \circ x) \circ g^{-1}) \circ g \leftrightarrow f \circ x = y \circ g)$
81	68 80	bitr4d	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (f \circ x = f \circ (f^{-1} \circ (y \circ g)) \leftrightarrow y \circ g = ((f \circ x) \circ g^{-1}) \circ g)$
82		f1of1	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{1-1}{⟶} B$
83	82	ad2antrr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to f : A \underset{1-1}{⟶} B$
84		simprl	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to x : C ⟶ A$
85	46	adantrl	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (f^{-1} \circ (y \circ g)) : C ⟶ A$
86		cocan1	$⊢ (f : A \underset{1-1}{⟶} B \land x : C ⟶ A \land (f^{-1} \circ (y \circ g)) : C ⟶ A) \to (f \circ x = f \circ (f^{-1} \circ (y \circ g)) \leftrightarrow x = f^{-1} \circ (y \circ g))$
87	83 84 85 86	syl3anc	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (f \circ x = f \circ (f^{-1} \circ (y \circ g)) \leftrightarrow x = f^{-1} \circ (y \circ g))$
88	27	adantr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to g : C \underset{onto}{⟶} D$
89		ffn	$⊢ y : D ⟶ B \to y Fn D$
90	89	ad2antll	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to y Fn D$
91	16	adantrr	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to ((f \circ x) \circ g^{-1}) : D ⟶ B$
92	91	ffnd	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to ((f \circ x) \circ g^{-1}) Fn D$
93		cocan2	$⊢ (g : C \underset{onto}{⟶} D \land y Fn D \land ((f \circ x) \circ g^{-1}) Fn D) \to (y \circ g = ((f \circ x) \circ g^{-1}) \circ g \leftrightarrow y = (f \circ x) \circ g^{-1})$
94	88 90 92 93	syl3anc	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (y \circ g = ((f \circ x) \circ g^{-1}) \circ g \leftrightarrow y = (f \circ x) \circ g^{-1})$
95	81 87 94	3bitr3d	$⊢ ((f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \land (x : C ⟶ A \land y : D ⟶ B)) \to (x = f^{-1} \circ (y \circ g) \leftrightarrow y = (f \circ x) \circ g^{-1})$
96	95	ex	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to ((x : C ⟶ A \land y : D ⟶ B) \to (x = f^{-1} \circ (y \circ g) \leftrightarrow y = (f \circ x) \circ g^{-1}))$
97	6 35 96	syl2ani	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to ((x \in (A^{C}) \land y \in (B^{D})) \to (x = f^{-1} \circ (y \circ g) \leftrightarrow y = (f \circ x) \circ g^{-1}))$
98	4 5 34 58 97	en3d	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to (A^{C}) \approx (B^{D})$
99	98	exlimivv	$⊢ \exists f \exists g (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to (A^{C}) \approx (B^{D})$
100	3 99	sylbir	$⊢ (\exists f f : A \underset{1-1 onto}{⟶} B \land \exists g g : C \underset{1-1 onto}{⟶} D) \to (A^{C}) \approx (B^{D})$
101	1 2 100	syl2anb	$⊢ (A \approx B \land C \approx D) \to (A^{C}) \approx (B^{D})$

Metamath Proof Explorer

Theorem mapen

Proof