Metamath Proof Explorer

Theorem finxp1o

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

Ref Expression
Assertion finxp1o 
|- ( U ^^ 1o ) = U

Proof

Step Hyp Ref Expression
1 1onn 
 |-  1o e. _om
2 1 a1i 
 |-  ( y e. U -> 1o e. _om )
3 finxpreclem1 
 |-  ( y e. U -> (/) = ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` <. 1o , y >. ) )
4 1on 
 |-  1o e. On
5 1n0 
 |-  1o =/= (/)
6 nnlim 
 |-  ( 1o e. _om -> -. Lim 1o )
7 1 6 ax-mp 
 |-  -. Lim 1o
8 rdgsucuni 
 |-  ( ( 1o e. On /\ 1o =/= (/) /\ -. Lim 1o ) -> ( 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) = ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` ( 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 >. ) ) ) , <. 1o , y >. ) ` U. 1o ) ) )
9 4 5 7 8 mp3an 
 |-  ( 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) = ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` ( 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 >. ) ) ) , <. 1o , y >. ) ` U. 1o ) )
10 df-1o 
 |-  1o = suc (/)
11 10 unieqi 
 |-  U. 1o = U. suc (/)
12 0elon 
 |-  (/) e. On
13 12 onunisuci 
 |-  U. suc (/) = (/)
14 11 13 eqtri 
 |-  U. 1o = (/)
15 14 fveq2i 
 |-  ( 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 >. ) ) ) , <. 1o , y >. ) ` U. 1o ) = ( 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 >. ) ) ) , <. 1o , y >. ) ` (/) )
16 opex 
 |-  <. 1o , y >. e. _V
17 16 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 >. ) ) ) , <. 1o , y >. ) ` (/) ) = <. 1o , y >.
18 15 17 eqtri 
 |-  ( 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 >. ) ) ) , <. 1o , y >. ) ` U. 1o ) = <. 1o , y >.
19 18 fveq2i 
 |-  ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` ( 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 >. ) ) ) , <. 1o , y >. ) ` U. 1o ) ) = ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` <. 1o , y >. )
20 9 19 eqtri 
 |-  ( 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) = ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` <. 1o , y >. )
21 3 20 eqtr4di 
 |-  ( 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) )
22 df-finxp 
 |-  ( U ^^ 1o ) = { y | ( 1o 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) ) }
23 22 abeq2i 
 |-  ( y e. ( U ^^ 1o ) <-> ( 1o 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) ) )
24 2 21 23 sylanbrc 
 |-  ( y e. U -> y e. ( U ^^ 1o ) )
25 1 23 mpbiran 
 |-  ( y e. ( U ^^ 1o ) <-> (/) = ( 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) )
26 vex 
 |-  y e. _V
27 20 eqcomi 
 |-  ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` <. 1o , y >. ) = ( 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 >. ) ) ) , <. 1o , y >. ) ` 1o )
28 finxpreclem2 
 |-  ( ( y e. _V /\ -. y e. U ) -> -. (/) = ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` <. 1o , y >. ) )
29 28 neqned 
 |-  ( ( y e. _V /\ -. y e. U ) -> (/) =/= ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` <. 1o , y >. ) )
30 29 necomd 
 |-  ( ( y e. _V /\ -. y e. U ) -> ( ( n e. _om , x e. _V |-> if ( ( n = 1o /\ x e. U ) , (/) , if ( x e. ( _V X. U ) , <. U. n , ( 1st ` x ) >. , <. n , x >. ) ) ) ` <. 1o , y >. ) =/= (/) )
31 27 30 eqnetrrid 
 |-  ( ( y e. _V /\ -. 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) =/= (/) )
32 31 necomd 
 |-  ( ( y e. _V /\ -. 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) )
33 32 neneqd 
 |-  ( ( y e. _V /\ -. 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) )
34 26 33 mpan 
 |-  ( -. 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) )
35 34 con4i 
 |-  ( (/) = ( 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 >. ) ) ) , <. 1o , y >. ) ` 1o ) -> y e. U )
36 25 35 sylbi 
 |-  ( y e. ( U ^^ 1o ) -> y e. U )
37 24 36 impbii 
 |-  ( y e. U <-> y e. ( U ^^ 1o ) )
38 37 eqriv 
 |-  U = ( U ^^ 1o )
39 38 eqcomi 
 |-  ( U ^^ 1o ) = U