Theorem finxpnom 31863

Description: Cartesian exponentiation when the exponent is not a natural number defaults to the empty set. (Contributed by ML, 24-Oct-2020.)

Assertion

Ref	Expression
finxpnom	|- ( -. N e. om -> ( U ^^ ^^ N ) = (/) )

Proof of Theorem finxpnom

Dummy variables n x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 464	. . . . 5 |- ( ( N e. om /\ (/) = ( rec ( ( n e. om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) -> N e. om )
2	1	con3i 142	. . . 4 |- ( -. N e. om -> -. ( N e. om /\ (/) = ( rec ( ( n e. om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) )
3		abid 2459	. . . 4 |- ( y e. { y | ( N e. om /\ (/) = ( rec ( ( n e. om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) } <-> ( N e. om /\ (/) = ( rec ( ( n e. om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) )
4	2, 3	sylnibr 312	. . 3 |- ( -. N e. om -> -. y e. { y | ( N e. om /\ (/) = ( rec ( ( n e. om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) } )
5		df-finxp 31846	. . . 4 |- ( U ^^ ^^ N ) = { y | ( N e. om /\ (/) = ( rec ( ( n e. om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) }
6	5	eleq2i 2541	. . 3 |- ( y e. ( U ^^ ^^ N ) <-> y e. { y | ( N e. om /\ (/) = ( rec ( ( n e. om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) , <. N , y >. ) ` N ) ) } )
7	4, 6	sylnibr 312	. 2 |- ( -. N e. om -> -. y e. ( U ^^ ^^ N ) )
8	7	eq0rdv 3773	1 |- ( -. N e. om -> ( U ^^ ^^ N ) = (/) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 376   = wceq 1452   e. wcel 1904   {cab 2457   _Vcvv 3031   (/)c0 3722   ifcif 3872   <.cop 3965   U.cuni 4190   X. cxp 4837   ` cfv 5589   |-> cmpt2 6310   omcom 6711   1stc1st 6810   reccrdg 7145   1oc1o 7193   ^^ ^^cfinxp 31845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451

This theorem depends on definitions:  df-bi 190  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-dif 3393  df-in 3397  df-ss 3404  df-nul 3723  df-finxp 31846

This theorem is referenced by:  finxp00  31864