Theorem 4atexlemnclw 37238

Description: Lemma for 4atexlem7 37243. (Contributed by NM, 24-Nov-2012.)

Hypotheses

Ref	Expression
4thatlem.ph	⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))
4thatlem0.l	⊢ ≤ = (le‘𝐾)
4thatlem0.j	⊢ ∨ = (join‘𝐾)
4thatlem0.m	⊢ ∧ = (meet‘𝐾)
4thatlem0.a	⊢ 𝐴 = (Atoms‘𝐾)
4thatlem0.h	⊢ 𝐻 = (LHyp‘𝐾)
4thatlem0.u	⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
4thatlem0.v	⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)
4thatlem0.c	⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))

Assertion

Ref	Expression
4atexlemnclw	⊢ (𝜑 → ¬ 𝐶 ≤ 𝑊)

Proof of Theorem 4atexlemnclw

Step	Hyp	Ref	Expression
1		4thatlem0.c	. . . 4 ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆))
2		4thatlem.ph	. . . . . 6 ⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))))
3	2	4atexlemkl 37225	. . . . 5 ⊢ (𝜑 → 𝐾 ∈ Lat)
4		4thatlem0.j	. . . . . 6 ⊢ ∨ = (join‘𝐾)
5		4thatlem0.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
6	2, 4, 5	4atexlemqtb 37229	. . . . 5 ⊢ (𝜑 → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾))
7	2, 4, 5	4atexlempsb 37228	. . . . 5 ⊢ (𝜑 → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾))
8		eqid 2821	. . . . . 6 ⊢ (Base‘𝐾) = (Base‘𝐾)
9		4thatlem0.l	. . . . . 6 ⊢ ≤ = (le‘𝐾)
10		4thatlem0.m	. . . . . 6 ⊢ ∧ = (meet‘𝐾)
11	8, 9, 10	latmle1 17669	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑇))
12	3, 6, 7, 11	syl3anc 1367	. . . 4 ⊢ (𝜑 → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑄 ∨ 𝑇))
13	1, 12	eqbrtrid 5087	. . 3 ⊢ (𝜑 → 𝐶 ≤ (𝑄 ∨ 𝑇))
14		simp13r 1285	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑄 ≤ 𝑊)
15	2, 14	sylbi 219	. . . 4 ⊢ (𝜑 → ¬ 𝑄 ≤ 𝑊)
16	2	4atexlemkc 37226	. . . . . 6 ⊢ (𝜑 → 𝐾 ∈ CvLat)
17		4thatlem0.h	. . . . . . 7 ⊢ 𝐻 = (LHyp‘𝐾)
18		4thatlem0.u	. . . . . . 7 ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊)
19		4thatlem0.v	. . . . . . 7 ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊)
20	2, 9, 4, 10, 5, 17, 18, 19	4atexlemv 37233	. . . . . 6 ⊢ (𝜑 → 𝑉 ∈ 𝐴)
21	2	4atexlemq 37219	. . . . . 6 ⊢ (𝜑 → 𝑄 ∈ 𝐴)
22	2	4atexlemt 37221	. . . . . 6 ⊢ (𝜑 → 𝑇 ∈ 𝐴)
23	2, 9, 4, 10, 5, 17, 18	4atexlemu 37232	. . . . . . 7 ⊢ (𝜑 → 𝑈 ∈ 𝐴)
24	2, 9, 4, 10, 5, 17, 18, 19	4atexlemunv 37234	. . . . . . 7 ⊢ (𝜑 → 𝑈 ≠ 𝑉)
25	2	4atexlemutvt 37222	. . . . . . 7 ⊢ (𝜑 → (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))
26	5, 4	cvlsupr6 36515	. . . . . . . 8 ⊢ ((𝐾 ∈ CvLat ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ≠ 𝑉 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) → 𝑇 ≠ 𝑉)
27	26	necomd 3071	. . . . . . 7 ⊢ ((𝐾 ∈ CvLat ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ≠ 𝑉 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) → 𝑉 ≠ 𝑇)
28	16, 23, 20, 22, 24, 25, 27	syl132anc 1384	. . . . . 6 ⊢ (𝜑 → 𝑉 ≠ 𝑇)
29	9, 4, 5	cvlatexch2 36505	. . . . . 6 ⊢ ((𝐾 ∈ CvLat ∧ (𝑉 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ 𝑉 ≠ 𝑇) → (𝑉 ≤ (𝑄 ∨ 𝑇) → 𝑄 ≤ (𝑉 ∨ 𝑇)))
30	16, 20, 21, 22, 28, 29	syl131anc 1379	. . . . 5 ⊢ (𝜑 → (𝑉 ≤ (𝑄 ∨ 𝑇) → 𝑄 ≤ (𝑉 ∨ 𝑇)))
31	2, 17	4atexlemwb 37227	. . . . . . . . 9 ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐾))
32	8, 9, 10	latmle2 17670	. . . . . . . . 9 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾)) → ((𝑃 ∨ 𝑆) ∧ 𝑊) ≤ 𝑊)
33	3, 7, 31, 32	syl3anc 1367	. . . . . . . 8 ⊢ (𝜑 → ((𝑃 ∨ 𝑆) ∧ 𝑊) ≤ 𝑊)
34	19, 33	eqbrtrid 5087	. . . . . . 7 ⊢ (𝜑 → 𝑉 ≤ 𝑊)
35	2, 9, 4, 10, 5, 17, 18, 19	4atexlemtlw 37235	. . . . . . 7 ⊢ (𝜑 → 𝑇 ≤ 𝑊)
36	8, 5	atbase 36457	. . . . . . . . 9 ⊢ (𝑉 ∈ 𝐴 → 𝑉 ∈ (Base‘𝐾))
37	20, 36	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑉 ∈ (Base‘𝐾))
38	8, 5	atbase 36457	. . . . . . . . 9 ⊢ (𝑇 ∈ 𝐴 → 𝑇 ∈ (Base‘𝐾))
39	22, 38	syl 17	. . . . . . . 8 ⊢ (𝜑 → 𝑇 ∈ (Base‘𝐾))
40	8, 9, 4	latjle12 17655	. . . . . . . 8 ⊢ ((𝐾 ∈ Lat ∧ (𝑉 ∈ (Base‘𝐾) ∧ 𝑇 ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑉 ≤ 𝑊 ∧ 𝑇 ≤ 𝑊) ↔ (𝑉 ∨ 𝑇) ≤ 𝑊))
41	3, 37, 39, 31, 40	syl13anc 1368	. . . . . . 7 ⊢ (𝜑 → ((𝑉 ≤ 𝑊 ∧ 𝑇 ≤ 𝑊) ↔ (𝑉 ∨ 𝑇) ≤ 𝑊))
42	34, 35, 41	mpbi2and 710	. . . . . 6 ⊢ (𝜑 → (𝑉 ∨ 𝑇) ≤ 𝑊)
43	8, 5	atbase 36457	. . . . . . . 8 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ (Base‘𝐾))
44	21, 43	syl 17	. . . . . . 7 ⊢ (𝜑 → 𝑄 ∈ (Base‘𝐾))
45	2	4atexlemk 37215	. . . . . . . 8 ⊢ (𝜑 → 𝐾 ∈ HL)
46	8, 4, 5	hlatjcl 36535	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ 𝑉 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) → (𝑉 ∨ 𝑇) ∈ (Base‘𝐾))
47	45, 20, 22, 46	syl3anc 1367	. . . . . . 7 ⊢ (𝜑 → (𝑉 ∨ 𝑇) ∈ (Base‘𝐾))
48	8, 9	lattr 17649	. . . . . . 7 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∈ (Base‘𝐾) ∧ (𝑉 ∨ 𝑇) ∈ (Base‘𝐾) ∧ 𝑊 ∈ (Base‘𝐾))) → ((𝑄 ≤ (𝑉 ∨ 𝑇) ∧ (𝑉 ∨ 𝑇) ≤ 𝑊) → 𝑄 ≤ 𝑊))
49	3, 44, 47, 31, 48	syl13anc 1368	. . . . . 6 ⊢ (𝜑 → ((𝑄 ≤ (𝑉 ∨ 𝑇) ∧ (𝑉 ∨ 𝑇) ≤ 𝑊) → 𝑄 ≤ 𝑊))
50	42, 49	mpan2d 692	. . . . 5 ⊢ (𝜑 → (𝑄 ≤ (𝑉 ∨ 𝑇) → 𝑄 ≤ 𝑊))
51	30, 50	syld 47	. . . 4 ⊢ (𝜑 → (𝑉 ≤ (𝑄 ∨ 𝑇) → 𝑄 ≤ 𝑊))
52	15, 51	mtod 200	. . 3 ⊢ (𝜑 → ¬ 𝑉 ≤ (𝑄 ∨ 𝑇))
53		nbrne2 5072	. . 3 ⊢ ((𝐶 ≤ (𝑄 ∨ 𝑇) ∧ ¬ 𝑉 ≤ (𝑄 ∨ 𝑇)) → 𝐶 ≠ 𝑉)
54	13, 52, 53	syl2anc 586	. 2 ⊢ (𝜑 → 𝐶 ≠ 𝑉)
55	2	4atexlemw 37216	. . . 4 ⊢ (𝜑 → 𝑊 ∈ 𝐻)
56	45, 55	jca 514	. . 3 ⊢ (𝜑 → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻))
57	2	4atexlempw 37217	. . 3 ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊))
58	2	4atexlems 37220	. . 3 ⊢ (𝜑 → 𝑆 ∈ 𝐴)
59	2, 9, 4, 10, 5, 17, 18, 19, 1	4atexlemc 37237	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝐴)
60	2, 9, 4, 5	4atexlempns 37230	. . 3 ⊢ (𝜑 → 𝑃 ≠ 𝑆)
61	8, 9, 10	latmle2 17670	. . . . 5 ⊢ ((𝐾 ∈ Lat ∧ (𝑄 ∨ 𝑇) ∈ (Base‘𝐾) ∧ (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑃 ∨ 𝑆))
62	3, 6, 7, 61	syl3anc 1367	. . . 4 ⊢ (𝜑 → ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ≤ (𝑃 ∨ 𝑆))
63	1, 62	eqbrtrid 5087	. . 3 ⊢ (𝜑 → 𝐶 ≤ (𝑃 ∨ 𝑆))
64	9, 4, 10, 5, 17, 19	lhpat3 37214	. . 3 ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ 𝐶 ∈ 𝐴) ∧ (𝑃 ≠ 𝑆 ∧ 𝐶 ≤ (𝑃 ∨ 𝑆))) → (¬ 𝐶 ≤ 𝑊 ↔ 𝐶 ≠ 𝑉))
65	56, 57, 58, 59, 60, 63, 64	syl222anc 1382	. 2 ⊢ (𝜑 → (¬ 𝐶 ≤ 𝑊 ↔ 𝐶 ≠ 𝑉))
66	54, 65	mpbird 259	1 ⊢ (𝜑 → ¬ 𝐶 ≤ 𝑊)

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1083   = wceq 1537   ∈ wcel 2114   ≠ wne 3016   class class class wbr 5052  ‘cfv 6341  (class class class)co 7142  Basecbs 16466  lecple 16555  joincjn 17537  meetcmee 17538  Latclat 17638  Atomscatm 36431  CvLatclc 36433  HLchlt 36518  LHypclh 37152

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-rep 5176  ax-sep 5189  ax-nul 5196  ax-pow 5252  ax-pr 5316  ax-un 7447

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3488  df-sbc 3764  df-csb 3872  df-dif 3927  df-un 3929  df-in 3931  df-ss 3940  df-nul 4280  df-if 4454  df-pw 4527  df-sn 4554  df-pr 4556  df-op 4560  df-uni 4825  df-iun 4907  df-br 5053  df-opab 5115  df-mpt 5133  df-id 5446  df-xp 5547  df-rel 5548  df-cnv 5549  df-co 5550  df-dm 5551  df-rn 5552  df-res 5553  df-ima 5554  df-iota 6300  df-fun 6343  df-fn 6344  df-f 6345  df-f1 6346  df-fo 6347  df-f1o 6348  df-fv 6349  df-riota 7100  df-ov 7145  df-oprab 7146  df-proset 17521  df-poset 17539  df-plt 17551  df-lub 17567  df-glb 17568  df-join 17569  df-meet 17570  df-p0 17632  df-p1 17633  df-lat 17639  df-clat 17701  df-oposet 36344  df-ol 36346  df-oml 36347  df-covers 36434  df-ats 36435  df-atl 36466  df-cvlat 36490  df-hlat 36519  df-llines 36666  df-lplanes 36667  df-lhyp 37156

This theorem is referenced by:  4atexlemex2  37239  4atexlemcnd  37240