cvlcvr1 - Mathbox for Norm Megill

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

Theorem cvlcvr1 30139

Description: The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 23860 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 990	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
2		cvllat 30126	. . . . . . 7
3	1, 2	syl 16	. . . . . 6 $/\$ $/\$ $/\$ $/\$
4		simp2 959	. . . . . 6 $/\$ $/\$ $/\$ $/\$
5		cvlcvr1.b	. . . . . . . 8
6		cvlcvr1.a	. . . . . . . 8
7	5, 6	atbase 30089	. . . . . . 7
8	7	3ad2ant3 981	. . . . . 6 $/\$ $/\$ $/\$ $/\$
9		cvlcvr1.l	. . . . . . 7
10		eqid 2438	. . . . . . 7
11		cvlcvr1.j	. . . . . . 7 $.\/$
12	5, 9, 10, 11	latnle 14516	. . . . . 6 $/\$ $/\$ $.\/$
13	3, 4, 8, 12	syl3anc 1185	. . . . 5 $/\$ $/\$ $/\$ $/\$ $.\/$
14	13	biimpd 200	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
15		simpl13 1035	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
16	15, 2	syl 16	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
17		simprll 740	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
18		simpl2 962	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
19		simpl3 963	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
20	19, 7	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
21	5, 11	latjcl 14481	. . . . . . . . 9 $/\$ $/\$ $.\/$
22	16, 18, 20, 21	syl3anc 1185	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
23		simprrr 743	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
24		simprrl 742	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
25		simpl11 1033	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
26		simpl12 1034	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
27		cvlatl 30125	. . . . . . . . . . . 12
28	15, 27	syl 16	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
29	5, 9, 10, 6	atlrelat1 30121	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
30	25, 26, 28, 18, 17, 29	syl311anc 1199	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
31	24, 30	mpd 15	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$
32	16	adantr 453	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
33	5, 6	atbase 30089	. . . . . . . . . . . . . 14
34	33	ad2antrl 710	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
35	17	adantr 453	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
36	22	adantr 453	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
37		simprrr 743	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
38	23	adantr 453	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
39	5, 9, 32, 34, 35, 36, 37, 38	lattrd 14489	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
40	15	adantr 453	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
41		simprl 734	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
42		simpll3 999	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
43		simpll2 998	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
44		simprrl 742	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
45	5, 9, 11, 6	cvlexch1 30128	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
46	40, 41, 42, 43, 44, 45	syl131anc 1198	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
47	39, 46	mpd 15	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
48		simprlr 741	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
49	48	adantr 453	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
50	5, 9, 11, 6	cvlexchb1 30130	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
51	40, 42, 41, 43, 49, 50	syl131anc 1198	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $.\/$
52	47, 51	mpbid 203	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$ $.\/$
53	9, 10	pltle 14420	. . . . . . . . . . . . . 14 $/\$ $/\$
54	25, 18, 17, 53	syl3anc 1185	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
55	24, 54	mpd 15	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
56	55	adantr 453	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$
57	5, 9, 11	latjle12 14493	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $.\/$
58	32, 43, 34, 35, 57	syl13anc 1187	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $.\/$
59	56, 37, 58	mpbi2and 889	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
60	52, 59	eqbrtrd 4234	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $/\$ $.\/$
61	31, 60	rexlimddv 2836	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
62	5, 9, 16, 17, 22, 23, 61	latasymd 14488	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
63	62	exp44 598	. . . . . 6 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
64	63	imp 420	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
65	64	ralrimdva 2798	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
66	14, 65	jcad 521	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
67	3, 4, 8, 21	syl3anc 1185	. . . 4 $/\$ $/\$ $/\$ $/\$ $.\/$
68		cvlcvr1.c	. . . . 5
69	5, 9, 10, 68	cvrval2 30074	. . . 4 $/\$ $/\$ $.\/$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
70	3, 4, 67, 69	syl3anc 1185	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$ $/\$ $/\$ $.\/$ $.\/$
71	66, 70	sylibrd 227	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$
72	3	adantr 453	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
73		simpl2 962	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$
74	67	adantr 453	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
75		simpr 449	. . . . 5 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
76	5, 10, 68	cvrlt 30070	. . . . 5 $/\$ $/\$ $.\/$ $/\$ $.\/$ $.\/$
77	72, 73, 74, 75, 76	syl31anc 1188	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
78	77	ex 425	. . 3 $/\$ $/\$ $/\$ $/\$ $.\/$ $.\/$
79	78, 13	sylibrd 227	. 2 $/\$ $/\$ $/\$ $/\$ $.\/$
80	71, 79	impbid 185	1 $/\$ $/\$ $/\$ $/\$ $.\/$

Colors of variables: wff set class

Syntax hints:

wn 3

wi 4

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

wceq 1653

wcel 1726

wral 2707

wrex 2708 class class class wbr 4214

cfv 5456 (class class class)co 6083

cbs 13471

cple 13538

cplt 14400

cjn 14403

clat 14476

ccla 14538

coml 29975

ccvr 30062

catm 30063

cal 30064

clc 30065

This theorem is referenced by: cvlcvrp 30140 cvr1 30209

This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 ax-gen 1556 ax-5 1567 ax-17 1627 ax-9 1667 ax-8 1688 ax-13 1728 ax-14 1730 ax-6 1745 ax-7 1750 ax-11 1762 ax-12 1951 ax-ext 2419 ax-rep 4322 ax-sep 4332 ax-nul 4340 ax-pow 4379 ax-pr 4405 ax-un 4703

This theorem depends on definitions: df-bi 179 df-or 361 df-an 362 df-3an 939 df-tru 1329 df-ex 1552 df-nf 1555 df-sb 1660 df-eu 2287 df-mo 2288 df-clab 2425 df-cleq 2431 df-clel 2434 df-nfc 2563 df-ne 2603 df-nel 2604 df-ral 2712 df-rex 2713 df-reu 2714 df-rab 2716 df-v 2960 df-sbc 3164 df-csb 3254 df-dif 3325 df-un 3327 df-in 3329 df-ss 3336 df-nul 3631 df-if 3742 df-pw 3803 df-sn 3822 df-pr 3823 df-op 3825 df-uni 4018 df-iun 4097 df-br 4215 df-opab 4269 df-mpt 4270 df-id 4500 df-xp 4886 df-rel 4887 df-cnv 4888 df-co 4889 df-dm 4890 df-rn 4891 df-res 4892 df-ima 4893 df-iota 5420 df-fun 5458 df-fn 5459 df-f 5460 df-f1 5461 df-fo 5462 df-f1o 5463 df-fv 5464 df-ov 6086 df-oprab 6087 df-mpt2 6088 df-1st 6351 df-2nd 6352 df-undef 6545 df-riota 6551 df-poset 14405 df-plt 14417 df-lub 14433 df-glb 14434 df-join 14435 df-meet 14436 df-p0 14470 df-lat 14477 df-clat 14539 df-oposet 29976 df-ol 29978 df-oml 29979 df-covers 30066 df-ats 30067 df-atl 30098 df-cvlat 30122

W3C validator