Metamath Proof Explorer

Theorem dffinxpf

Description: This theorem is the same as Definition df-finxp , except that the large function is replaced by a class variable for brevity. (Contributed by ML, 24-Oct-2020)

Ref Expression
Hypothesis dffinxpf.1 ⊢ F = n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x
Assertion dffinxpf ⊢ U ↑↑ N = y | N ∈ ω ∧ ∅ = rec ⁡ F N y ⁡ N

Proof

Step Hyp Ref Expression
1 dffinxpf.1 ⊢ F = n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x
2 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
3 rdgeq1 ⊢ F = n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x → rec ⁡ F N y = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y
4 1 3 ax-mp ⊢ rec ⁡ F N y = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y
5 4 fveq1i ⊢ rec ⁡ F 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 eqeq2i ⊢ ∅ = rec ⁡ F 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
7 6 anbi2i ⊢ N ∈ ω ∧ ∅ = rec ⁡ F 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
8 7 abbii ⊢ y | N ∈ ω ∧ ∅ = rec ⁡ F N y ⁡ 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
9 2 8 eqtr4i ⊢ U ↑↑ N = y | N ∈ ω ∧ ∅ = rec ⁡ F N y ⁡ N