Theorem 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 e. V -> ( A ^m 2o ) ~~ ( A X. A ) )

Proof

Step	Hyp	Ref	Expression
1		df2o3	|- 2o = { (/) , 1o }
2		df-pr	|- { (/) , 1o } = ( { (/) } u. { 1o } )
3	1 2	eqtri	|- 2o = ( { (/) } u. { 1o } )
4	3	oveq2i	|- ( A ^m 2o ) = ( A ^m ( { (/) } u. { 1o } ) )
5		snex	|- { (/) } e. _V
6	5	a1i	|- ( A e. V -> { (/) } e. _V )
7		snex	|- { 1o } e. _V
8	7	a1i	|- ( A e. V -> { 1o } e. _V )
9		id	|- ( A e. V -> A e. V )
10		1n0	|- 1o =/= (/)
11	10	neii	|- -. 1o = (/)
12		elsni	|- ( 1o e. { (/) } -> 1o = (/) )
13	11 12	mto	|- -. 1o e. { (/) }
14		disjsn	|- ( ( { (/) } i^i { 1o } ) = (/) <-> -. 1o e. { (/) } )
15	13 14	mpbir	|- ( { (/) } i^i { 1o } ) = (/)
16	15	a1i	|- ( A e. V -> ( { (/) } i^i { 1o } ) = (/) )
17		mapunen	|- ( ( ( { (/) } e. _V /\ { 1o } e. _V /\ A e. V ) /\ ( { (/) } i^i { 1o } ) = (/) ) -> ( A ^m ( { (/) } u. { 1o } ) ) ~~ ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) )
18	6 8 9 16 17	syl31anc	|- ( A e. V -> ( A ^m ( { (/) } u. { 1o } ) ) ~~ ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) )
19	4 18	eqbrtrid	|- ( A e. V -> ( A ^m 2o ) ~~ ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) )
20		0ex	|- (/) e. _V
21	20	a1i	|- ( A e. V -> (/) e. _V )
22	9 21	mapsnend	|- ( A e. V -> ( A ^m { (/) } ) ~~ A )
23		1oex	|- 1o e. _V
24	23	a1i	|- ( A e. V -> 1o e. _V )
25	9 24	mapsnend	|- ( A e. V -> ( A ^m { 1o } ) ~~ A )
26		xpen	|- ( ( ( A ^m { (/) } ) ~~ A /\ ( A ^m { 1o } ) ~~ A ) -> ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) ~~ ( A X. A ) )
27	22 25 26	syl2anc	|- ( A e. V -> ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) ~~ ( A X. A ) )
28		entr	|- ( ( ( A ^m 2o ) ~~ ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) /\ ( ( A ^m { (/) } ) X. ( A ^m { 1o } ) ) ~~ ( A X. A ) ) -> ( A ^m 2o ) ~~ ( A X. A ) )
29	19 27 28	syl2anc	|- ( A e. V -> ( A ^m 2o ) ~~ ( A X. A ) )