Metamath Proof Explorer


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 NAUBVABA×BrN=A×B

Proof

Step Hyp Ref Expression
1 oveq2 x=1A×Brx=A×Br1
2 1 eqeq1d x=1A×Brx=A×BA×Br1=A×B
3 2 imbi2d x=1AUBVABA×Brx=A×BAUBVABA×Br1=A×B
4 oveq2 x=yA×Brx=A×Bry
5 4 eqeq1d x=yA×Brx=A×BA×Bry=A×B
6 5 imbi2d x=yAUBVABA×Brx=A×BAUBVABA×Bry=A×B
7 oveq2 x=y+1A×Brx=A×Bry+1
8 7 eqeq1d x=y+1A×Brx=A×BA×Bry+1=A×B
9 8 imbi2d x=y+1AUBVABA×Brx=A×BAUBVABA×Bry+1=A×B
10 oveq2 x=NA×Brx=A×BrN
11 10 eqeq1d x=NA×Brx=A×BA×BrN=A×B
12 11 imbi2d x=NAUBVABA×Brx=A×BAUBVABA×BrN=A×B
13 3simpa AUBVABAUBV
14 xpexg AUBVA×BV
15 relexp1g A×BVA×Br1=A×B
16 13 14 15 3syl AUBVABA×Br1=A×B
17 simp2 yAUBVABA×Bry=A×BAUBVAB
18 17 13 14 3syl yAUBVABA×Bry=A×BA×BV
19 simp1 yAUBVABA×Bry=A×By
20 relexpsucnnr A×BVyA×Bry+1=A×BryA×B
21 18 19 20 syl2anc yAUBVABA×Bry=A×BA×Bry+1=A×BryA×B
22 simp3 yAUBVABA×Bry=A×BA×Bry=A×B
23 22 coeq1d yAUBVABA×Bry=A×BA×BryA×B=A×BA×B
24 simp23 yAUBVABA×Bry=A×BAB
25 24 xpcoidgend yAUBVABA×Bry=A×BA×BA×B=A×B
26 21 23 25 3eqtrd yAUBVABA×Bry=A×BA×Bry+1=A×B
27 26 3exp yAUBVABA×Bry=A×BA×Bry+1=A×B
28 27 a2d yAUBVABA×Bry=A×BAUBVABA×Bry+1=A×B
29 3 6 9 12 16 28 nnind NAUBVABA×BrN=A×B