Metamath Proof Explorer


Theorem finxp1o

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

Ref Expression
Assertion finxp1o U ↑↑ 1 𝑜 = U

Proof

Step Hyp Ref Expression
1 1onn 1 𝑜 ω
2 1 a1i y U 1 𝑜 ω
3 finxpreclem1 y U = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y
4 1on 1 𝑜 On
5 1n0 1 𝑜
6 nnlim 1 𝑜 ω ¬ Lim 1 𝑜
7 1 6 ax-mp ¬ Lim 1 𝑜
8 rdgsucuni 1 𝑜 On 1 𝑜 ¬ Lim 1 𝑜 rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜 = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜
9 4 5 7 8 mp3an rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜 = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜
10 df-1o 1 𝑜 = suc
11 10 unieqi 1 𝑜 = suc
12 0elon On
13 12 onunisuci suc =
14 11 13 eqtri 1 𝑜 =
15 14 fveq2i rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜 = rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y
16 opex 1 𝑜 y V
17 16 rdg0 rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y = 1 𝑜 y
18 15 17 eqtri rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜 = 1 𝑜 y
19 18 fveq2i n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜 = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y
20 9 19 eqtri rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜 = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y
21 3 20 eqtr4di y U = rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜
22 df-finxp U ↑↑ 1 𝑜 = y | 1 𝑜 ω = rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜
23 22 abeq2i y U ↑↑ 1 𝑜 1 𝑜 ω = rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜
24 2 21 23 sylanbrc y U y U ↑↑ 1 𝑜
25 1 23 mpbiran y U ↑↑ 1 𝑜 = rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜
26 vex y V
27 20 eqcomi n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y = rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜
28 finxpreclem2 y V ¬ y U ¬ = n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y
29 28 neqned y V ¬ y U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y
30 29 necomd y V ¬ y U n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y
31 27 30 eqnetrrid y V ¬ y U rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜
32 31 necomd y V ¬ y U rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜
33 32 neneqd y V ¬ y U ¬ = rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜
34 26 33 mpan ¬ y U ¬ = rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜
35 34 con4i = rec n ω , x V if n = 1 𝑜 x U if x V × U n 1 st x n x 1 𝑜 y 1 𝑜 y U
36 25 35 sylbi y U ↑↑ 1 𝑜 y U
37 24 36 impbii y U y U ↑↑ 1 𝑜
38 37 eqriv U = U ↑↑ 1 𝑜
39 38 eqcomi U ↑↑ 1 𝑜 = U