relexpsucnnr - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > relexpsucnnr		Structured version Visualization version Unicode version

Theorem relexpsucnnr 13088

Description: A reduction for relation exponentiation to the right. (Contributed by RP, 22-May-2020.)

**Assertion**
Ref	Expression
relexpsucnnr	$/\$

Proof of Theorem relexpsucnnr Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqidd 2452	. . . 4 $/\$
2		simprr 766	. . . . 5 $/\$ $/\$ $/\$
3		dmeq 5035	. . . . . . . . . . 11
4		rneq 5060	. . . . . . . . . . 11
5	3, 4	uneq12d 3589	. . . . . . . . . 10
6	5	reseq2d 5105	. . . . . . . . 9
7		eqidd 2452	. . . . . . . . . . 11
8		coeq2 4993	. . . . . . . . . . . 12
9	8	mpt2eq3dv 6357	. . . . . . . . . . 11
10		id 22	. . . . . . . . . . . 12
11	10	mpteq2dv 4490	. . . . . . . . . . 11
12	7, 9, 11	seqeq123d 12222	. . . . . . . . . 10
13	12	fveq1d 5867	. . . . . . . . 9
14	6, 13	ifeq12d 3901	. . . . . . . 8
15	14	ad2antrl 734	. . . . . . 7 $/\$ $/\$ $/\$
16	15	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
17		eqeq1 2455	. . . . . . . 8
18	17	anbi2d 710	. . . . . . 7 $/\$ $/\$
19	18	anbi2d 710	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		eqeq1 2455	. . . . . . . 8
21		fveq2 5865	. . . . . . . 8
22	20, 21	ifbieq2d 3906	. . . . . . 7
23	22	eqeq1d 2453	. . . . . 6
24	16, 19, 23	3imtr4d 272	. . . . 5 $/\$ $/\$ $/\$
25	2, 24	mpcom 37	. . . 4 $/\$ $/\$ $/\$
26		elex 3054	. . . . 5
27	26	adantr 467	. . . 4 $/\$
28		simpr 463	. . . . . 6 $/\$
29	28	peano2nnd 10626	. . . . 5 $/\$
30	29	nnnn0d 10925	. . . 4 $/\$
31		dmexg 6724	. . . . . . . 8
32		rnexg 6725	. . . . . . . 8
33		unexg 6592	. . . . . . . 8 $/\$
34	31, 32, 33	syl2anc 667	. . . . . . 7
35		resiexg 6729	. . . . . . 7
36	34, 35	syl 17	. . . . . 6
37	36	adantr 467	. . . . 5 $/\$
38		fvex 5875	. . . . . 6
39	38	a1i 11	. . . . 5 $/\$
40	37, 39	ifcld 3924	. . . 4 $/\$
41	1, 25, 27, 30, 40	ovmpt2d 6424	. . 3 $/\$
42		nnne0 10642	. . . . . 6
43	42	neneqd 2629	. . . . 5
44	29, 43	syl 17	. . . 4 $/\$
45	44	iffalsed 3892	. . 3 $/\$
46		elnnuz 11195	. . . . . . 7
47	46	biimpi 198	. . . . . 6
48	47	adantl 468	. . . . 5 $/\$
49		seqp1 12228	. . . . 5
50	48, 49	syl 17	. . . 4 $/\$
51		ovex 6318	. . . . . 6
52		simpl 459	. . . . . 6 $/\$
53		eqidd 2452	. . . . . . 7
54		eqid 2451	. . . . . . 7
55	53, 54	fvmptg 5946	. . . . . 6 $/\$
56	51, 52, 55	sylancr 669	. . . . 5 $/\$
57	56	oveq2d 6306	. . . 4 $/\$
58		nfcv 2592	. . . . . . 7
59		nfcv 2592	. . . . . . 7
60		nfcv 2592	. . . . . . 7
61		nfcv 2592	. . . . . . 7
62		simpl 459	. . . . . . . 8 $/\$
63	62	coeq1d 4996	. . . . . . 7 $/\$
64	58, 59, 60, 61, 63	cbvmpt2 6370	. . . . . 6
65		oveq 6296	. . . . . 6
66	64, 65	mp1i 13	. . . . 5 $/\$
67		eqidd 2452	. . . . . 6 $/\$
68		simprl 764	. . . . . . 7 $/\$ $/\$ $/\$
69	68	coeq1d 4996	. . . . . 6 $/\$ $/\$ $/\$
70		fvex 5875	. . . . . . 7
71	70	a1i 11	. . . . . 6 $/\$
72		coexg 6744	. . . . . . 7 $/\$
73	70, 52, 72	sylancr 669	. . . . . 6 $/\$
74	67, 69, 71, 27, 73	ovmpt2d 6424	. . . . 5 $/\$
75		simpr 463	. . . . . . . . . . 11 $/\$
76	75	eqeq1d 2453	. . . . . . . . . 10 $/\$
77	6	adantr 467	. . . . . . . . . 10 $/\$
78	12	adantr 467	. . . . . . . . . . 11 $/\$
79	78, 75	fveq12d 5871	. . . . . . . . . 10 $/\$
80	76, 77, 79	ifbieq12d 3908	. . . . . . . . 9 $/\$
81	80	adantl 468	. . . . . . . 8 $/\$ $/\$ $/\$
82	28	nnnn0d 10925	. . . . . . . 8 $/\$
83	37, 71	ifcld 3924	. . . . . . . 8 $/\$
84	1, 81, 27, 82, 83	ovmpt2d 6424	. . . . . . 7 $/\$
85		nnne0 10642	. . . . . . . . . 10
86	85	adantl 468	. . . . . . . . 9 $/\$
87	86	neneqd 2629	. . . . . . . 8 $/\$
88	87	iffalsed 3892	. . . . . . 7 $/\$
89	84, 88	eqtr2d 2486	. . . . . 6 $/\$
90	89	coeq1d 4996	. . . . 5 $/\$
91	66, 74, 90	3eqtrd 2489	. . . 4 $/\$
92	50, 57, 91	3eqtrd 2489	. . 3 $/\$
93	41, 45, 92	3eqtrd 2489	. 2 $/\$
94		df-relexp 13084	. . 3
95		oveq 6296	. . . . 5
96		oveq 6296	. . . . . 6
97	96	coeq1d 4996	. . . . 5
98	95, 97	eqeq12d 2466	. . . 4
99	98	imbi2d 318	. . 3 $/\$ $/\$
100	94, 99	ax-mp 5	. 2 $/\$ $/\$
101	93, 100	mpbir 213	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 188 $/\$ wa 371

wceq 1444

wcel 1887

wne 2622

cvv 3045

cun 3402

cif 3881

cmpt 4461

cid 4744

cdm 4834

crn 4835

cres 4836

ccom 4838

cfv 5582 (class class class)co 6290

cmpt2 6292

cc0 9539

c1 9540

caddc 9542

cn 10609

cn0 10869

cuz 11159

cseq 12213

crelexp 13083

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1669 ax-4 1682 ax-5 1758 ax-6 1805 ax-7 1851 ax-8 1889 ax-9 1896 ax-10 1915 ax-11 1920 ax-12 1933 ax-13 2091 ax-ext 2431 ax-sep 4525 ax-nul 4534 ax-pow 4581 ax-pr 4639 ax-un 6583 ax-cnex 9595 ax-resscn 9596 ax-1cn 9597 ax-icn 9598 ax-addcl 9599 ax-addrcl 9600 ax-mulcl 9601 ax-mulrcl 9602 ax-mulcom 9603 ax-addass 9604 ax-mulass 9605 ax-distr 9606 ax-i2m1 9607 ax-1ne0 9608 ax-1rid 9609 ax-rnegex 9610 ax-rrecex 9611 ax-cnre 9612 ax-pre-lttri 9613 ax-pre-lttrn 9614 ax-pre-ltadd 9615 ax-pre-mulgt0 9616

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 986 df-3an 987 df-tru 1447 df-ex 1664 df-nf 1668 df-sb 1798 df-eu 2303 df-mo 2304 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2581 df-ne 2624 df-nel 2625 df-ral 2742 df-rex 2743 df-reu 2744 df-rab 2746 df-v 3047 df-sbc 3268 df-csb 3364 df-dif 3407 df-un 3409 df-in 3411 df-ss 3418 df-pss 3420 df-nul 3732 df-if 3882 df-pw 3953 df-sn 3969 df-pr 3971 df-tp 3973 df-op 3975 df-uni 4199 df-iun 4280 df-br 4403 df-opab 4462 df-mpt 4463 df-tr 4498 df-eprel 4745 df-id 4749 df-po 4755 df-so 4756 df-fr 4793 df-we 4795 df-xp 4840 df-rel 4841 df-cnv 4842 df-co 4843 df-dm 4844 df-rn 4845 df-res 4846 df-ima 4847 df-pred 5380 df-ord 5426 df-on 5427 df-lim 5428 df-suc 5429 df-iota 5546 df-fun 5584 df-fn 5585 df-f 5586 df-f1 5587 df-fo 5588 df-f1o 5589 df-fv 5590 df-riota 6252 df-ov 6293 df-oprab 6294 df-mpt2 6295 df-om 6693 df-2nd 6794 df-wrecs 7028 df-recs 7090 df-rdg 7128 df-er 7363 df-en 7570 df-dom 7571 df-sdom 7572 df-pnf 9677 df-mnf 9678 df-xr 9679 df-ltxr 9680 df-le 9681 df-sub 9862 df-neg 9863 df-nn 10610 df-n0 10870 df-z 10938 df-uz 11160 df-seq 12214 df-relexp 13084

This theorem is referenced by: relexpsucr 13092 relexpsucnnl 13095 relexpcnv 13098 relexprelg 13101 relexpnndm 13104 relexp2 36269 relexpxpnnidm 36295 relexpss1d 36297 relexpmulnn 36301 trclrelexplem 36303 relexp0a 36308 trclfvcom 36315 cotrcltrcl 36317 trclfvdecomr 36320 cotrclrcl 36334

W3C validator