Theorem cvrat4 39889

Description: A condition implying existence of an atom with the properties shown. Lemma 3.2.20 in [PtakPulmannova] p. 68. Also Lemma 9.2(delta) in [MaedaMaeda] p. 41. (atcvat4i 32468 analog.) (Contributed by NM, 30-Nov-2011.)

Hypotheses

Ref	Expression
cvrat4.b	⊢ 𝐵 = (Base‘𝐾)
cvrat4.l	⊢ ≤ = (le‘𝐾)
cvrat4.j	⊢ ∨ = (join‘𝐾)
cvrat4.z	⊢ 0 = (0.‘𝐾)
cvrat4.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
cvrat4	⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))

Distinct variable groups:   𝐴,𝑟   𝐵,𝑟   ∨ ,𝑟   𝐾,𝑟   ≤ ,𝑟   𝑃,𝑟   𝑄,𝑟   𝑋,𝑟

Allowed substitution hint:   0 (𝑟)

Proof of Theorem cvrat4

Step	Hyp	Ref	Expression
1		hlatl 39806	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2	1	adantr 480	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ AtLat)
3		simpr1 1196	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑋 ∈ 𝐵)
4		cvrat4.b	. . . . . . . . . . 11 ⊢ 𝐵 = (Base‘𝐾)
5		cvrat4.l	. . . . . . . . . . 11 ⊢ ≤ = (le‘𝐾)
6		cvrat4.z	. . . . . . . . . . 11 ⊢ 0 = (0.‘𝐾)
7		cvrat4.a	. . . . . . . . . . 11 ⊢ 𝐴 = (Atoms‘𝐾)
8	4, 5, 6, 7	atlex 39762	. . . . . . . . . 10 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑟 ∈ 𝐴 𝑟 ≤ 𝑋)
9	8	3exp 1120	. . . . . . . . 9 ⊢ (𝐾 ∈ AtLat → (𝑋 ∈ 𝐵 → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟 ≤ 𝑋)))
10	2, 3, 9	sylc 65	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟 ≤ 𝑋))
11	10	adantr 480	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟 ≤ 𝑋))
12		simpll 767	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ HL)
13		simplr3 1219	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐴)
14		simpr 484	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
15		cvrat4.j	. . . . . . . . . . . . . . 15 ⊢ ∨ = (join‘𝐾)
16	5, 15, 7	hlatlej1 39821	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑟))
17	12, 13, 14, 16	syl3anc 1374	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑟))
18		breq1 5088	. . . . . . . . . . . . 13 ⊢ (𝑃 = 𝑄 → (𝑃 ≤ (𝑄 ∨ 𝑟) ↔ 𝑄 ≤ (𝑄 ∨ 𝑟)))
19	17, 18	imbitrrid 246	. . . . . . . . . . . 12 ⊢ (𝑃 = 𝑄 → (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝑃 ≤ (𝑄 ∨ 𝑟)))
20	19	expd 415	. . . . . . . . . . 11 ⊢ (𝑃 = 𝑄 → ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑟 ∈ 𝐴 → 𝑃 ≤ (𝑄 ∨ 𝑟))))
21	20	impcom 407	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (𝑟 ∈ 𝐴 → 𝑃 ≤ (𝑄 ∨ 𝑟)))
22	21	anim2d 613	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → ((𝑟 ≤ 𝑋 ∧ 𝑟 ∈ 𝐴) → (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))
23	22	expcomd 416	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (𝑟 ∈ 𝐴 → (𝑟 ≤ 𝑋 → (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
24	23	reximdvai 3148	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (∃𝑟 ∈ 𝐴 𝑟 ≤ 𝑋 → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))
25	11, 24	syld 47	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))
26	25	ex 412	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 = 𝑄 → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
27	26	a1i 11	. . . 4 ⊢ (𝑃 ≤ (𝑋 ∨ 𝑄) → ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 = 𝑄 → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))))
28	27	com4l 92	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 = 𝑄 → (𝑋 ≠ 0 → (𝑃 ≤ (𝑋 ∨ 𝑄) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))))
29	28	imp4a 422	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 = 𝑄 → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
30		hllat 39809	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
31	30	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ Lat)
32		simpr3 1198	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑄 ∈ 𝐴)
33	4, 7	atbase 39735	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵)
34	32, 33	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑄 ∈ 𝐵)
35	4, 5, 15	latleeqj2 18418	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑄 ≤ 𝑋 ↔ (𝑋 ∨ 𝑄) = 𝑋))
36	31, 34, 3, 35	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄 ≤ 𝑋 ↔ (𝑋 ∨ 𝑄) = 𝑋))
37	36	biimpa 476	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) → (𝑋 ∨ 𝑄) = 𝑋)
38	37	breq2d 5097	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ 𝑃 ≤ 𝑋))
39	38	biimpa 476	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → 𝑃 ≤ 𝑋)
40	39	expl 457	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑄 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → 𝑃 ≤ 𝑋))
41		simpl 482	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ HL)
42		simpr2 1197	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑃 ∈ 𝐴)
43	5, 15, 7	hlatlej2 39822	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → 𝑃 ≤ (𝑄 ∨ 𝑃))
44	41, 32, 42, 43	syl3anc 1374	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑃 ≤ (𝑄 ∨ 𝑃))
45	40, 44	jctird 526	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑄 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑃))))
46	45, 42	jctild 525	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑄 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → (𝑃 ∈ 𝐴 ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑃)))))
47	46	impl 455	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → (𝑃 ∈ 𝐴 ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑃))))
48		breq1 5088	. . . . . . 7 ⊢ (𝑟 = 𝑃 → (𝑟 ≤ 𝑋 ↔ 𝑃 ≤ 𝑋))
49		oveq2 7375	. . . . . . . 8 ⊢ (𝑟 = 𝑃 → (𝑄 ∨ 𝑟) = (𝑄 ∨ 𝑃))
50	49	breq2d 5097	. . . . . . 7 ⊢ (𝑟 = 𝑃 → (𝑃 ≤ (𝑄 ∨ 𝑟) ↔ 𝑃 ≤ (𝑄 ∨ 𝑃)))
51	48, 50	anbi12d 633	. . . . . 6 ⊢ (𝑟 = 𝑃 → ((𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)) ↔ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑃))))
52	51	rspcev 3564	. . . . 5 ⊢ ((𝑃 ∈ 𝐴 ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑃))) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))
53	47, 52	syl 17	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))
54	53	adantrl 717	. . 3 ⊢ ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) ∧ (𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))
55	54	exp31 419	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄 ≤ 𝑋 → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
56		simpr 484	. . 3 ⊢ ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → 𝑃 ≤ (𝑋 ∨ 𝑄))
57		ioran 986	. . . . 5 ⊢ (¬ (𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋) ↔ (¬ 𝑃 = 𝑄 ∧ ¬ 𝑄 ≤ 𝑋))
58		df-ne 2933	. . . . . 6 ⊢ (𝑃 ≠ 𝑄 ↔ ¬ 𝑃 = 𝑄)
59	58	anbi1i 625	. . . . 5 ⊢ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ↔ (¬ 𝑃 = 𝑄 ∧ ¬ 𝑄 ≤ 𝑋))
60	57, 59	bitr4i 278	. . . 4 ⊢ (¬ (𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋) ↔ (𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋))
61		eqid 2736	. . . . . . . . . 10 ⊢ (meet‘𝐾) = (meet‘𝐾)
62	4, 5, 15, 61, 7	cvrat3 39888	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴))
63	62	3expd 1355	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 ≠ 𝑄 → (¬ 𝑄 ≤ 𝑋 → (𝑃 ≤ (𝑋 ∨ 𝑄) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴))))
64	63	imp4c 423	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴))
65	4, 7	atbase 39735	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
66	42, 65	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑃 ∈ 𝐵)
67	4, 15	latjcl 18405	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → (𝑃 ∨ 𝑄) ∈ 𝐵)
68	31, 66, 34, 67	syl3anc 1374	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 ∨ 𝑄) ∈ 𝐵)
69	4, 5, 61	latmle1 18430	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋)
70	31, 3, 68, 69	syl3anc 1374	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋)
71	70	adantr 480	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋)
72		simpll 767	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → 𝐾 ∈ HL)
73	63	imp44 428	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴)
74		simplr2 1218	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → 𝑃 ∈ 𝐴)
75	34	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → 𝑄 ∈ 𝐵)
76	73, 74, 75	3jca 1129	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵))
77	72, 76	jca 511	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → (𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)))
78	4, 5, 61, 6, 7	atnle 39763	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (¬ 𝑄 ≤ 𝑋 ↔ (𝑄(meet‘𝐾)𝑋) = 0 ))
79	2, 32, 3, 78	syl3anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (¬ 𝑄 ≤ 𝑋 ↔ (𝑄(meet‘𝐾)𝑋) = 0 ))
80	4, 61	latmcom 18429	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑄(meet‘𝐾)𝑋) = (𝑋(meet‘𝐾)𝑄))
81	31, 34, 3, 80	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄(meet‘𝐾)𝑋) = (𝑋(meet‘𝐾)𝑄))
82	81	eqeq1d 2738	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑄(meet‘𝐾)𝑋) = 0 ↔ (𝑋(meet‘𝐾)𝑄) = 0 ))
83	79, 82	bitrd 279	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (¬ 𝑄 ≤ 𝑋 ↔ (𝑋(meet‘𝐾)𝑄) = 0 ))
84	4, 61	latmcl 18406	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵)
85	31, 3, 68, 84	syl3anc 1374	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵)
86	85, 3, 34	3jca 1129	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵))
87	31, 86	jca 511	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝐾 ∈ Lat ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵)))
88	4, 5, 61	latmlem2 18436	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵)) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ (𝑄(meet‘𝐾)𝑋)))
89	87, 70, 88	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ (𝑄(meet‘𝐾)𝑋))
90	89, 81	breqtrd 5111	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ (𝑋(meet‘𝐾)𝑄))
91		breq2 5089	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋(meet‘𝐾)𝑄) = 0 → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ (𝑋(meet‘𝐾)𝑄) ↔ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ 0 ))
92	90, 91	syl5ibcom 245	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋(meet‘𝐾)𝑄) = 0 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ 0 ))
93		hlop 39808	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
94	93	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ OP)
95	4, 61	latmcl 18406	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ∈ 𝐵)
96	31, 34, 85, 95	syl3anc 1374	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ∈ 𝐵)
97	4, 5, 6	ople0 39633	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ OP ∧ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ∈ 𝐵) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ 0 ↔ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 ))
98	94, 96, 97	syl2anc 585	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ 0 ↔ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 ))
99	92, 98	sylibd 239	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋(meet‘𝐾)𝑄) = 0 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 ))
100	83, 99	sylbid 240	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (¬ 𝑄 ≤ 𝑋 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 ))
101	100	imp 406	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ¬ 𝑄 ≤ 𝑋) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 )
102	101	adantrl 717	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 )
103	102	adantrr 718	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 )
104	4, 5, 61	latmle2 18431	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑃 ∨ 𝑄))
105	31, 3, 68, 104	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑃 ∨ 𝑄))
106	4, 15	latjcom 18413	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
107	31, 66, 34, 106	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
108	105, 107	breqtrd 5111	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑄 ∨ 𝑃))
109	108	adantr 480	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑄 ∨ 𝑃))
110	30	adantr 480	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → 𝐾 ∈ Lat)
111		simpr3 1198	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → 𝑄 ∈ 𝐵)
112		simpr1 1196	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴)
113	4, 7	atbase 39735	. . . . . . . . . . . . . 14 ⊢ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵)
114	112, 113	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵)
115	4, 61	latmcom 18429	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))(meet‘𝐾)𝑄))
116	110, 111, 114, 115	syl3anc 1374	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))(meet‘𝐾)𝑄))
117	116	eqeq1d 2738	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 ↔ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))(meet‘𝐾)𝑄) = 0 ))
118	4, 5, 15, 61, 6, 7	hlexch3 39837	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵) ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))(meet‘𝐾)𝑄) = 0 ) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑄 ∨ 𝑃) → 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)))))
119	118	3expia 1122	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → (((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))(meet‘𝐾)𝑄) = 0 → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑄 ∨ 𝑃) → 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))))
120	117, 119	sylbid 240	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑄 ∨ 𝑃) → 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))))
121	77, 103, 109, 120	syl3c 66	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))
122	71, 121	jca 511	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)))))
123	122	ex 412	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))))
124	64, 123	jcad 512	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)))))))
125		breq1 5088	. . . . . . . 8 ⊢ (𝑟 = (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) → (𝑟 ≤ 𝑋 ↔ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋))
126		oveq2 7375	. . . . . . . . 9 ⊢ (𝑟 = (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) → (𝑄 ∨ 𝑟) = (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))
127	126	breq2d 5097	. . . . . . . 8 ⊢ (𝑟 = (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) → (𝑃 ≤ (𝑄 ∨ 𝑟) ↔ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)))))
128	125, 127	anbi12d 633	. . . . . . 7 ⊢ (𝑟 = (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) → ((𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)) ↔ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))))
129	128	rspcev 3564	. . . . . 6 ⊢ (((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))
130	124, 129	syl6 35	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))
131	130	expd 415	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
132	60, 131	biimtrid 242	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (¬ (𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
133	56, 132	syl7 74	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (¬ (𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋) → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
134	29, 55, 133	ecase3d 1035	1 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 848   ∧ w3a 1087   = wceq 1542   ∈ wcel 2114   ≠ wne 2932  ∃wrex 3061   class class class wbr 5085  ‘cfv 6498  (class class class)co 7367  Basecbs 17179  lecple 17227  joincjn 18277  meetcmee 18278  0.cp0 18387  Latclat 18397  OPcops 39618  Atomscatm 39709  AtLatcal 39710  HLchlt 39796

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708  ax-rep 5212  ax-sep 5231  ax-nul 5241  ax-pow 5307  ax-pr 5375  ax-un 7689

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2539  df-eu 2569  df-clab 2715  df-cleq 2728  df-clel 2811  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3062  df-rmo 3342  df-reu 3343  df-rab 3390  df-v 3431  df-sbc 3729  df-csb 3838  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-pw 4543  df-sn 4568  df-pr 4570  df-op 4574  df-uni 4851  df-iun 4935  df-br 5086  df-opab 5148  df-mpt 5167  df-id 5526  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-iota 6454  df-fun 6500  df-fn 6501  df-f 6502  df-f1 6503  df-fo 6504  df-f1o 6505  df-fv 6506  df-riota 7324  df-ov 7370  df-oprab 7371  df-proset 18260  df-poset 18279  df-plt 18294  df-lub 18310  df-glb 18311  df-join 18312  df-meet 18313  df-p0 18389  df-lat 18398  df-clat 18465  df-oposet 39622  df-ol 39624  df-oml 39625  df-covers 39712  df-ats 39713  df-atl 39744  df-cvlat 39768  df-hlat 39797

This theorem is referenced by:  cvrat42  39890  ps-2  39924