cdlemkuu - Mathbox for Norm Megill

	Mathbox for Norm Megill		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdlemkuu		Structured version Visualization version Unicode version

Theorem cdlemkuu 34533

Description: Convert between function and operation forms of

. TODO: Use operation form everywhere. (Contributed by NM, 6-Jul-2013.)

**Hypotheses**
Ref	Expression
cdlemk3.b
cdlemk3.l
cdlemk3.j	$.\/$
cdlemk3.m	$./\$
cdlemk3.a
cdlemk3.h
cdlemk3.t
cdlemk3.r
cdlemk3.s	$.\/$ $./\$ $.\/$
cdlemk3.u1	$.\/$ $./\$ $.\/$
cdlemk3.o2
cdlemk3.u2	$.\/$ $./\$ $.\/$

**Assertion**
Ref	Expression
cdlemkuu	$/\$

Distinct variable groups:

, $./\$

$.\/$ ,

Allowed substitution hints:

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

)

(

) $.\/$ (

)

(

)

(

) $./\$ (

)

(

)

(

)

(

)

(

)

**Proof of Theorem cdlemkuu**
Step	Hyp	Ref	Expression
1		fveq2 5879	. . . . . . . . 9
2		cdlemk3.o2	. . . . . . . . 9
3	1, 2	syl6eqr 2523	. . . . . . . 8
4	3	fveq1d 5881	. . . . . . 7
5		cnveq 5013	. . . . . . . . 9
6	5	coeq2d 5002	. . . . . . . 8
7	6	fveq2d 5883	. . . . . . 7
8	4, 7	oveq12d 6326	. . . . . 6 $.\/$ $.\/$
9	8	oveq2d 6324	. . . . 5 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
10	9	eqeq2d 2481	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
11	10	riotabidv 6272	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
12		fveq2 5879	. . . . . . 7
13	12	oveq2d 6324	. . . . . 6 $.\/$ $.\/$
14		coeq1 4997	. . . . . . . 8
15	14	fveq2d 5883	. . . . . . 7
16	15	oveq2d 6324	. . . . . 6 $.\/$ $.\/$
17	13, 16	oveq12d 6326	. . . . 5 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
18	17	eqeq2d 2481	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
19	18	riotabidv 6272	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
20		cdlemk3.u1	. . 3 $.\/$ $./\$ $.\/$
21		riotaex 6274	. . 3 $.\/$ $./\$ $.\/$
22	11, 19, 20, 21	ovmpt2 6451	. 2 $/\$ $.\/$ $./\$ $.\/$
23		cdlemk3.b	. . . 4
24		cdlemk3.l	. . . 4
25		cdlemk3.j	. . . 4 $.\/$
26		cdlemk3.a	. . . 4
27		cdlemk3.h	. . . 4
28		cdlemk3.t	. . . 4
29		cdlemk3.r	. . . 4
30		cdlemk3.m	. . . 4 $./\$
31		cdlemk3.u2	. . . 4 $.\/$ $./\$ $.\/$
32	23, 24, 25, 26, 27, 28, 29, 30, 31	cdlemksv 34482	. . 3 $.\/$ $./\$ $.\/$
33	32	adantl 473	. 2 $/\$ $.\/$ $./\$ $.\/$
34	22, 33	eqtr4d 2508	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 376

wceq 1452

wcel 1904

cmpt 4454

ccnv 4838

ccom 4843

cfv 5589

crio 6269 (class class class)co 6308

cmpt2 6310

cbs 15199

cple 15275

cjn 16267

cmee 16268

catm 32900

clh 33620

cltrn 33737

ctrl 33795

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1677 ax-4 1690 ax-5 1766 ax-6 1813 ax-7 1859 ax-9 1913 ax-10 1932 ax-11 1937 ax-12 1950 ax-13 2104 ax-ext 2451 ax-sep 4518 ax-nul 4527 ax-pr 4639

This theorem depends on definitions: df-bi 190 df-or 377 df-an 378 df-3an 1009 df-tru 1455 df-ex 1672 df-nf 1676 df-sb 1806 df-eu 2323 df-mo 2324 df-clab 2458 df-cleq 2464 df-clel 2467 df-nfc 2601 df-ne 2643 df-ral 2761 df-rex 2762 df-rab 2765 df-v 3033 df-sbc 3256 df-dif 3393 df-un 3395 df-in 3397 df-ss 3404 df-nul 3723 df-if 3873 df-sn 3960 df-pr 3962 df-op 3966 df-uni 4191 df-br 4396 df-opab 4455 df-mpt 4456 df-id 4754 df-xp 4845 df-rel 4846 df-cnv 4847 df-co 4848 df-dm 4849 df-iota 5553 df-fun 5591 df-fv 5597 df-riota 6270 df-ov 6311 df-oprab 6312 df-mpt2 6313

This theorem is referenced by: cdlemk31 34534 cdlemkuel-3 34536 cdlemkuv2-3N 34537 cdlemk18-3N 34538 cdlemk22-3 34539 cdlemkyu 34565

W3C validator