Metamath Proof Explorer

Theorem finxpeq2

Description: Equality theorem for Cartesian exponentiation. (Contributed by ML, 19-Oct-2020)

Ref Expression
Assertion finxpeq2 ⊢ M = N → U ↑↑ M = U ↑↑ N

Proof

Step Hyp Ref Expression
1 eleq1 ⊢ M = N → M ∈ ω ↔ N ∈ ω
2 opeq1 ⊢ M = N → M y = N y
3 rdgeq2 ⊢ M y = N y → rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x M y = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y
4 2 3 syl ⊢ M = N → rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x M y = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y
5 id ⊢ M = N → M = N
6 4 5 fveq12d ⊢ M = N → rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x M y ⁡ M = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
7 6 eqeq2d ⊢ M = N → ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x M y ⁡ M ↔ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
8 1 7 anbi12d ⊢ M = N → M ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x M y ⁡ M ↔ N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
9 8 abbidv ⊢ M = N → y | M ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x M y ⁡ M = y | N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N
10 df-finxp ⊢ U ↑↑ M = y | M ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x M y ⁡ M
11 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
12 9 10 11 3eqtr4g ⊢ M = N → U ↑↑ M = U ↑↑ N