Theorem relexpxpnnidm

Description: Any positive power of a Cartesian product of non-disjoint sets is itself. (Contributed by RP, 13-Jun-2020)

	Ref	Expression
Assertion	relexpxpnnidm	⊢ ( 𝑁 ∈ ℕ → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑁 ) = ( 𝐴 × 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑥 = 1 → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 1 ) )
2	1	eqeq1d	⊢ ( 𝑥 = 1 → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( 𝐴 × 𝐵 ) ↔ ( ( 𝐴 × 𝐵 ) ↑𝑟 1 ) = ( 𝐴 × 𝐵 ) ) )
3	2	imbi2d	⊢ ( 𝑥 = 1 → ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 1 ) = ( 𝐴 × 𝐵 ) ) ) )
4		oveq2	⊢ ( 𝑥 = 𝑦 → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) )
5	4	eqeq1d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( 𝐴 × 𝐵 ) ↔ ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) )
6	5	imbi2d	⊢ ( 𝑥 = 𝑦 → ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) ) )
7		oveq2	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 ( 𝑦 + 1 ) ) )
8	7	eqeq1d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( 𝐴 × 𝐵 ) ↔ ( ( 𝐴 × 𝐵 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝐴 × 𝐵 ) ) )
9	8	imbi2d	⊢ ( 𝑥 = ( 𝑦 + 1 ) → ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝐴 × 𝐵 ) ) ) )
10		oveq2	⊢ ( 𝑥 = 𝑁 → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑁 ) )
11	10	eqeq1d	⊢ ( 𝑥 = 𝑁 → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( 𝐴 × 𝐵 ) ↔ ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑁 ) = ( 𝐴 × 𝐵 ) ) )
12	11	imbi2d	⊢ ( 𝑥 = 𝑁 → ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑥 ) = ( 𝐴 × 𝐵 ) ) ↔ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑁 ) = ( 𝐴 × 𝐵 ) ) ) )
13		3simpa	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) )
14		xpexg	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ) → ( 𝐴 × 𝐵 ) ∈ V )
15		relexp1g	⊢ ( ( 𝐴 × 𝐵 ) ∈ V → ( ( 𝐴 × 𝐵 ) ↑𝑟 1 ) = ( 𝐴 × 𝐵 ) )
16	13 14 15	3syl	⊢ ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 1 ) = ( 𝐴 × 𝐵 ) )
17		simp2	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) → ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) )
18	17 13 14	3syl	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) → ( 𝐴 × 𝐵 ) ∈ V )
19		simp1	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) → 𝑦 ∈ ℕ )
20		relexpsucnnr	⊢ ( ( ( 𝐴 × 𝐵 ) ∈ V ∧ 𝑦 ∈ ℕ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) ∘ ( 𝐴 × 𝐵 ) ) )
21	18 19 20	syl2anc	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) ∘ ( 𝐴 × 𝐵 ) ) )
22		simp3	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) )
23	22	coeq1d	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) ∘ ( 𝐴 × 𝐵 ) ) = ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) )
24		simp23	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) → ( 𝐴 ∩ 𝐵 ) ≠ ∅ )
25	24	xpcoidgend	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) → ( ( 𝐴 × 𝐵 ) ∘ ( 𝐴 × 𝐵 ) ) = ( 𝐴 × 𝐵 ) )
26	21 23 25	3eqtrd	⊢ ( ( 𝑦 ∈ ℕ ∧ ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) ∧ ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝐴 × 𝐵 ) )
27	26	3exp	⊢ ( 𝑦 ∈ ℕ → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝐴 × 𝐵 ) ) ) )
28	27	a2d	⊢ ( 𝑦 ∈ ℕ → ( ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑦 ) = ( 𝐴 × 𝐵 ) ) → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 ( 𝑦 + 1 ) ) = ( 𝐴 × 𝐵 ) ) ) )
29	3 6 9 12 16 28	nnind	⊢ ( 𝑁 ∈ ℕ → ( ( 𝐴 ∈ 𝑈 ∧ 𝐵 ∈ 𝑉 ∧ ( 𝐴 ∩ 𝐵 ) ≠ ∅ ) → ( ( 𝐴 × 𝐵 ) ↑𝑟 𝑁 ) = ( 𝐴 × 𝐵 ) ) )