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 28779

Description: The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 22896 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**
Step	Hyp	Ref	Expression
1		simp13 992	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
2		cvllat 28766	. . . . . . 7
3	1, 2	syl 17	. . . . . 6 $/\$ $/\$ $/\$ $/\$
4		simp2 961	. . . . . 6 $/\$ $/\$ $/\$ $/\$
5		cvlcvr1.b	. . . . . . . 8
6		cvlcvr1.a	. . . . . . . 8
7	5, 6	atbase 28729	. . . . . . 7
8	7	3ad2ant3 983	. . . . . 6 $/\$ $/\$ $/\$ $/\$
9		cvlcvr1.l	. . . . . . 7
10		eqid 2258	. . . . . . 7
11		cvlcvr1.j	. . . . . . 7 $.\/$
12	5, 9, 10, 11	latnle 14154	. . . . . 6 $/\$ $/\$ $.\/$
13	3, 4, 8, 12	syl3anc 1187	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$
14	13	biimpd 200	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
15		simpl13 1037	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
16	15, 2	syl 17	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
17		simprll 741	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
18		simpl2 964	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
19		simpl3 965	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
20	19, 7	syl 17	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
21	5, 11	latjcl 14119	. . . . . . . . 9 $/\$ $/\$ $.\/$
22	16, 18, 20, 21	syl3anc 1187	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
23		simprrr 744	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
24		simprrl 743	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
25		simpl11 1035	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
26		simpl12 1036	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
27		cvlatl 28765	. . . . . . . . . . . 12
28	15, 27	syl 17	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
29	5, 9, 10, 6	atlrelat1 28761	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
30	25, 26, 28, 18, 17, 29	syl311anc 1201	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
31	24, 30	mpd 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
32	16	adantr 453	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
33	5, 6	atbase 28729	. . . . . . . . . . . . . . . 16
34	33	ad2antrl 711	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
35	17	adantr 453	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
36	22	adantr 453	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
37		simprrr 744	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
38	23	adantr 453	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
39	5, 9, 32, 34, 35, 36, 37, 38	lattrd 14127	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
40	15	adantr 453	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
41		simprl 735	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
42		simpll3 1001	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
43		simpll2 1000	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
44		simprrl 743	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
45	5, 9, 11, 6	cvlexch1 28768	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
46	40, 41, 42, 43, 44, 45	syl131anc 1200	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
47	39, 46	mpd 16	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
48		simprlr 742	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
49	48	adantr 453	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
50	5, 9, 11, 6	cvlexchb1 28770	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
51	40, 42, 41, 43, 49, 50	syl131anc 1200	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
52	47, 51	mpbid 203	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
53	9, 10	pltle 14058	. . . . . . . . . . . . . . . 16 $/\$ $/\$
54	25, 18, 17, 53	syl3anc 1187	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
55	24, 54	mpd 16	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
56	55	adantr 453	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
57	5, 9, 11	latjle12 14131	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $.\/$
58	32, 43, 34, 35, 57	syl13anc 1189	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
59	56, 37, 58	mpbi2and 892	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
60	52, 59	eqbrtrd 4017	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
61	60	exp32 591	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
62	61	rexlimdv 2641	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $.\/$
63	31, 62	mpd 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
64	5, 9, 16, 17, 22, 23, 63	latasymd 14126	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
65	64	exp44 599	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
66	65	imp 420	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
67	66	ralrimdva 2608	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
68	14, 67	jcad 521	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
69	3, 4, 8, 21	syl3anc 1187	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
70		cvlcvr1.c	. . . . 5
71	5, 9, 10, 70	cvrval2 28714	. . . 4 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
72	3, 4, 69, 71	syl3anc 1187	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
73	68, 72	sylibrd 227	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$
74	3	adantr 453	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
75		simpl2 964	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
76	69	adantr 453	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
77		simpr 449	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
78	5, 10, 70	cvrlt 28710	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
79	74, 75, 76, 77, 78	syl31anc 1190	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
80	79	ex 425	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
81	80, 13	sylibrd 227	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$
82	73, 81	impbid 185	1 $/\$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff set class

Syntax hints:

wn 5

wi 6

wb 178 $/\$ wa 360 $/\$ w3a 939

wceq 1619

wcel 1621

wral 2518

wrex 2519 class class class wbr 3997

cfv 4673 (class class class)co 5792

cbs 13111

cple 13178

cplt 14038

cjn 14041

clat 14114

ccla 14176

coml 28615

ccvr 28702

catm 28703

cal 28704

clc 28705

This theorem is referenced by: cvlcvrp 28780 cvr1 28849

This theorem was proved from axioms: ax-1 7 ax-2 8 ax-3 9 ax-mp 10 ax-5 1533 ax-6 1534 ax-7 1535 ax-gen 1536 ax-8 1623 ax-11 1624 ax-13 1625 ax-14 1626 ax-17 1628 ax-12o 1664 ax-10 1678 ax-9 1684 ax-4 1692 ax-16 1927 ax-ext 2239 ax-rep 4105 ax-sep 4115 ax-nul 4123 ax-pow 4160 ax-pr 4186 ax-un 4484

This theorem depends on definitions: df-bi 179 df-or 361 df-an 362 df-3an 941 df-tru 1315 df-ex 1538 df-nf 1540 df-sb 1884 df-eu 2122 df-mo 2123 df-clab 2245 df-cleq 2251 df-clel 2254 df-nfc 2383 df-ne 2423 df-nel 2424 df-ral 2523 df-rex 2524 df-reu 2525 df-rab 2527 df-v 2765 df-sbc 2967 df-csb 3057 df-dif 3130 df-un 3132 df-in 3134 df-ss 3141 df-nul 3431 df-if 3540 df-pw 3601 df-sn 3620 df-pr 3621 df-op 3623 df-uni 3802 df-iun 3881 df-br 3998 df-opab 4052 df-mpt 4053 df-id 4281 df-xp 4675 df-rel 4676 df-cnv 4677 df-co 4678 df-dm 4679 df-rn 4680 df-res 4681 df-ima 4682 df-fun 4683 df-fn 4684 df-f 4685 df-f1 4686 df-fo 4687 df-f1o 4688 df-fv 4689 df-ov 5795 df-oprab 5796 df-mpt2 5797 df-1st 6056 df-2nd 6057 df-iota 6225 df-undef 6264 df-riota 6272 df-poset 14043 df-plt 14055 df-lub 14071 df-glb 14072 df-join 14073 df-meet 14074 df-p0 14108 df-lat 14115 df-clat 14177 df-oposet 28616 df-ol 28618 df-oml 28619 df-covers 28706 df-ats 28707 df-atl 28738 df-cvlat 28762

W3C validator