mapdjuen

Description: Sum of exponents law for cardinal arithmetic. Theorem 6I(4) of Enderton p. 142. (Contributed by NM, 27-Sep-2004) (Revised by Mario Carneiro, 29-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		df-dju	$⊢ (B ⊔︀ C) = (\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C)$
2	1	oveq2i	$⊢ A^{(B ⊔︀ C)} = A^{((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C))}$
3		snex	$⊢ \{\emptyset\} \in V$
4		simp2	$⊢ (A \in V \land B \in W \land C \in X) \to B \in W$
5		xpexg	$⊢ (\{\emptyset\} \in V \land B \in W) \to \{\emptyset\} \times B \in V$
6	3 4 5	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to \{\emptyset\} \times B \in V$
7		snex	$⊢ \{1_{𝑜}\} \in V$
8		simp3	$⊢ (A \in V \land B \in W \land C \in X) \to C \in X$
9		xpexg	$⊢ (\{1_{𝑜}\} \in V \land C \in X) \to \{1_{𝑜}\} \times C \in V$
10	7 8 9	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to \{1_{𝑜}\} \times C \in V$
11		simp1	$⊢ (A \in V \land B \in W \land C \in X) \to A \in V$
12		xp01disjl	$⊢ (\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times C) = \emptyset$
13	12	a1i	$⊢ (A \in V \land B \in W \land C \in X) \to (\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times C) = \emptyset$
14		mapunen	$⊢ ((\{\emptyset\} \times B \in V \land \{1_{𝑜}\} \times C \in V \land A \in V) \land (\{\emptyset\} \times B) \cap (\{1_{𝑜}\} \times C) = \emptyset) \to (A^{((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C))}) \approx ((A^{(\{\emptyset\} \times B)}) \times (A^{(\{1_{𝑜}\} \times C)}))$
15	6 10 11 13 14	syl31anc	$⊢ (A \in V \land B \in W \land C \in X) \to (A^{((\{\emptyset\} \times B) \cup (\{1_{𝑜}\} \times C))}) \approx ((A^{(\{\emptyset\} \times B)}) \times (A^{(\{1_{𝑜}\} \times C)}))$
16	2 15	eqbrtrid	$⊢ (A \in V \land B \in W \land C \in X) \to (A^{(B ⊔︀ C)}) \approx ((A^{(\{\emptyset\} \times B)}) \times (A^{(\{1_{𝑜}\} \times C)}))$
17		enrefg	$⊢ A \in V \to A \approx A$
18	11 17	syl	$⊢ (A \in V \land B \in W \land C \in X) \to A \approx A$
19		0ex	$⊢ \emptyset \in V$
20		xpsnen2g	$⊢ (\emptyset \in V \land B \in W) \to (\{\emptyset\} \times B) \approx B$
21	19 4 20	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to (\{\emptyset\} \times B) \approx B$
22		mapen	$⊢ (A \approx A \land (\{\emptyset\} \times B) \approx B) \to (A^{(\{\emptyset\} \times B)}) \approx (A^{B})$
23	18 21 22	syl2anc	$⊢ (A \in V \land B \in W \land C \in X) \to (A^{(\{\emptyset\} \times B)}) \approx (A^{B})$
24		1on	$⊢ 1_{𝑜} \in On$
25		xpsnen2g	$⊢ (1_{𝑜} \in On \land C \in X) \to (\{1_{𝑜}\} \times C) \approx C$
26	24 8 25	sylancr	$⊢ (A \in V \land B \in W \land C \in X) \to (\{1_{𝑜}\} \times C) \approx C$
27		mapen	$⊢ (A \approx A \land (\{1_{𝑜}\} \times C) \approx C) \to (A^{(\{1_{𝑜}\} \times C)}) \approx (A^{C})$
28	18 26 27	syl2anc	$⊢ (A \in V \land B \in W \land C \in X) \to (A^{(\{1_{𝑜}\} \times C)}) \approx (A^{C})$
29		xpen	$⊢ ((A^{(\{\emptyset\} \times B)}) \approx (A^{B}) \land (A^{(\{1_{𝑜}\} \times C)}) \approx (A^{C})) \to ((A^{(\{\emptyset\} \times B)}) \times (A^{(\{1_{𝑜}\} \times C)})) \approx ((A^{B}) \times (A^{C}))$
30	23 28 29	syl2anc	$⊢ (A \in V \land B \in W \land C \in X) \to ((A^{(\{\emptyset\} \times B)}) \times (A^{(\{1_{𝑜}\} \times C)})) \approx ((A^{B}) \times (A^{C}))$
31		entr	$⊢ ((A^{(B ⊔︀ C)}) \approx ((A^{(\{\emptyset\} \times B)}) \times (A^{(\{1_{𝑜}\} \times C)})) \land ((A^{(\{\emptyset\} \times B)}) \times (A^{(\{1_{𝑜}\} \times C)})) \approx ((A^{B}) \times (A^{C}))) \to (A^{(B ⊔︀ C)}) \approx ((A^{B}) \times (A^{C}))$
32	16 30 31	syl2anc	$⊢ (A \in V \land B \in W \land C \in X) \to (A^{(B ⊔︀ C)}) \approx ((A^{B}) \times (A^{C}))$

Metamath Proof Explorer

Theorem mapdjuen

Proof