Metamath Proof Explorer

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 ⊢ ¬ N ∈ ω → U ↑↑ N = ∅

Proof

Step Hyp Ref Expression
1 simpl ⊢ N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N → N ∈ ω
2 1 con3i ⊢ ¬ N ∈ ω → ¬ N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
3 abid ⊢ y ∈ y | N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N ↔ N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
4 2 3 sylnibr ⊢ ¬ N ∈ ω → ¬ y ∈ y | N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
5 df-finxp ⊢ U ↑↑ N = y | N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
6 5 eleq2i ⊢ y ∈ U ↑↑ N ↔ y ∈ y | N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
7 4 6 sylnibr ⊢ ¬ N ∈ ω → ¬ y ∈ U ↑↑ N
8 7 eq0rdv ⊢ ¬ N ∈ ω → U ↑↑ N = ∅