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	⊢ ( ∅ ↑↑ 𝑁 ) = ∅

Proof

Step	Hyp	Ref	Expression
1		finxpeq2	⊢ ( 𝑛 = ∅ → ( ∅ ↑↑ 𝑛 ) = ( ∅ ↑↑ ∅ ) )
2	1	eqeq1d	⊢ ( 𝑛 = ∅ → ( ( ∅ ↑↑ 𝑛 ) = ∅ ↔ ( ∅ ↑↑ ∅ ) = ∅ ) )
3		finxpeq2	⊢ ( 𝑛 = 𝑚 → ( ∅ ↑↑ 𝑛 ) = ( ∅ ↑↑ 𝑚 ) )
4	3	eqeq1d	⊢ ( 𝑛 = 𝑚 → ( ( ∅ ↑↑ 𝑛 ) = ∅ ↔ ( ∅ ↑↑ 𝑚 ) = ∅ ) )
5		finxpeq2	⊢ ( 𝑛 = suc 𝑚 → ( ∅ ↑↑ 𝑛 ) = ( ∅ ↑↑ suc 𝑚 ) )
6	5	eqeq1d	⊢ ( 𝑛 = suc 𝑚 → ( ( ∅ ↑↑ 𝑛 ) = ∅ ↔ ( ∅ ↑↑ suc 𝑚 ) = ∅ ) )
7		finxpeq2	⊢ ( 𝑛 = 𝑁 → ( ∅ ↑↑ 𝑛 ) = ( ∅ ↑↑ 𝑁 ) )
8	7	eqeq1d	⊢ ( 𝑛 = 𝑁 → ( ( ∅ ↑↑ 𝑛 ) = ∅ ↔ ( ∅ ↑↑ 𝑁 ) = ∅ ) )
9		finxp0	⊢ ( ∅ ↑↑ ∅ ) = ∅
10		suceq	⊢ ( 𝑚 = ∅ → suc 𝑚 = suc ∅ )
11		df-1o	⊢ 1o = suc ∅
12	10 11	eqtr4di	⊢ ( 𝑚 = ∅ → suc 𝑚 = 1o )
13		finxpeq2	⊢ ( suc 𝑚 = 1o → ( ∅ ↑↑ suc 𝑚 ) = ( ∅ ↑↑ 1o ) )
14	12 13	syl	⊢ ( 𝑚 = ∅ → ( ∅ ↑↑ suc 𝑚 ) = ( ∅ ↑↑ 1o ) )
15		finxp1o	⊢ ( ∅ ↑↑ 1o ) = ∅
16	14 15	eqtrdi	⊢ ( 𝑚 = ∅ → ( ∅ ↑↑ suc 𝑚 ) = ∅ )
17	16	adantl	⊢ ( ( 𝑚 ∈ ω ∧ 𝑚 = ∅ ) → ( ∅ ↑↑ suc 𝑚 ) = ∅ )
18		finxpsuc	⊢ ( ( 𝑚 ∈ ω ∧ 𝑚 ≠ ∅ ) → ( ∅ ↑↑ suc 𝑚 ) = ( ( ∅ ↑↑ 𝑚 ) × ∅ ) )
19		xp0	⊢ ( ( ∅ ↑↑ 𝑚 ) × ∅ ) = ∅
20	18 19	eqtrdi	⊢ ( ( 𝑚 ∈ ω ∧ 𝑚 ≠ ∅ ) → ( ∅ ↑↑ suc 𝑚 ) = ∅ )
21	17 20	pm2.61dane	⊢ ( 𝑚 ∈ ω → ( ∅ ↑↑ suc 𝑚 ) = ∅ )
22	21	a1d	⊢ ( 𝑚 ∈ ω → ( ( ∅ ↑↑ 𝑚 ) = ∅ → ( ∅ ↑↑ suc 𝑚 ) = ∅ ) )
23	2 4 6 8 9 22	finds	⊢ ( 𝑁 ∈ ω → ( ∅ ↑↑ 𝑁 ) = ∅ )
24		finxpnom	⊢ ( ¬ 𝑁 ∈ ω → ( ∅ ↑↑ 𝑁 ) = ∅ )
25	23 24	pm2.61i	⊢ ( ∅ ↑↑ 𝑁 ) = ∅