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 37018

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 5848	. . . . . . . . 9
2		cdlemk3.o2	. . . . . . . . 9
3	1, 2	syl6eqr 2513	. . . . . . . 8
4	3	fveq1d 5850	. . . . . . 7
5		cnveq 5165	. . . . . . . . 9
6	5	coeq2d 5154	. . . . . . . 8
7	6	fveq2d 5852	. . . . . . 7
8	4, 7	oveq12d 6288	. . . . . 6 $.\/$ $.\/$
9	8	oveq2d 6286	. . . . 5 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
10	9	eqeq2d 2468	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
11	10	riotabidv 6234	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
12		fveq2 5848	. . . . . . 7
13	12	oveq2d 6286	. . . . . 6 $.\/$ $.\/$
14		coeq1 5149	. . . . . . . 8
15	14	fveq2d 5852	. . . . . . 7
16	15	oveq2d 6286	. . . . . 6 $.\/$ $.\/$
17	13, 16	oveq12d 6288	. . . . 5 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
18	17	eqeq2d 2468	. . . 4 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
19	18	riotabidv 6234	. . 3 $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$
20		cdlemk3.u1	. . 3 $.\/$ $./\$ $.\/$
21		riotaex 6236	. . 3 $.\/$ $./\$ $.\/$
22	11, 19, 20, 21	ovmpt2 6411	. 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 36967	. . 3 $.\/$ $./\$ $.\/$
33	32	adantl 464	. 2 $/\$ $.\/$ $./\$ $.\/$
34	22, 33	eqtr4d 2498	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 367

wceq 1398

wcel 1823

cmpt 4497

ccnv 4987

ccom 4992

cfv 5570

crio 6231 (class class class)co 6270

cmpt2 6272

cbs 14716

cple 14791

cjn 15772

cmee 15773

catm 35385

clh 36105

cltrn 36222

ctrl 36280

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-9 1827 ax-10 1842 ax-11 1847 ax-12 1859 ax-13 2004 ax-ext 2432 ax-sep 4560 ax-nul 4568 ax-pr 4676

This theorem depends on definitions: df-bi 185 df-or 368 df-an 369 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-ral 2809 df-rex 2810 df-rab 2813 df-v 3108 df-sbc 3325 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-nul 3784 df-if 3930 df-sn 4017 df-pr 4019 df-op 4023 df-uni 4236 df-br 4440 df-opab 4498 df-mpt 4499 df-id 4784 df-xp 4994 df-rel 4995 df-cnv 4996 df-co 4997 df-dm 4998 df-iota 5534 df-fun 5572 df-fv 5578 df-riota 6232 df-ov 6273 df-oprab 6274 df-mpt2 6275

This theorem is referenced by: cdlemk31 37019 cdlemkuel-3 37021 cdlemkuv2-3N 37022 cdlemk18-3N 37023 cdlemk22-3 37024 cdlemkyu 37050

W3C validator