dalemeea - Mathbox for Norm Megill

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

Theorem dalemeea 32937

Description: Lemma for dath 33010. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.)

**Assertion**
Ref	Expression
dalemeea

**Proof of Theorem dalemeea**
Step	Hyp	Ref	Expression
1		dalema.ph	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		dalemc.l	. . 3
3		dalemc.j	. . 3 $.\/$
4		dalemc.a	. . 3
5		dalemeea.y	. . 3 $.\/$ $.\/$
6		dalemeea.z	. . 3 $.\/$ $.\/$
7	1, 2, 3, 4, 5, 6	dalemrot 32931	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
8		biid 239	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
9		dalemeea.m	. . 3 $./\$
10		dalemeea.o	. . 3
11		eqid 2429	. . 3 $.\/$ $.\/$ $.\/$ $.\/$
12		eqid 2429	. . 3 $.\/$ $.\/$ $.\/$ $.\/$
13		dalemeea.e	. . 3 $.\/$ $./\$ $.\/$
14	8, 2, 3, 4, 9, 10, 11, 12, 13	dalemdea 32936	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
15	7, 14	syl 17	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 187 $/\$ wa 370 $/\$ w3a 982

wceq 1437

wcel 1870 class class class wbr 4426

cfv 5601 (class class class)co 6305

cbs 15084

cple 15159

cjn 16140

cmee 16141

catm 32538

chlt 32625

clpl 32766

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1665 ax-4 1678 ax-5 1751 ax-6 1797 ax-7 1841 ax-8 1872 ax-9 1874 ax-10 1889 ax-11 1894 ax-12 1907 ax-13 2055 ax-ext 2407 ax-rep 4538 ax-sep 4548 ax-nul 4556 ax-pow 4603 ax-pr 4661 ax-un 6597

This theorem depends on definitions: df-bi 188 df-or 371 df-an 372 df-3an 984 df-tru 1440 df-ex 1660 df-nf 1664 df-sb 1790 df-eu 2270 df-mo 2271 df-clab 2415 df-cleq 2421 df-clel 2424 df-nfc 2579 df-ne 2627 df-ral 2787 df-rex 2788 df-reu 2789 df-rab 2791 df-v 3089 df-sbc 3306 df-csb 3402 df-dif 3445 df-un 3447 df-in 3449 df-ss 3456 df-nul 3768 df-if 3916 df-pw 3987 df-sn 4003 df-pr 4005 df-op 4009 df-uni 4223 df-iun 4304 df-br 4427 df-opab 4485 df-mpt 4486 df-id 4769 df-xp 4860 df-rel 4861 df-cnv 4862 df-co 4863 df-dm 4864 df-rn 4865 df-res 4866 df-ima 4867 df-iota 5565 df-fun 5603 df-fn 5604 df-f 5605 df-f1 5606 df-fo 5607 df-f1o 5608 df-fv 5609 df-riota 6267 df-ov 6308 df-oprab 6309 df-preset 16124 df-poset 16142 df-plt 16155 df-lub 16171 df-glb 16172 df-join 16173 df-meet 16174 df-p0 16236 df-lat 16243 df-clat 16305 df-oposet 32451 df-ol 32453 df-oml 32454 df-covers 32541 df-ats 32542 df-atl 32573 df-cvlat 32597 df-hlat 32626 df-llines 32772 df-lplanes 32773

This theorem is referenced by: dalem16 32953 dalem60 33006