Theorem finxp2o

Description: The value of Cartesian exponentiation at two. (Contributed by ML, 19-Oct-2020)

	Ref	Expression
Assertion	finxp2o	|- ( U ^^ 2o ) = ( U X. U )

Proof

Step	Hyp	Ref	Expression
1		df-2o	|- 2o = suc 1o
2		finxpeq2	|- ( 2o = suc 1o -> ( U ^^ 2o ) = ( U ^^ suc 1o ) )
3	1 2	ax-mp	|- ( U ^^ 2o ) = ( U ^^ suc 1o )
4		1onn	|- 1o e. _om
5		1n0	|- 1o =/= (/)
6		finxpsuc	|- ( ( 1o e. _om /\ 1o =/= (/) ) -> ( U ^^ suc 1o ) = ( ( U ^^ 1o ) X. U ) )
7	4 5 6	mp2an	|- ( U ^^ suc 1o ) = ( ( U ^^ 1o ) X. U )
8		finxp1o	|- ( U ^^ 1o ) = U
9	8	xpeq1i	|- ( ( U ^^ 1o ) X. U ) = ( U X. U )
10	3 7 9	3eqtri	|- ( U ^^ 2o ) = ( U X. U )