dalem32 - Mathbox for Norm Megill

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

Theorem dalem32 35168

Description: Lemma for dath 35200. Analog of dalem27 35163 for

. (Contributed by NM, 8-Aug-2012.)

**Hypotheses**
Ref	Expression
dalem.ph	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
dalem.l
dalem.j	$.\/$
dalem.a
dalem.ps	$/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
dalem29.m	$./\$
dalem29.o
dalem29.y	$.\/$ $.\/$
dalem29.z	$.\/$ $.\/$
dalem29.h	$.\/$ $./\$ $.\/$

**Assertion**
Ref	Expression
dalem32	$/\$ $/\$ $.\/$

**Proof of Theorem dalem32**
Step	Hyp	Ref	Expression
1		dalem.ph	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
2		dalem.l	. . . 4
3		dalem.j	. . . 4 $.\/$
4		dalem.a	. . . 4
5		dalem29.y	. . . 4 $.\/$ $.\/$
6		dalem29.z	. . . 4 $.\/$ $.\/$
7	1, 2, 3, 4, 5, 6	dalemrot 35121	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
8	7	3ad2ant1 1018	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
9	1, 2, 3, 4, 5, 6	dalemrotyz 35122	. . 3 $/\$ $.\/$ $.\/$ $.\/$ $.\/$
10	9	3adant3 1017	. 2 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$
11		dalem.ps	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
12	1, 2, 3, 4, 11, 5	dalemrotps 35155	. . 3 $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
13	12	3adant2 1016	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
14		biid 236	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$
15		biid 236	. . 3 $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$
16		dalem29.m	. . 3 $./\$
17		dalem29.o	. . 3
18		eqid 2443	. . 3 $.\/$ $.\/$ $.\/$ $.\/$
19		eqid 2443	. . 3 $.\/$ $.\/$ $.\/$ $.\/$
20		dalem29.h	. . 3 $.\/$ $./\$ $.\/$
21	14, 2, 3, 4, 15, 16, 17, 18, 19, 20	dalem27 35163	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $/\$ $.\/$ $.\/$ $.\/$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $.\/$ $.\/$
22	8, 10, 13, 21	syl3anc 1229	1 $/\$ $/\$ $.\/$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 974

wceq 1383

wcel 1804

wne 2638 class class class wbr 4437

cfv 5578 (class class class)co 6281

cbs 14509

cple 14581

cjn 15447

cmee 15448

catm 34728

chlt 34815

clpl 34956

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1605 ax-4 1618 ax-5 1691 ax-6 1734 ax-7 1776 ax-8 1806 ax-9 1808 ax-10 1823 ax-11 1828 ax-12 1840 ax-13 1985 ax-ext 2421 ax-rep 4548 ax-sep 4558 ax-nul 4566 ax-pow 4615 ax-pr 4676 ax-un 6577

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3an 976 df-tru 1386 df-ex 1600 df-nf 1604 df-sb 1727 df-eu 2272 df-mo 2273 df-clab 2429 df-cleq 2435 df-clel 2438 df-nfc 2593 df-ne 2640 df-ral 2798 df-rex 2799 df-reu 2800 df-rab 2802 df-v 3097 df-sbc 3314 df-csb 3421 df-dif 3464 df-un 3466 df-in 3468 df-ss 3475 df-nul 3771 df-if 3927 df-pw 3999 df-sn 4015 df-pr 4017 df-op 4021 df-uni 4235 df-iun 4317 df-br 4438 df-opab 4496 df-mpt 4497 df-id 4785 df-xp 4995 df-rel 4996 df-cnv 4997 df-co 4998 df-dm 4999 df-rn 5000 df-res 5001 df-ima 5002 df-iota 5541 df-fun 5580 df-fn 5581 df-f 5582 df-f1 5583 df-fo 5584 df-f1o 5585 df-fv 5586 df-riota 6242 df-ov 6284 df-oprab 6285 df-preset 15431 df-poset 15449 df-plt 15462 df-lub 15478 df-glb 15479 df-join 15480 df-meet 15481 df-p0 15543 df-lat 15550 df-clat 15612 df-oposet 34641 df-ol 34643 df-oml 34644 df-covers 34731 df-ats 34732 df-atl 34763 df-cvlat 34787 df-hlat 34816 df-llines 34962 df-lplanes 34963

This theorem is referenced by: dalem36 35172 dalem51 35187 dalem52 35188

W3C validator