Theorem finxpsuc

Description: The value of Cartesian exponentiation at a successor. (Contributed by ML, 24-Oct-2020)

	Ref	Expression
Assertion	finxpsuc	|- ( ( N e. _om /\ N =/= (/) ) -> ( U ^^ suc N ) = ( ( U ^^ N ) X. U ) )

Proof

Step	Hyp	Ref	Expression
1		nnord	|- ( N e. _om -> Ord N )
2		ordge1n0	|- ( Ord N -> ( 1o C_ N <-> N =/= (/) ) )
3	1 2	syl	|- ( N e. _om -> ( 1o C_ N <-> N =/= (/) ) )
4	3	biimprd	|- ( N e. _om -> ( N =/= (/) -> 1o C_ N ) )
5	4	imdistani	|- ( ( N e. _om /\ N =/= (/) ) -> ( N e. _om /\ 1o C_ N ) )
6		eqid	|- ( y e. _om , x e. _V |-> if ( ( y = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. y , ( 1st ` x ) >. , <. y , x >. ) ) ) = ( y e. _om , x e. _V |-> if ( ( y = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. y , ( 1st ` x ) >. , <. y , x >. ) ) )
7	6	finxpsuclem	|- ( ( N e. _om /\ 1o C_ N ) -> ( U ^^ suc N ) = ( ( U ^^ N ) X. U ) )
8	5 7	syl	|- ( ( N e. _om /\ N =/= (/) ) -> ( U ^^ suc N ) = ( ( U ^^ N ) X. U ) )