cdlemkuu - Mathbox for Norm Megill

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

Theorem cdlemkuu 35700

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 5865	. . . . . . . . 9
2		cdlemk3.o2	. . . . . . . . 9
3	1, 2	syl6eqr 2526	. . . . . . . 8
4	3	fveq1d 5867	. . . . . . 7
5		cnveq 5175	. . . . . . . . 9
6	5	coeq2d 5164	. . . . . . . 8
7	6	fveq2d 5869	. . . . . . 7
8	4, 7	oveq12d 6301	. . . . . 6 $.\/$ $.\/$
9	8	oveq2d 6299	. . . . 5 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
10	9	eqeq2d 2481	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
11	10	riotabidv 6246	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
12		fveq2 5865	. . . . . . 7
13	12	oveq2d 6299	. . . . . 6 $.\/$ $.\/$
14		coeq1 5159	. . . . . . . 8
15	14	fveq2d 5869	. . . . . . 7
16	15	oveq2d 6299	. . . . . 6 $.\/$ $.\/$
17	13, 16	oveq12d 6301	. . . . 5 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
18	17	eqeq2d 2481	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
19	18	riotabidv 6246	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
20		cdlemk3.u1	. . 3 $.\/$ $./\$ $.\/$
21		riotaex 6248	. . 3 $.\/$ $./\$ $.\/$
22	11, 19, 20, 21	ovmpt2 6421	. 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 35649	. . 3 $.\/$ $./\$ $.\/$
33	32	adantl 466	. 2 $/\$ $.\/$ $./\$ $.\/$
34	22, 33	eqtr4d 2511	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369

wceq 1379

wcel 1767

cmpt 4505

ccnv 4998

ccom 5003

cfv 5587

crio 6243 (class class class)co 6283

cmpt2 6285

cbs 14489

cple 14561

cjn 15430

cmee 15431

catm 34069

clh 34789

cltrn 34906

ctrl 34963

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-sep 4568 ax-nul 4576 ax-pr 4686

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 975 df-tru 1382 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-ral 2819 df-rex 2820 df-rab 2823 df-v 3115 df-sbc 3332 df-dif 3479 df-un 3481 df-in 3483 df-ss 3490 df-nul 3786 df-if 3940 df-sn 4028 df-pr 4030 df-op 4034 df-uni 4246 df-br 4448 df-opab 4506 df-mpt 4507 df-id 4795 df-xp 5005 df-rel 5006 df-cnv 5007 df-co 5008 df-dm 5009 df-iota 5550 df-fun 5589 df-fv 5595 df-riota 6244 df-ov 6286 df-oprab 6287 df-mpt2 6288

This theorem is referenced by: cdlemk31 35701 cdlemkuel-3 35703 cdlemkuv2-3N 35704 cdlemk18-3N 35705 cdlemk22-3 35706 cdlemkyu 35732

W3C validator