map2xp

Description: A cardinal power with exponent 2 is equivalent to a Cartesian product with itself. (Contributed by Mario Carneiro, 31-May-2015) (Proof shortened by AV, 17-Jul-2022)

		Ref	Expression
	Assertion	map2xp	$⊢ A \in V \to (A^{2_{𝑜}}) \approx (A \times A)$

Proof

Step	Hyp	Ref	Expression
1		df2o3	$⊢ 2_{𝑜} = \{\emptyset, 1_{𝑜}\}$
2		df-pr	$⊢ \{\emptyset, 1_{𝑜}\} = \{\emptyset\} \cup \{1_{𝑜}\}$
3	1 2	eqtri	$⊢ 2_{𝑜} = \{\emptyset\} \cup \{1_{𝑜}\}$
4	3	oveq2i	$⊢ A^{2_{𝑜}} = A^{(\{\emptyset\} \cup \{1_{𝑜}\})}$
5		snex	$⊢ \{\emptyset\} \in V$
6	5	a1i	$⊢ A \in V \to \{\emptyset\} \in V$
7		snex	$⊢ \{1_{𝑜}\} \in V$
8	7	a1i	$⊢ A \in V \to \{1_{𝑜}\} \in V$
9		id	$⊢ A \in V \to A \in V$
10		1n0	$⊢ 1_{𝑜} \neq \emptyset$
11	10	neii	$⊢ \neg 1_{𝑜} = \emptyset$
12		elsni	$⊢ 1_{𝑜} \in \{\emptyset\} \to 1_{𝑜} = \emptyset$
13	11 12	mto	$⊢ \neg 1_{𝑜} \in \{\emptyset\}$
14		disjsn	$⊢ \{\emptyset\} \cap \{1_{𝑜}\} = \emptyset \leftrightarrow \neg 1_{𝑜} \in \{\emptyset\}$
15	13 14	mpbir	$⊢ \{\emptyset\} \cap \{1_{𝑜}\} = \emptyset$
16	15	a1i	$⊢ A \in V \to \{\emptyset\} \cap \{1_{𝑜}\} = \emptyset$
17		mapunen	$⊢ ((\{\emptyset\} \in V \land \{1_{𝑜}\} \in V \land A \in V) \land \{\emptyset\} \cap \{1_{𝑜}\} = \emptyset) \to (A^{(\{\emptyset\} \cup \{1_{𝑜}\})}) \approx ((A^{\{\emptyset\}}) \times (A^{\{1_{𝑜}\}}))$
18	6 8 9 16 17	syl31anc	$⊢ A \in V \to (A^{(\{\emptyset\} \cup \{1_{𝑜}\})}) \approx ((A^{\{\emptyset\}}) \times (A^{\{1_{𝑜}\}}))$
19	4 18	eqbrtrid	$⊢ A \in V \to (A^{2_{𝑜}}) \approx ((A^{\{\emptyset\}}) \times (A^{\{1_{𝑜}\}}))$
20		0ex	$⊢ \emptyset \in V$
21	20	a1i	$⊢ A \in V \to \emptyset \in V$
22	9 21	mapsnend	$⊢ A \in V \to (A^{\{\emptyset\}}) \approx A$
23		1oex	$⊢ 1_{𝑜} \in V$
24	23	a1i	$⊢ A \in V \to 1_{𝑜} \in V$
25	9 24	mapsnend	$⊢ A \in V \to (A^{\{1_{𝑜}\}}) \approx A$
26		xpen	$⊢ ((A^{\{\emptyset\}}) \approx A \land (A^{\{1_{𝑜}\}}) \approx A) \to ((A^{\{\emptyset\}}) \times (A^{\{1_{𝑜}\}})) \approx (A \times A)$
27	22 25 26	syl2anc	$⊢ A \in V \to ((A^{\{\emptyset\}}) \times (A^{\{1_{𝑜}\}})) \approx (A \times A)$
28		entr	$⊢ ((A^{2_{𝑜}}) \approx ((A^{\{\emptyset\}}) \times (A^{\{1_{𝑜}\}})) \land ((A^{\{\emptyset\}}) \times (A^{\{1_{𝑜}\}})) \approx (A \times A)) \to (A^{2_{𝑜}}) \approx (A \times A)$
29	19 27 28	syl2anc	$⊢ A \in V \to (A^{2_{𝑜}}) \approx (A \times A)$

Metamath Proof Explorer

Theorem map2xp

Proof