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	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m 2o ) ≈ ( 𝐴 × 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		df2o3	⊢ 2o = { ∅ , 1o }
2		df-pr	⊢ { ∅ , 1o } = ( { ∅ } ∪ { 1o } )
3	1 2	eqtri	⊢ 2o = ( { ∅ } ∪ { 1o } )
4	3	oveq2i	⊢ ( 𝐴 ↑m 2o ) = ( 𝐴 ↑m ( { ∅ } ∪ { 1o } ) )
5		snex	⊢ { ∅ } ∈ V
6	5	a1i	⊢ ( 𝐴 ∈ 𝑉 → { ∅ } ∈ V )
7		snex	⊢ { 1o } ∈ V
8	7	a1i	⊢ ( 𝐴 ∈ 𝑉 → { 1o } ∈ V )
9		id	⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
10		1n0	⊢ 1o ≠ ∅
11	10	neii	⊢ ¬ 1o = ∅
12		elsni	⊢ ( 1o ∈ { ∅ } → 1o = ∅ )
13	11 12	mto	⊢ ¬ 1o ∈ { ∅ }
14		disjsn	⊢ ( ( { ∅ } ∩ { 1o } ) = ∅ ↔ ¬ 1o ∈ { ∅ } )
15	13 14	mpbir	⊢ ( { ∅ } ∩ { 1o } ) = ∅
16	15	a1i	⊢ ( 𝐴 ∈ 𝑉 → ( { ∅ } ∩ { 1o } ) = ∅ )
17		mapunen	⊢ ( ( ( { ∅ } ∈ V ∧ { 1o } ∈ V ∧ 𝐴 ∈ 𝑉 ) ∧ ( { ∅ } ∩ { 1o } ) = ∅ ) → ( 𝐴 ↑m ( { ∅ } ∪ { 1o } ) ) ≈ ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) )
18	6 8 9 16 17	syl31anc	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m ( { ∅ } ∪ { 1o } ) ) ≈ ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) )
19	4 18	eqbrtrid	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m 2o ) ≈ ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) )
20		0ex	⊢ ∅ ∈ V
21	20	a1i	⊢ ( 𝐴 ∈ 𝑉 → ∅ ∈ V )
22	9 21	mapsnend	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m { ∅ } ) ≈ 𝐴 )
23		1oex	⊢ 1o ∈ V
24	23	a1i	⊢ ( 𝐴 ∈ 𝑉 → 1o ∈ V )
25	9 24	mapsnend	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m { 1o } ) ≈ 𝐴 )
26		xpen	⊢ ( ( ( 𝐴 ↑m { ∅ } ) ≈ 𝐴 ∧ ( 𝐴 ↑m { 1o } ) ≈ 𝐴 ) → ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) ≈ ( 𝐴 × 𝐴 ) )
27	22 25 26	syl2anc	⊢ ( 𝐴 ∈ 𝑉 → ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) ≈ ( 𝐴 × 𝐴 ) )
28		entr	⊢ ( ( ( 𝐴 ↑m 2o ) ≈ ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) ∧ ( ( 𝐴 ↑m { ∅ } ) × ( 𝐴 ↑m { 1o } ) ) ≈ ( 𝐴 × 𝐴 ) ) → ( 𝐴 ↑m 2o ) ≈ ( 𝐴 × 𝐴 ) )
29	19 27 28	syl2anc	⊢ ( 𝐴 ∈ 𝑉 → ( 𝐴 ↑m 2o ) ≈ ( 𝐴 × 𝐴 ) )