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		fco	$⊢ ((f \circ x) : C ⟶ B \land g^{-1} : D ⟶ C) \to ((f \circ x) \circ g^{-1}) : D ⟶ B$
17	10 15 16	syl2anc	$⊢ ((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$
18	17	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)$
19	6 18	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)$
20		f1ofo	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{onto}{⟶} B$
21	20	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to f : A \underset{onto}{⟶} B$
22		forn	$⊢ f : A \underset{onto}{⟶} B \to ran f = B$
23	21 22	syl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to ran f = B$
24		vex	$⊢ f \in V$
25	24	rnex	$⊢ ran f \in V$
26	23 25	eqeltrrdi	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to B \in V$
27		f1ofo	$⊢ g : C \underset{1-1 onto}{⟶} D \to g : C \underset{onto}{⟶} D$
28	27	adantl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to g : C \underset{onto}{⟶} D$
29		forn	$⊢ g : C \underset{onto}{⟶} D \to ran g = D$
30	28 29	syl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to ran g = D$
31		vex	$⊢ g \in V$
32	31	rnex	$⊢ ran g \in V$
33	30 32	eqeltrrdi	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to D \in V$
34	26 33	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)$
35	19 34	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}))$
36		elmapi	$⊢ y \in (B^{D}) \to y : D ⟶ B$
37		f1ocnv	$⊢ f : A \underset{1-1 onto}{⟶} B \to f^{-1} : B \underset{1-1 onto}{⟶} A$
38	37	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$
39		f1of	$⊢ f^{-1} : B \underset{1-1 onto}{⟶} A \to f^{-1} : B ⟶ A$
40	38 39	syl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to f^{-1} : B ⟶ A$
41	40	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$
42		id	$⊢ y : D ⟶ B \to y : D ⟶ B$
43		f1of	$⊢ g : C \underset{1-1 onto}{⟶} D \to g : C ⟶ D$
44	43	adantl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to g : C ⟶ D$
45		fco	$⊢ (y : D ⟶ B \land g : C ⟶ D) \to (y \circ g) : C ⟶ B$
46	42 44 45	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$
47		fco	$⊢ (f^{-1} : B ⟶ A \land (y \circ g) : C ⟶ B) \to (f^{-1} \circ (y \circ g)) : C ⟶ A$
48	41 46 47	syl2anc	$⊢ ((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$
49	48	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)$
50	36 49	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)$
51		f1odm	$⊢ f : A \underset{1-1 onto}{⟶} B \to dom f = A$
52	51	adantr	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to dom f = A$
53	24	dmex	$⊢ dom f \in V$
54	52 53	eqeltrrdi	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to A \in V$
55		f1odm	$⊢ g : C \underset{1-1 onto}{⟶} D \to dom g = C$
56	55	adantl	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to dom g = C$
57	31	dmex	$⊢ dom g \in V$
58	56 57	eqeltrrdi	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to C \in V$
59	54 58	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)$
60	50 59	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}))$
61		coass	$⊢ (f \circ f^{-1}) \circ (y \circ g) = f \circ (f^{-1} \circ (y \circ g))$
62		f1ococnv2	$⊢ f : A \underset{1-1 onto}{⟶} B \to f \circ f^{-1} = {I ↾}_{B}$
63	62	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}$
64	63	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)$
65	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 (y \circ g) : C ⟶ B$
66		fcoi2	$⊢ (y \circ g) : C ⟶ B \to ({I ↾}_{B}) \circ (y \circ g) = y \circ g$
67	65 66	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$
68	64 67	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$
69	61 68	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$
70	69	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)$
71		coass	$⊢ ((f \circ x) \circ g^{-1}) \circ g = (f \circ x) \circ (g^{-1} \circ g)$
72		f1ococnv1	$⊢ g : C \underset{1-1 onto}{⟶} D \to g^{-1} \circ g = {I ↾}_{C}$
73	72	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}$
74	73	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})$
75	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$
76		fcoi1	$⊢ (f \circ x) : C ⟶ B \to (f \circ x) \circ ({I ↾}_{C}) = f \circ x$
77	75 76	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$
78	74 77	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$
79	71 78	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$
80	79	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)$
81		eqcom	$⊢ y \circ g = f \circ x \leftrightarrow f \circ x = y \circ g$
82	80 81	syl6bb	$⊢ ((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)$
83	70 82	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)$
84		f1of1	$⊢ f : A \underset{1-1 onto}{⟶} B \to f : A \underset{1-1}{⟶} B$
85	84	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$
86		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$
87	48	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$
88		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))$
89	85 86 87 88	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))$
90	28	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$
91		ffn	$⊢ y : D ⟶ B \to y Fn D$
92	91	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$
93	17	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$
94	93	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$
95		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})$
96	90 92 94 95	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})$
97	83 89 96	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})$
98	97	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}))$
99	6 36 98	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}))$
100	4 5 35 60 99	en3d	$⊢ (f : A \underset{1-1 onto}{⟶} B \land g : C \underset{1-1 onto}{⟶} D) \to (A^{C}) \approx (B^{D})$
101	100	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})$
102	3 101	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})$
103	1 2 102	syl2anb	$⊢ (A \approx B \land C \approx D) \to (A^{C}) \approx (B^{D})$

Metamath Proof Explorer

Theorem mapen

Proof