Metamath Proof Explorer

Theorem finxp0

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

Ref Expression
Assertion finxp0 
|- ( U ^^ (/) ) = (/)

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 vex 
 |-  y e. _V
3 1 2 opnzi 
 |-  <. (/) , y >. =/= (/)
4 3 nesymi 
 |-  -. (/) = <. (/) , y >.
5 peano1 
 |-  (/) e. _om
6 df-finxp 
 |-  ( U ^^ (/) ) = { y | ( (/) 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 >. ) ) ) , <. (/) , y >. ) ` (/) ) ) }
7 6 abeq2i 
 |-  ( y e. ( U ^^ (/) ) <-> ( (/) 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 >. ) ) ) , <. (/) , y >. ) ` (/) ) ) )
8 5 7 mpbiran 
 |-  ( y e. ( U ^^ (/) ) <-> (/) = ( 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 >. ) ) ) , <. (/) , y >. ) ` (/) ) )
9 opex 
 |-  <. (/) , y >. e. _V
10 9 rdg0 
 |-  ( 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 >. ) ) ) , <. (/) , y >. ) ` (/) ) = <. (/) , y >.
11 10 eqeq2i 
 |-  ( (/) = ( 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 >. ) ) ) , <. (/) , y >. ) ` (/) ) <-> (/) = <. (/) , y >. )
12 8 11 bitri 
 |-  ( y e. ( U ^^ (/) ) <-> (/) = <. (/) , y >. )
13 4 12 mtbir 
 |-  -. y e. ( U ^^ (/) )
14 13 nel0 
 |-  ( U ^^ (/) ) = (/)