Metamath Proof Explorer

Theorem finxpeq1

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

Ref Expression
Assertion finxpeq1 ⊢ U = V → U ↑↑ N = V ↑↑ N

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ U = V → x ∈ U ↔ x ∈ V
2 1 anbi2d ⊢ U = V → n = 1 𝑜 ∧ x ∈ U ↔ n = 1 𝑜 ∧ x ∈ V
3 xpeq2 ⊢ U = V → V × U = V × V
4 3 eleq2d ⊢ U = V → x ∈ V × U ↔ x ∈ V × V
5 4 ifbid ⊢ U = V → if x ∈ V × U ⋃ n 1 st ⁡ x n x = if x ∈ V × V ⋃ n 1 st ⁡ x n x
6 2 5 ifbieq2d ⊢ U = V → if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x = if n = 1 𝑜 ∧ x ∈ V ∅ if x ∈ V × V ⋃ n 1 st ⁡ x n x
7 6 mpoeq3dv ⊢ U = V → n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x = n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ V ∅ if x ∈ V × V ⋃ n 1 st ⁡ x n x
8 rdgeq1 ⊢ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x = n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ V ∅ if x ∈ V × V ⋃ n 1 st ⁡ x n x → rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ V ∅ if x ∈ V × V ⋃ n 1 st ⁡ x n x N y
9 7 8 syl ⊢ U = V → rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ V ∅ if x ∈ V × V ⋃ n 1 st ⁡ x n x N y
10 9 fveq1d ⊢ U = V → rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ V ∅ if x ∈ V × V ⋃ n 1 st ⁡ x n x N y ⁡ N
11 10 eqeq2d ⊢ U = V → ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N ↔ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ V ∅ if x ∈ V × V ⋃ n 1 st ⁡ x n x N y ⁡ N
12 11 anbi2d ⊢ U = V → 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 ∈ V ∅ if x ∈ V × V ⋃ n 1 st ⁡ x n x N y ⁡ N
13 12 abbidv ⊢ U = V → y | N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ U ∅ if x ∈ V × U ⋃ n 1 st ⁡ x n x N y ⁡ N = y | N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ V ∅ if x ∈ V × V ⋃ n 1 st ⁡ x n x N y ⁡ N
14 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
15 df-finxp ⊢ V ↑↑ N = y | N ∈ ω ∧ ∅ = rec ⁡ n ∈ ω , x ∈ V ⟼ if n = 1 𝑜 ∧ x ∈ V ∅ if x ∈ V × V ⋃ n 1 st ⁡ x n x N y ⁡ N
16 13 14 15 3eqtr4g ⊢ U = V → U ↑↑ N = V ↑↑ N