Theorem finxpsuc

Description: The value of Cartesian exponentiation at a successor. (Contributed by ML, 24-Oct-2020)

	Ref	Expression
Assertion	finxpsuc	⊢ ( ( 𝑁 ∈ ω ∧ 𝑁 ≠ ∅ ) → ( 𝑈 ↑↑ suc 𝑁 ) = ( ( 𝑈 ↑↑ 𝑁 ) × 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		nnord	⊢ ( 𝑁 ∈ ω → Ord 𝑁 )
2		ordge1n0	⊢ ( Ord 𝑁 → ( 1o ⊆ 𝑁 ↔ 𝑁 ≠ ∅ ) )
3	1 2	syl	⊢ ( 𝑁 ∈ ω → ( 1o ⊆ 𝑁 ↔ 𝑁 ≠ ∅ ) )
4	3	biimprd	⊢ ( 𝑁 ∈ ω → ( 𝑁 ≠ ∅ → 1o ⊆ 𝑁 ) )
5	4	imdistani	⊢ ( ( 𝑁 ∈ ω ∧ 𝑁 ≠ ∅ ) → ( 𝑁 ∈ ω ∧ 1o ⊆ 𝑁 ) )
6		eqid	⊢ ( 𝑦 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑦 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑦 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑦 , 𝑥 ⟩ ) ) ) = ( 𝑦 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑦 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑦 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑦 , 𝑥 ⟩ ) ) )
7	6	finxpsuclem	⊢ ( ( 𝑁 ∈ ω ∧ 1o ⊆ 𝑁 ) → ( 𝑈 ↑↑ suc 𝑁 ) = ( ( 𝑈 ↑↑ 𝑁 ) × 𝑈 ) )
8	5 7	syl	⊢ ( ( 𝑁 ∈ ω ∧ 𝑁 ≠ ∅ ) → ( 𝑈 ↑↑ suc 𝑁 ) = ( ( 𝑈 ↑↑ 𝑁 ) × 𝑈 ) )