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 = ∅