Theorem finxpnom

Description: Cartesian exponentiation when the exponent is not a natural number defaults to the empty set. (Contributed by ML, 24-Oct-2020)

	Ref	Expression
Assertion	finxpnom	⊢ ( ¬ 𝑁 ∈ ω → ( 𝑈 ↑↑ 𝑁 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		simpl	⊢ ( ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) → 𝑁 ∈ ω )
2	1	con3i	⊢ ( ¬ 𝑁 ∈ ω → ¬ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) )
3		abid	⊢ ( 𝑦 ∈ { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) } ↔ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) )
4	2 3	sylnibr	⊢ ( ¬ 𝑁 ∈ ω → ¬ 𝑦 ∈ { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) } )
5		df-finxp	⊢ ( 𝑈 ↑↑ 𝑁 ) = { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) }
6	5	eleq2i	⊢ ( 𝑦 ∈ ( 𝑈 ↑↑ 𝑁 ) ↔ 𝑦 ∈ { 𝑦 ∣ ( 𝑁 ∈ ω ∧ ∅ = ( rec ( ( 𝑛 ∈ ω , 𝑥 ∈ V ↦ if ( ( 𝑛 = 1o ∧ 𝑥 ∈ 𝑈 ) , ∅ , if ( 𝑥 ∈ ( V × 𝑈 ) , ⟨ ∪ 𝑛 , ( 1st ‘ 𝑥 ) ⟩ , ⟨ 𝑛 , 𝑥 ⟩ ) ) ) , ⟨ 𝑁 , 𝑦 ⟩ ) ‘ 𝑁 ) ) } )
7	4 6	sylnibr	⊢ ( ¬ 𝑁 ∈ ω → ¬ 𝑦 ∈ ( 𝑈 ↑↑ 𝑁 ) )
8	7	eq0rdv	⊢ ( ¬ 𝑁 ∈ ω → ( 𝑈 ↑↑ 𝑁 ) = ∅ )