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	$⊢ N \in ℕ \to ((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} N = A \times B)$

Proof

Step	Hyp	Ref	Expression
1		oveq2	$⊢ x = 1 \to (A \times B) ↑_{r} x = (A \times B) ↑_{r} 1$
2	1	eqeq1d	$⊢ x = 1 \to ((A \times B) ↑_{r} x = A \times B \leftrightarrow (A \times B) ↑_{r} 1 = A \times B)$
3	2	imbi2d	$⊢ x = 1 \to (((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} x = A \times B) \leftrightarrow ((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} 1 = A \times B))$
4		oveq2	$⊢ x = y \to (A \times B) ↑_{r} x = (A \times B) ↑_{r} y$
5	4	eqeq1d	$⊢ x = y \to ((A \times B) ↑_{r} x = A \times B \leftrightarrow (A \times B) ↑_{r} y = A \times B)$
6	5	imbi2d	$⊢ x = y \to (((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} x = A \times B) \leftrightarrow ((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} y = A \times B))$
7		oveq2	$⊢ x = y + 1 \to (A \times B) ↑_{r} x = (A \times B) ↑_{r} (y + 1)$
8	7	eqeq1d	$⊢ x = y + 1 \to ((A \times B) ↑_{r} x = A \times B \leftrightarrow (A \times B) ↑_{r} (y + 1) = A \times B)$
9	8	imbi2d	$⊢ x = y + 1 \to (((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} x = A \times B) \leftrightarrow ((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} (y + 1) = A \times B))$
10		oveq2	$⊢ x = N \to (A \times B) ↑_{r} x = (A \times B) ↑_{r} N$
11	10	eqeq1d	$⊢ x = N \to ((A \times B) ↑_{r} x = A \times B \leftrightarrow (A \times B) ↑_{r} N = A \times B)$
12	11	imbi2d	$⊢ x = N \to (((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} x = A \times B) \leftrightarrow ((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} N = A \times B))$
13		3simpa	$⊢ (A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \in U \land B \in V)$
14		xpexg	$⊢ (A \in U \land B \in V) \to A \times B \in V$
15		relexp1g	$⊢ A \times B \in V \to (A \times B) ↑_{r} 1 = A \times B$
16	13 14 15	3syl	$⊢ (A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} 1 = A \times B$
17		simp2	$⊢ (y \in ℕ \land (A \in U \land B \in V \land A \cap B \neq \emptyset) \land (A \times B) ↑_{r} y = A \times B) \to (A \in U \land B \in V \land A \cap B \neq \emptyset)$
18	17 13 14	3syl	$⊢ (y \in ℕ \land (A \in U \land B \in V \land A \cap B \neq \emptyset) \land (A \times B) ↑_{r} y = A \times B) \to A \times B \in V$
19		simp1	$⊢ (y \in ℕ \land (A \in U \land B \in V \land A \cap B \neq \emptyset) \land (A \times B) ↑_{r} y = A \times B) \to y \in ℕ$
20		relexpsucnnr	$⊢ (A \times B \in V \land y \in ℕ) \to (A \times B) ↑_{r} (y + 1) = ((A \times B) ↑_{r} y) \circ (A \times B)$
21	18 19 20	syl2anc	$⊢ (y \in ℕ \land (A \in U \land B \in V \land A \cap B \neq \emptyset) \land (A \times B) ↑_{r} y = A \times B) \to (A \times B) ↑_{r} (y + 1) = ((A \times B) ↑_{r} y) \circ (A \times B)$
22		simp3	$⊢ (y \in ℕ \land (A \in U \land B \in V \land A \cap B \neq \emptyset) \land (A \times B) ↑_{r} y = A \times B) \to (A \times B) ↑_{r} y = A \times B$
23	22	coeq1d	$⊢ (y \in ℕ \land (A \in U \land B \in V \land A \cap B \neq \emptyset) \land (A \times B) ↑_{r} y = A \times B) \to ((A \times B) ↑_{r} y) \circ (A \times B) = (A \times B) \circ (A \times B)$
24		simp23	$⊢ (y \in ℕ \land (A \in U \land B \in V \land A \cap B \neq \emptyset) \land (A \times B) ↑_{r} y = A \times B) \to A \cap B \neq \emptyset$
25	24	xpcoidgend	$⊢ (y \in ℕ \land (A \in U \land B \in V \land A \cap B \neq \emptyset) \land (A \times B) ↑_{r} y = A \times B) \to (A \times B) \circ (A \times B) = A \times B$
26	21 23 25	3eqtrd	$⊢ (y \in ℕ \land (A \in U \land B \in V \land A \cap B \neq \emptyset) \land (A \times B) ↑_{r} y = A \times B) \to (A \times B) ↑_{r} (y + 1) = A \times B$
27	26	3exp	$⊢ y \in ℕ \to ((A \in U \land B \in V \land A \cap B \neq \emptyset) \to ((A \times B) ↑_{r} y = A \times B \to (A \times B) ↑_{r} (y + 1) = A \times B))$
28	27	a2d	$⊢ y \in ℕ \to (((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} y = A \times B) \to ((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} (y + 1) = A \times B))$
29	3 6 9 12 16 28	nnind	$⊢ N \in ℕ \to ((A \in U \land B \in V \land A \cap B \neq \emptyset) \to (A \times B) ↑_{r} N = A \times B)$

Metamath Proof Explorer

Theorem relexpxpnnidm

Proof