Metamath Proof Explorer

Theorem finxp0

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

Ref Expression
Assertion finxp0 ⊢ U ↑↑ ∅ = ∅

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 vex ⊢ y ∈ V
3 1 2 opnzi ⊢ ∅ y ≠ ∅
4 3 nesymi ⊢ ¬ ∅ = ∅ y
5 peano1 ⊢ ∅ ∈ ω
6 df-finxp ⊢ U ↑↑ ∅ = y | ∅ ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x ∅ y ⁡ ∅
7 6 eqabri ⊢ y ∈ U ↑↑ ∅ ↔ ∅ ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x ∅ y ⁡ ∅
8 5 7 mpbiran ⊢ y ∈ U ↑↑ ∅ ↔ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x ∅ y ⁡ ∅
9 opex ⊢ ∅ y ∈ V
10 9 rdg0 ⊢ rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x ∅ y ⁡ ∅ = ∅ y
11 10 eqeq2i ⊢ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x ∅ y ⁡ ∅ ↔ ∅ = ∅ y
12 8 11 bitri ⊢ y ∈ U ↑↑ ∅ ↔ ∅ = ∅ y
13 4 12 mtbir ⊢ ¬ y ∈ U ↑↑ ∅
14 13 nel0 ⊢ U ↑↑ ∅ = ∅