cvlcvr1 - Mathbox for Norm Megill

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

Theorem cvlcvr1 29826

Description: The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 23815 analog.) (Contributed by NM, 5-Nov-2012.)

**Hypotheses**
Ref	Expression
cvlcvr1.b
cvlcvr1.l
cvlcvr1.j	$.\/$
cvlcvr1.c
cvlcvr1.a

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

Proof of Theorem cvlcvr1 Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simp13 989	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
2		cvllat 29813	. . . . . . 7
3	1, 2	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$
4		simp2 958	. . . . . 6 $/\$ $/\$ $/\$ $/\$
5		cvlcvr1.b	. . . . . . . 8
6		cvlcvr1.a	. . . . . . . 8
7	5, 6	atbase 29776	. . . . . . 7
8	7	3ad2ant3 980	. . . . . 6 $/\$ $/\$ $/\$ $/\$
9		cvlcvr1.l	. . . . . . 7
10		eqid 2408	. . . . . . 7
11		cvlcvr1.j	. . . . . . 7 $.\/$
12	5, 9, 10, 11	latnle 14473	. . . . . 6 $/\$ $/\$ $.\/$
13	3, 4, 8, 12	syl3anc 1184	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$
14	13	biimpd 199	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
15		simpl13 1034	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
16	15, 2	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
17		simprll 739	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
18		simpl2 961	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
19		simpl3 962	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
20	19, 7	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
21	5, 11	latjcl 14438	. . . . . . . . 9 $/\$ $/\$ $.\/$
22	16, 18, 20, 21	syl3anc 1184	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
23		simprrr 742	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
24		simprrl 741	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
25		simpl11 1032	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
26		simpl12 1033	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
27		cvlatl 29812	. . . . . . . . . . . 12
28	15, 27	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
29	5, 9, 10, 6	atlrelat1 29808	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
30	25, 26, 28, 18, 17, 29	syl311anc 1198	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
31	24, 30	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
32	16	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
33	5, 6	atbase 29776	. . . . . . . . . . . . . 14
34	33	ad2antrl 709	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
35	17	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
36	22	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
37		simprrr 742	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
38	23	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
39	5, 9, 32, 34, 35, 36, 37, 38	lattrd 14446	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
40	15	adantr 452	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
41		simprl 733	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
42		simpll3 998	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
43		simpll2 997	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
44		simprrl 741	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
45	5, 9, 11, 6	cvlexch1 29815	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
46	40, 41, 42, 43, 44, 45	syl131anc 1197	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
47	39, 46	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
48		simprlr 740	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
49	48	adantr 452	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
50	5, 9, 11, 6	cvlexchb1 29817	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
51	40, 42, 41, 43, 49, 50	syl131anc 1197	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
52	47, 51	mpbid 202	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
53	9, 10	pltle 14377	. . . . . . . . . . . . . 14 $/\$ $/\$
54	25, 18, 17, 53	syl3anc 1184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
55	24, 54	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
56	55	adantr 452	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
57	5, 9, 11	latjle12 14450	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $.\/$
58	32, 43, 34, 35, 57	syl13anc 1186	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
59	56, 37, 58	mpbi2and 888	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
60	52, 59	eqbrtrd 4196	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
61	31, 60	rexlimddv 2798	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
62	5, 9, 16, 17, 22, 23, 61	latasymd 14445	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
63	62	exp44 597	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
64	63	imp 419	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
65	64	ralrimdva 2760	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
66	14, 65	jcad 520	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
67	3, 4, 8, 21	syl3anc 1184	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
68		cvlcvr1.c	. . . . 5
69	5, 9, 10, 68	cvrval2 29761	. . . 4 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
70	3, 4, 67, 69	syl3anc 1184	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
71	66, 70	sylibrd 226	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$
72	3	adantr 452	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
73		simpl2 961	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
74	67	adantr 452	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
75		simpr 448	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
76	5, 10, 68	cvrlt 29757	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
77	72, 73, 74, 75, 76	syl31anc 1187	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
78	77	ex 424	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
79	78, 13	sylibrd 226	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$
80	71, 79	impbid 184	1 $/\$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 177 $/\$ wa 359 $/\$ w3a 936

wceq 1649

wcel 1721

wral 2670

wrex 2671 class class class wbr 4176

cfv 5417 (class class class)co 6044

cbs 13428

cple 13495

cplt 14357

cjn 14360

clat 14433

ccla 14495

coml 29662

ccvr 29749

catm 29750

cal 29751

clc 29752

This theorem is referenced by: cvlcvrp 29827 cvr1 29896

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1552 ax-5 1563 ax-17 1623 ax-9 1662 ax-8 1683 ax-13 1723 ax-14 1725 ax-6 1740 ax-7 1745 ax-11 1757 ax-12 1946 ax-ext 2389 ax-rep 4284 ax-sep 4294 ax-nul 4302 ax-pow 4341 ax-pr 4367 ax-un 4664

This theorem depends on definitions: df-bi 178 df-or 360 df-an 361 df-3an 938 df-tru 1325 df-ex 1548 df-nf 1551 df-sb 1656 df-eu 2262 df-mo 2263 df-clab 2395 df-cleq 2401 df-clel 2404 df-nfc 2533 df-ne 2573 df-nel 2574 df-ral 2675 df-rex 2676 df-reu 2677 df-rab 2679 df-v 2922 df-sbc 3126 df-csb 3216 df-dif 3287 df-un 3289 df-in 3291 df-ss 3298 df-nul 3593 df-if 3704 df-pw 3765 df-sn 3784 df-pr 3785 df-op 3787 df-uni 3980 df-iun 4059 df-br 4177 df-opab 4231 df-mpt 4232 df-id 4462 df-xp 4847 df-rel 4848 df-cnv 4849 df-co 4850 df-dm 4851 df-rn 4852 df-res 4853 df-ima 4854 df-iota 5381 df-fun 5419 df-fn 5420 df-f 5421 df-f1 5422 df-fo 5423 df-f1o 5424 df-fv 5425 df-ov 6047 df-oprab 6048 df-mpt2 6049 df-1st 6312 df-2nd 6313 df-undef 6506 df-riota 6512 df-poset 14362 df-plt 14374 df-lub 14390 df-glb 14391 df-join 14392 df-meet 14393 df-p0 14427 df-lat 14434 df-clat 14496 df-oposet 29663 df-ol 29665 df-oml 29666 df-covers 29753 df-ats 29754 df-atl 29785 df-cvlat 29809

W3C validator