Metamath Proof Explorer


Theorem finxp00

Description: Cartesian exponentiation of the empty set to any power is the empty set. (Contributed by ML, 24-Oct-2020)

Ref Expression
Assertion finxp00 ↑↑ N =

Proof

Step Hyp Ref Expression
1 finxpeq2 n = ↑↑ n = ↑↑
2 1 eqeq1d n = ↑↑ n = ↑↑ =
3 finxpeq2 n = m ↑↑ n = ↑↑ m
4 3 eqeq1d n = m ↑↑ n = ↑↑ m =
5 finxpeq2 n = suc m ↑↑ n = ↑↑ suc m
6 5 eqeq1d n = suc m ↑↑ n = ↑↑ suc m =
7 finxpeq2 n = N ↑↑ n = ↑↑ N
8 7 eqeq1d n = N ↑↑ n = ↑↑ N =
9 finxp0 ↑↑ =
10 suceq m = suc m = suc
11 df-1o 1 𝑜 = suc
12 10 11 eqtr4di m = suc m = 1 𝑜
13 finxpeq2 suc m = 1 𝑜 ↑↑ suc m = ↑↑ 1 𝑜
14 12 13 syl m = ↑↑ suc m = ↑↑ 1 𝑜
15 finxp1o ↑↑ 1 𝑜 =
16 14 15 eqtrdi m = ↑↑ suc m =
17 16 adantl m ω m = ↑↑ suc m =
18 finxpsuc m ω m ↑↑ suc m = ↑↑ m ×
19 xp0 ↑↑ m × =
20 18 19 eqtrdi m ω m ↑↑ suc m =
21 17 20 pm2.61dane m ω ↑↑ suc m =
22 21 a1d m ω ↑↑ m = ↑↑ suc m =
23 2 4 6 8 9 22 finds N ω ↑↑ N =
24 finxpnom ¬ N ω ↑↑ N =
25 23 24 pm2.61i ↑↑ N =