Metamath Proof Explorer

Theorem finxpnom

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

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( 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 
 |-  ( -. 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 
 |-  ( 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 
 |-  ( -. 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 
 |-  ( 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 
 |-  ( 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 
 |-  ( -. N e. _om -> -. y e. ( U ^^ N ) )
8 7 eq0rdv 
 |-  ( -. N e. _om -> ( U ^^ N ) = (/) )