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