relexpsucnnr - Metamath Proof Explorer

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

Theorem relexpsucnnr 12945

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 2455	. . . 4 $/\$
2		simprr 755	. . . . 5 $/\$ $/\$ $/\$
3		dmeq 5192	. . . . . . . . . . 11
4		rneq 5217	. . . . . . . . . . 11
5	3, 4	uneq12d 3645	. . . . . . . . . 10
6	5	reseq2d 5262	. . . . . . . . 9
7		eqidd 2455	. . . . . . . . . . 11
8		coeq2 5150	. . . . . . . . . . . 12
9	8	mpt2eq3dv 6336	. . . . . . . . . . 11
10		id 22	. . . . . . . . . . . 12
11	10	mpteq2dv 4526	. . . . . . . . . . 11
12	7, 9, 11	seqeq123d 12101	. . . . . . . . . 10
13	12	fveq1d 5850	. . . . . . . . 9
14	6, 13	ifeq12d 3949	. . . . . . . 8
15	14	ad2antrl 725	. . . . . . 7 $/\$ $/\$ $/\$
16	15	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
17		eqeq1 2458	. . . . . . . 8
18	17	anbi2d 701	. . . . . . 7 $/\$ $/\$
19	18	anbi2d 701	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
20		eqeq1 2458	. . . . . . . 8
21		fveq2 5848	. . . . . . . 8
22	20, 21	ifbieq2d 3954	. . . . . . 7
23	22	eqeq1d 2456	. . . . . 6
24	16, 19, 23	3imtr4d 268	. . . . 5 $/\$ $/\$ $/\$
25	2, 24	mpcom 36	. . . 4 $/\$ $/\$ $/\$
26		elex 3115	. . . . 5
27	26	adantr 463	. . . 4 $/\$
28		simpr 459	. . . . . 6 $/\$
29	28	peano2nnd 10548	. . . . 5 $/\$
30	29	nnnn0d 10848	. . . 4 $/\$
31		dmexg 6704	. . . . . . . 8
32		rnexg 6705	. . . . . . . 8
33		unexg 6574	. . . . . . . 8 $/\$
34	31, 32, 33	syl2anc 659	. . . . . . 7
35		resiexg 6709	. . . . . . 7
36	34, 35	syl 16	. . . . . 6
37	36	adantr 463	. . . . 5 $/\$
38		fvex 5858	. . . . . 6
39	38	a1i 11	. . . . 5 $/\$
40	37, 39	ifcld 3972	. . . 4 $/\$
41	1, 25, 27, 30, 40	ovmpt2d 6403	. . 3 $/\$
42		nnne0 10564	. . . . . 6
43	42	neneqd 2656	. . . . 5
44	29, 43	syl 16	. . . 4 $/\$
45	44	iffalsed 3940	. . 3 $/\$
46		elnnuz 11118	. . . . . . 7
47	46	biimpi 194	. . . . . 6
48	47	adantl 464	. . . . 5 $/\$
49		seqp1 12107	. . . . 5
50	48, 49	syl 16	. . . 4 $/\$
51		ovex 6298	. . . . . 6
52		simpl 455	. . . . . 6 $/\$
53		eqidd 2455	. . . . . . 7
54		eqid 2454	. . . . . . 7
55	53, 54	fvmptg 5929	. . . . . 6 $/\$
56	51, 52, 55	sylancr 661	. . . . 5 $/\$
57	56	oveq2d 6286	. . . 4 $/\$
58		nfcv 2616	. . . . . . 7
59		nfcv 2616	. . . . . . 7
60		nfcv 2616	. . . . . . 7
61		nfcv 2616	. . . . . . 7
62		simpl 455	. . . . . . . 8 $/\$
63	62	coeq1d 5153	. . . . . . 7 $/\$
64	58, 59, 60, 61, 63	cbvmpt2 6349	. . . . . 6
65		oveq 6276	. . . . . 6
66	64, 65	mp1i 12	. . . . 5 $/\$
67		eqidd 2455	. . . . . 6 $/\$
68		simprl 754	. . . . . . 7 $/\$ $/\$ $/\$
69	68	coeq1d 5153	. . . . . 6 $/\$ $/\$ $/\$
70		fvex 5858	. . . . . . 7
71	70	a1i 11	. . . . . 6 $/\$
72		coexg 6724	. . . . . . 7 $/\$
73	70, 52, 72	sylancr 661	. . . . . 6 $/\$
74	67, 69, 71, 27, 73	ovmpt2d 6403	. . . . 5 $/\$
75		simpr 459	. . . . . . . . . . 11 $/\$
76	75	eqeq1d 2456	. . . . . . . . . 10 $/\$
77	6	adantr 463	. . . . . . . . . 10 $/\$
78	12	adantr 463	. . . . . . . . . . 11 $/\$
79	78, 75	fveq12d 5854	. . . . . . . . . 10 $/\$
80	76, 77, 79	ifbieq12d 3956	. . . . . . . . 9 $/\$
81	80	adantl 464	. . . . . . . 8 $/\$ $/\$ $/\$
82	28	nnnn0d 10848	. . . . . . . 8 $/\$
83	37, 71	ifcld 3972	. . . . . . . 8 $/\$
84	1, 81, 27, 82, 83	ovmpt2d 6403	. . . . . . 7 $/\$
85		nnne0 10564	. . . . . . . . . 10
86	85	adantl 464	. . . . . . . . 9 $/\$
87	86	neneqd 2656	. . . . . . . 8 $/\$
88	87	iffalsed 3940	. . . . . . 7 $/\$
89	84, 88	eqtr2d 2496	. . . . . 6 $/\$
90	89	coeq1d 5153	. . . . 5 $/\$
91	66, 74, 90	3eqtrd 2499	. . . 4 $/\$
92	50, 57, 91	3eqtrd 2499	. . 3 $/\$
93	41, 45, 92	3eqtrd 2499	. 2 $/\$
94		df-relexp 12941	. . 3
95		oveq 6276	. . . . 5
96		oveq 6276	. . . . . 6
97	96	coeq1d 5153	. . . . 5
98	95, 97	eqeq12d 2476	. . . 4
99	98	imbi2d 314	. . 3 $/\$ $/\$
100	94, 99	ax-mp 5	. 2 $/\$ $/\$
101	93, 100	mpbir 209	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 367

wceq 1398

wcel 1823

wne 2649

cvv 3106

cun 3459

cif 3929

cmpt 4497

cid 4779

cdm 4988

crn 4989

cres 4990

ccom 4992

cfv 5570 (class class class)co 6270

cmpt2 6272

cc0 9481

c1 9482

caddc 9484

cn 10531

cn0 10791

cuz 11082

cseq 12092

crelexp 12940

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1623 ax-4 1636 ax-5 1709 ax-6 1752 ax-7 1795 ax-8 1825 ax-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-sep 4560 ax-nul 4568 ax-pow 4615 ax-pr 4676 ax-un 6565 ax-cnex 9537 ax-resscn 9538 ax-1cn 9539 ax-icn 9540 ax-addcl 9541 ax-addrcl 9542 ax-mulcl 9543 ax-mulrcl 9544 ax-mulcom 9545 ax-addass 9546 ax-mulass 9547 ax-distr 9548 ax-i2m1 9549 ax-1ne0 9550 ax-1rid 9551 ax-rnegex 9552 ax-rrecex 9553 ax-cnre 9554 ax-pre-lttri 9555 ax-pre-lttrn 9556 ax-pre-ltadd 9557 ax-pre-mulgt0 9558

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 df-3or 972 df-3an 973 df-tru 1401 df-ex 1618 df-nf 1622 df-sb 1745 df-eu 2288 df-mo 2289 df-clab 2440 df-cleq 2446 df-clel 2449 df-nfc 2604 df-ne 2651 df-nel 2652 df-ral 2809 df-rex 2810 df-reu 2811 df-rab 2813 df-v 3108 df-sbc 3325 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-pss 3477 df-nul 3784 df-if 3930 df-pw 4001 df-sn 4017 df-pr 4019 df-tp 4021 df-op 4023 df-uni 4236 df-iun 4317 df-br 4440 df-opab 4498 df-mpt 4499 df-tr 4533 df-eprel 4780 df-id 4784 df-po 4789 df-so 4790 df-fr 4827 df-we 4829 df-ord 4870 df-on 4871 df-lim 4872 df-suc 4873 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-rn 4999 df-res 5000 df-ima 5001 df-iota 5534 df-fun 5572 df-fn 5573 df-f 5574 df-f1 5575 df-fo 5576 df-f1o 5577 df-fv 5578 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275 df-om 6674 df-2nd 6774 df-recs 7034 df-rdg 7068 df-er 7303 df-en 7510 df-dom 7511 df-sdom 7512 df-pnf 9619 df-mnf 9620 df-xr 9621 df-ltxr 9622 df-le 9623 df-sub 9798 df-neg 9799 df-nn 10532 df-n0 10792 df-z 10861 df-uz 11083 df-seq 12093 df-relexp 12941

This theorem is referenced by: relexpsucr 12947 relexpsucnnl 12950 relexpcnv 12953 relexprelg 12956 relexpnndm 12959 relexp2 38219 relexpss1d 38238 relexp0a 38244 relexpxpnnidm 38246 relexpmulnn 38248 trclrelexplem 38250 cotrclrcl 38253 cotrcltrcl 38254

W3C validator