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 28808

Description: The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 22931 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 987	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
2		cvllat 28795	. . . . . . 7
3	1, 2	syl 15	. . . . . 6 $/\$ $/\$ $/\$ $/\$
4		simp2 956	. . . . . 6 $/\$ $/\$ $/\$ $/\$
5		cvlcvr1.b	. . . . . . . 8
6		cvlcvr1.a	. . . . . . . 8
7	5, 6	atbase 28758	. . . . . . 7
8	7	3ad2ant3 978	. . . . . 6 $/\$ $/\$ $/\$ $/\$
9		cvlcvr1.l	. . . . . . 7
10		eqid 2284	. . . . . . 7
11		cvlcvr1.j	. . . . . . 7 $.\/$
12	5, 9, 10, 11	latnle 14187	. . . . . 6 $/\$ $/\$ $.\/$
13	3, 4, 8, 12	syl3anc 1182	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$
14	13	biimpd 198	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
15		simpl13 1032	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
16	15, 2	syl 15	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
17		simprll 738	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
18		simpl2 959	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
19		simpl3 960	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
20	19, 7	syl 15	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
21	5, 11	latjcl 14152	. . . . . . . . 9 $/\$ $/\$ $.\/$
22	16, 18, 20, 21	syl3anc 1182	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
23		simprrr 741	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
24		simprrl 740	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
25		simpl11 1030	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
26		simpl12 1031	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
27		cvlatl 28794	. . . . . . . . . . . 12
28	15, 27	syl 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
29	5, 9, 10, 6	atlrelat1 28790	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
30	25, 26, 28, 18, 17, 29	syl311anc 1196	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
31	24, 30	mpd 14	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
32	16	adantr 451	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
33	5, 6	atbase 28758	. . . . . . . . . . . . . . . 16
34	33	ad2antrl 708	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
35	17	adantr 451	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
36	22	adantr 451	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
37		simprrr 741	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
38	23	adantr 451	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
39	5, 9, 32, 34, 35, 36, 37, 38	lattrd 14160	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
40	15	adantr 451	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
41		simprl 732	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
42		simpll3 996	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
43		simpll2 995	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
44		simprrl 740	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
45	5, 9, 11, 6	cvlexch1 28797	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
46	40, 41, 42, 43, 44, 45	syl131anc 1195	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
47	39, 46	mpd 14	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
48		simprlr 739	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
49	48	adantr 451	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
50	5, 9, 11, 6	cvlexchb1 28799	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
51	40, 42, 41, 43, 49, 50	syl131anc 1195	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
52	47, 51	mpbid 201	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
53	9, 10	pltle 14091	. . . . . . . . . . . . . . . 16 $/\$ $/\$
54	25, 18, 17, 53	syl3anc 1182	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
55	24, 54	mpd 14	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
56	55	adantr 451	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
57	5, 9, 11	latjle12 14164	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $.\/$
58	32, 43, 34, 35, 57	syl13anc 1184	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
59	56, 37, 58	mpbi2and 887	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
60	52, 59	eqbrtrd 4044	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
61	60	exp32 588	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
62	61	rexlimdv 2667	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
63	31, 62	mpd 14	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
64	5, 9, 16, 17, 22, 23, 63	latasymd 14159	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
65	64	exp44 596	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
66	65	imp 418	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
67	66	ralrimdva 2634	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
68	14, 67	jcad 519	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
69	3, 4, 8, 21	syl3anc 1182	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
70		cvlcvr1.c	. . . . 5
71	5, 9, 10, 70	cvrval2 28743	. . . 4 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
72	3, 4, 69, 71	syl3anc 1182	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
73	68, 72	sylibrd 225	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$
74	3	adantr 451	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
75		simpl2 959	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
76	69	adantr 451	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
77		simpr 447	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
78	5, 10, 70	cvrlt 28739	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
79	74, 75, 76, 77, 78	syl31anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
80	79	ex 423	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
81	80, 13	sylibrd 225	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$
82	73, 81	impbid 183	1 $/\$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

wb 176 $/\$ wa 358 $/\$ w3a 934

wceq 1623

wcel 1685

wral 2544

wrex 2545 class class class wbr 4024

cfv 5221 (class class class)co 5820

cbs 13144

cple 13211

cplt 14071

cjn 14074

clat 14147

ccla 14209

coml 28644

ccvr 28731

catm 28732

cal 28733

clc 28734

This theorem is referenced by: cvlcvrp 28809 cvr1 28878

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1533 ax-5 1544 ax-17 1603 ax-9 1636 ax-8 1644 ax-13 1687 ax-14 1689 ax-6 1704 ax-7 1709 ax-11 1716 ax-12 1868 ax-ext 2265 ax-rep 4132 ax-sep 4142 ax-nul 4150 ax-pow 4187 ax-pr 4213 ax-un 4511

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-tru 1310 df-ex 1529 df-nf 1532 df-sb 1631 df-eu 2148 df-mo 2149 df-clab 2271 df-cleq 2277 df-clel 2280 df-nfc 2409 df-ne 2449 df-nel 2450 df-ral 2549 df-rex 2550 df-reu 2551 df-rab 2553 df-v 2791 df-sbc 2993 df-csb 3083 df-dif 3156 df-un 3158 df-in 3160 df-ss 3167 df-nul 3457 df-if 3567 df-pw 3628 df-sn 3647 df-pr 3648 df-op 3650 df-uni 3829 df-iun 3908 df-br 4025 df-opab 4079 df-mpt 4080 df-id 4308 df-xp 4694 df-rel 4695 df-cnv 4696 df-co 4697 df-dm 4698 df-rn 4699 df-res 4700 df-ima 4701 df-fun 5223 df-fn 5224 df-f 5225 df-f1 5226 df-fo 5227 df-f1o 5228 df-fv 5229 df-ov 5823 df-oprab 5824 df-mpt2 5825 df-1st 6084 df-2nd 6085 df-iota 6253 df-undef 6292 df-riota 6300 df-poset 14076 df-plt 14088 df-lub 14104 df-glb 14105 df-join 14106 df-meet 14107 df-p0 14141 df-lat 14148 df-clat 14210 df-oposet 28645 df-ol 28647 df-oml 28648 df-covers 28735 df-ats 28736 df-atl 28767 df-cvlat 28791

W3C validator