Theorem 4atexlemtlw

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

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

Proof

Step	Hyp	Ref	Expression
1		4thatlem.ph	⊢ ( 𝜑 ↔ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊 ) ∧ ( 𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ) ) ∧ ( 𝑆 ∈ 𝐴 ∧ ( 𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ ( 𝑃 ∨ 𝑅 ) = ( 𝑄 ∨ 𝑅 ) ) ∧ ( 𝑇 ∈ 𝐴 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) ∧ ( 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ ( 𝑃 ∨ 𝑄 ) ) ) )
2		4thatlem0.l	⊢ ≤ = ( le ‘ 𝐾 )
3		4thatlem0.j	⊢ ∨ = ( join ‘ 𝐾 )
4		4thatlem0.m	⊢ ∧ = ( meet ‘ 𝐾 )
5		4thatlem0.a	⊢ 𝐴 = ( Atoms ‘ 𝐾 )
6		4thatlem0.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
7		4thatlem0.u	⊢ 𝑈 = ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 )
8		4thatlem0.v	⊢ 𝑉 = ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 )
9		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
10	1	4atexlemkl	⊢ ( 𝜑 → 𝐾 ∈ Lat )
11	1	4atexlemt	⊢ ( 𝜑 → 𝑇 ∈ 𝐴 )
12	9 5	atbase	⊢ ( 𝑇 ∈ 𝐴 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
13	11 12	syl	⊢ ( 𝜑 → 𝑇 ∈ ( Base ‘ 𝐾 ) )
14	1	4atexlemk	⊢ ( 𝜑 → 𝐾 ∈ HL )
15	1 2 3 4 5 6 7	4atexlemu	⊢ ( 𝜑 → 𝑈 ∈ 𝐴 )
16	1 2 3 4 5 6 7 8	4atexlemv	⊢ ( 𝜑 → 𝑉 ∈ 𝐴 )
17	9 3 5	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ) → ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
18	14 15 16 17	syl3anc	⊢ ( 𝜑 → ( 𝑈 ∨ 𝑉 ) ∈ ( Base ‘ 𝐾 ) )
19	1 6	4atexlemwb	⊢ ( 𝜑 → 𝑊 ∈ ( Base ‘ 𝐾 ) )
20	1	4atexlemkc	⊢ ( 𝜑 → 𝐾 ∈ CvLat )
21	1 2 3 4 5 6 7 8	4atexlemunv	⊢ ( 𝜑 → 𝑈 ≠ 𝑉 )
22	1	4atexlemutvt	⊢ ( 𝜑 → ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) )
23	5 2 3	cvlsupr4	⊢ ( ( 𝐾 ∈ CvLat ∧ ( 𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ) ∧ ( 𝑈 ≠ 𝑉 ∧ ( 𝑈 ∨ 𝑇 ) = ( 𝑉 ∨ 𝑇 ) ) ) → 𝑇 ≤ ( 𝑈 ∨ 𝑉 ) )
24	20 15 16 11 21 22 23	syl132anc	⊢ ( 𝜑 → 𝑇 ≤ ( 𝑈 ∨ 𝑉 ) )
25	1	4atexlemp	⊢ ( 𝜑 → 𝑃 ∈ 𝐴 )
26	1	4atexlemq	⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
27	9 3 5	hlatjcl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ) → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
28	14 25 26 27	syl3anc	⊢ ( 𝜑 → ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) )
29	9 2 4	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑄 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
30	10 28 19 29	syl3anc	⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑄 ) ∧ 𝑊 ) ≤ 𝑊 )
31	7 30	eqbrtrid	⊢ ( 𝜑 → 𝑈 ≤ 𝑊 )
32	1 3 5	4atexlempsb	⊢ ( 𝜑 → ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
33	9 2 4	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑃 ∨ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ≤ 𝑊 )
34	10 32 19 33	syl3anc	⊢ ( 𝜑 → ( ( 𝑃 ∨ 𝑆 ) ∧ 𝑊 ) ≤ 𝑊 )
35	8 34	eqbrtrid	⊢ ( 𝜑 → 𝑉 ≤ 𝑊 )
36	9 5	atbase	⊢ ( 𝑈 ∈ 𝐴 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
37	15 36	syl	⊢ ( 𝜑 → 𝑈 ∈ ( Base ‘ 𝐾 ) )
38	9 5	atbase	⊢ ( 𝑉 ∈ 𝐴 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
39	16 38	syl	⊢ ( 𝜑 → 𝑉 ∈ ( Base ‘ 𝐾 ) )
40	9 2 3	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑈 ∈ ( Base ‘ 𝐾 ) ∧ 𝑉 ∈ ( Base ‘ 𝐾 ) ∧ 𝑊 ∈ ( Base ‘ 𝐾 ) ) ) → ( ( 𝑈 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊 ) ↔ ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 ) )
41	10 37 39 19 40	syl13anc	⊢ ( 𝜑 → ( ( 𝑈 ≤ 𝑊 ∧ 𝑉 ≤ 𝑊 ) ↔ ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 ) )
42	31 35 41	mpbi2and	⊢ ( 𝜑 → ( 𝑈 ∨ 𝑉 ) ≤ 𝑊 )
43	9 2 10 13 18 19 24 42	lattrd	⊢ ( 𝜑 → 𝑇 ≤ 𝑊 )