Theorem cvrat4 37457

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 30759 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 37374	. . . . . . . . . 10 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2	1	adantr 481	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ AtLat)
3		simpr1 1193	. . . . . . . . 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 37330	. . . . . . . . . 10 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑟 ∈ 𝐴 𝑟 ≤ 𝑋)
9	8	3exp 1118	. . . . . . . . 9 ⊢ (𝐾 ∈ AtLat → (𝑋 ∈ 𝐵 → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟 ≤ 𝑋)))
10	2, 3, 9	sylc 65	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟 ≤ 𝑋))
11	10	adantr 481	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟 ≤ 𝑋))
12		simpll 764	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ HL)
13		simplr3 1216	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐴)
14		simpr 485	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
15		cvrat4.j	. . . . . . . . . . . . . . 15 ⊢ ∨ = (join‘𝐾)
16	5, 15, 7	hlatlej1 37389	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑟))
17	12, 13, 14, 16	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝑄 ≤ (𝑄 ∨ 𝑟))
18		breq1 5077	. . . . . . . . . . . . 13 ⊢ (𝑃 = 𝑄 → (𝑃 ≤ (𝑄 ∨ 𝑟) ↔ 𝑄 ≤ (𝑄 ∨ 𝑟)))
19	17, 18	syl5ibr 245	. . . . . . . . . . . 12 ⊢ (𝑃 = 𝑄 → (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → 𝑃 ≤ (𝑄 ∨ 𝑟)))
20	19	expd 416	. . . . . . . . . . 11 ⊢ (𝑃 = 𝑄 → ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑟 ∈ 𝐴 → 𝑃 ≤ (𝑄 ∨ 𝑟))))
21	20	impcom 408	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (𝑟 ∈ 𝐴 → 𝑃 ≤ (𝑄 ∨ 𝑟)))
22	21	anim2d 612	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → ((𝑟 ≤ 𝑋 ∧ 𝑟 ∈ 𝐴) → (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))
23	22	expcomd 417	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (𝑟 ∈ 𝐴 → (𝑟 ≤ 𝑋 → (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
24	23	reximdvai 3200	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (∃𝑟 ∈ 𝐴 𝑟 ≤ 𝑋 → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))
25	11, 24	syld 47	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑃 = 𝑄) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))
26	25	ex 413	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 = 𝑄 → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
27	26	a1i 11	. . . 4 ⊢ (𝑃 ≤ (𝑋 ∨ 𝑄) → ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 = 𝑄 → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))))
28	27	com4l 92	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 = 𝑄 → (𝑋 ≠ 0 → (𝑃 ≤ (𝑋 ∨ 𝑄) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))))
29	28	imp4a 423	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 = 𝑄 → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
30		hllat 37377	. . . . . . . . . . . . . 14 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
31	30	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ Lat)
32		simpr3 1195	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑄 ∈ 𝐴)
33	4, 7	atbase 37303	. . . . . . . . . . . . . 14 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵)
34	32, 33	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑄 ∈ 𝐵)
35	4, 5, 15	latleeqj2 18170	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑄 ≤ 𝑋 ↔ (𝑋 ∨ 𝑄) = 𝑋))
36	31, 34, 3, 35	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄 ≤ 𝑋 ↔ (𝑋 ∨ 𝑄) = 𝑋))
37	36	biimpa 477	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) → (𝑋 ∨ 𝑄) = 𝑋)
38	37	breq2d 5086	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ 𝑃 ≤ 𝑋))
39	38	biimpa 477	. . . . . . . . 9 ⊢ ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → 𝑃 ≤ 𝑋)
40	39	expl 458	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑄 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → 𝑃 ≤ 𝑋))
41		simpl 483	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ HL)
42		simpr2 1194	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑃 ∈ 𝐴)
43	5, 15, 7	hlatlej2 37390	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → 𝑃 ≤ (𝑄 ∨ 𝑃))
44	41, 32, 42, 43	syl3anc 1370	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑃 ≤ (𝑄 ∨ 𝑃))
45	40, 44	jctird 527	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑄 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑃))))
46	45, 42	jctild 526	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑄 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → (𝑃 ∈ 𝐴 ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑃)))))
47	46	impl 456	. . . . 5 ⊢ ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → (𝑃 ∈ 𝐴 ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑃))))
48		breq1 5077	. . . . . . 7 ⊢ (𝑟 = 𝑃 → (𝑟 ≤ 𝑋 ↔ 𝑃 ≤ 𝑋))
49		oveq2 7283	. . . . . . . 8 ⊢ (𝑟 = 𝑃 → (𝑄 ∨ 𝑟) = (𝑄 ∨ 𝑃))
50	49	breq2d 5086	. . . . . . 7 ⊢ (𝑟 = 𝑃 → (𝑃 ≤ (𝑄 ∨ 𝑟) ↔ 𝑃 ≤ (𝑄 ∨ 𝑃)))
51	48, 50	anbi12d 631	. . . . . 6 ⊢ (𝑟 = 𝑃 → ((𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)) ↔ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑃))))
52	51	rspcev 3561	. . . . 5 ⊢ ((𝑃 ∈ 𝐴 ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑃))) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))
53	47, 52	syl 17	. . . 4 ⊢ ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))
54	53	adantrl 713	. . 3 ⊢ ((((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑄 ≤ 𝑋) ∧ (𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))
55	54	exp31 420	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄 ≤ 𝑋 → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
56		simpr 485	. . 3 ⊢ ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → 𝑃 ≤ (𝑋 ∨ 𝑄))
57		ioran 981	. . . . 5 ⊢ (¬ (𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋) ↔ (¬ 𝑃 = 𝑄 ∧ ¬ 𝑄 ≤ 𝑋))
58		df-ne 2944	. . . . . 6 ⊢ (𝑃 ≠ 𝑄 ↔ ¬ 𝑃 = 𝑄)
59	58	anbi1i 624	. . . . 5 ⊢ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ↔ (¬ 𝑃 = 𝑄 ∧ ¬ 𝑄 ≤ 𝑋))
60	57, 59	bitr4i 277	. . . 4 ⊢ (¬ (𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋) ↔ (𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋))
61		eqid 2738	. . . . . . . . . 10 ⊢ (meet‘𝐾) = (meet‘𝐾)
62	4, 5, 15, 61, 7	cvrat3 37456	. . . . . . . . 9 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴))
63	62	3expd 1352	. . . . . . . 8 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 ≠ 𝑄 → (¬ 𝑄 ≤ 𝑋 → (𝑃 ≤ (𝑋 ∨ 𝑄) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴))))
64	63	imp4c 424	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴))
65	4, 7	atbase 37303	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
66	42, 65	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑃 ∈ 𝐵)
67	4, 15	latjcl 18157	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → (𝑃 ∨ 𝑄) ∈ 𝐵)
68	31, 66, 34, 67	syl3anc 1370	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 ∨ 𝑄) ∈ 𝐵)
69	4, 5, 61	latmle1 18182	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋)
70	31, 3, 68, 69	syl3anc 1370	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋)
71	70	adantr 481	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋)
72		simpll 764	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → 𝐾 ∈ HL)
73	63	imp44 429	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴)
74		simplr2 1215	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → 𝑃 ∈ 𝐴)
75	34	adantr 481	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → 𝑄 ∈ 𝐵)
76	73, 74, 75	3jca 1127	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵))
77	72, 76	jca 512	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → (𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)))
78	4, 5, 61, 6, 7	atnle 37331	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ AtLat ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (¬ 𝑄 ≤ 𝑋 ↔ (𝑄(meet‘𝐾)𝑋) = 0 ))
79	2, 32, 3, 78	syl3anc 1370	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (¬ 𝑄 ≤ 𝑋 ↔ (𝑄(meet‘𝐾)𝑋) = 0 ))
80	4, 61	latmcom 18181	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) → (𝑄(meet‘𝐾)𝑋) = (𝑋(meet‘𝐾)𝑄))
81	31, 34, 3, 80	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄(meet‘𝐾)𝑋) = (𝑋(meet‘𝐾)𝑄))
82	81	eqeq1d 2740	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑄(meet‘𝐾)𝑋) = 0 ↔ (𝑋(meet‘𝐾)𝑄) = 0 ))
83	79, 82	bitrd 278	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (¬ 𝑄 ≤ 𝑋 ↔ (𝑋(meet‘𝐾)𝑄) = 0 ))
84	4, 61	latmcl 18158	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵)
85	31, 3, 68, 84	syl3anc 1370	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵)
86	85, 3, 34	3jca 1127	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵))
87	31, 86	jca 512	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝐾 ∈ Lat ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵)))
88	4, 5, 61	latmlem2 18188	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵)) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ (𝑄(meet‘𝐾)𝑋)))
89	87, 70, 88	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ (𝑄(meet‘𝐾)𝑋))
90	89, 81	breqtrd 5100	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ (𝑋(meet‘𝐾)𝑄))
91		breq2 5078	. . . . . . . . . . . . . . . 16 ⊢ ((𝑋(meet‘𝐾)𝑄) = 0 → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ (𝑋(meet‘𝐾)𝑄) ↔ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ 0 ))
92	90, 91	syl5ibcom 244	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋(meet‘𝐾)𝑄) = 0 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ 0 ))
93		hlop 37376	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ HL → 𝐾 ∈ OP)
94	93	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ OP)
95	4, 61	latmcl 18158	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ∈ 𝐵)
96	31, 34, 85, 95	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ∈ 𝐵)
97	4, 5, 6	ople0 37201	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ OP ∧ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ∈ 𝐵) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ 0 ↔ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 ))
98	94, 96, 97	syl2anc 584	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) ≤ 0 ↔ (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 ))
99	92, 98	sylibd 238	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋(meet‘𝐾)𝑄) = 0 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 ))
100	83, 99	sylbid 239	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (¬ 𝑄 ≤ 𝑋 → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 ))
101	100	imp 407	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ¬ 𝑄 ≤ 𝑋) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 )
102	101	adantrl 713	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 )
103	102	adantrr 714	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 )
104	4, 5, 61	latmle2 18183	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑃 ∨ 𝑄))
105	31, 3, 68, 104	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑃 ∨ 𝑄))
106	4, 15	latjcom 18165	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
107	31, 66, 34, 106	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑃))
108	105, 107	breqtrd 5100	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑄 ∨ 𝑃))
109	108	adantr 481	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑄 ∨ 𝑃))
110	30	adantr 481	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → 𝐾 ∈ Lat)
111		simpr3 1195	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → 𝑄 ∈ 𝐵)
112		simpr1 1193	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴)
113	4, 7	atbase 37303	. . . . . . . . . . . . . 14 ⊢ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵)
114	112, 113	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵)
115	4, 61	latmcom 18181	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ 𝑄 ∈ 𝐵 ∧ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐵) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))(meet‘𝐾)𝑄))
116	110, 111, 114, 115	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → (𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))(meet‘𝐾)𝑄))
117	116	eqeq1d 2740	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 ↔ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))(meet‘𝐾)𝑄) = 0 ))
118	4, 5, 15, 61, 6, 7	hlexch3 37405	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵) ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))(meet‘𝐾)𝑄) = 0 ) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑄 ∨ 𝑃) → 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)))))
119	118	3expia 1120	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → (((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))(meet‘𝐾)𝑄) = 0 → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑄 ∨ 𝑃) → 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))))
120	117, 119	sylbid 239	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐵)) → ((𝑄(meet‘𝐾)(𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))) = 0 → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ (𝑄 ∨ 𝑃) → 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))))
121	77, 103, 109, 120	syl3c 66	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))
122	71, 121	jca 512	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄))) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)))))
123	122	ex 413	. . . . . . 7 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))))
124	64, 123	jcad 513	. . . . . 6 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)))))))
125		breq1 5077	. . . . . . . 8 ⊢ (𝑟 = (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) → (𝑟 ≤ 𝑋 ↔ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋))
126		oveq2 7283	. . . . . . . . 9 ⊢ (𝑟 = (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) → (𝑄 ∨ 𝑟) = (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))
127	126	breq2d 5086	. . . . . . . 8 ⊢ (𝑟 = (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) → (𝑃 ≤ (𝑄 ∨ 𝑟) ↔ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)))))
128	125, 127	anbi12d 631	. . . . . . 7 ⊢ (𝑟 = (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) → ((𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)) ↔ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))))
129	128	rspcev 3561	. . . . . 6 ⊢ (((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ∈ 𝐴 ∧ ((𝑋(meet‘𝐾)(𝑃 ∨ 𝑄)) ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ (𝑋(meet‘𝐾)(𝑃 ∨ 𝑄))))) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))
130	124, 129	syl6 35	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))
131	130	expd 416	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
132	60, 131	syl5bi 241	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (¬ (𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
133	56, 132	syl7 74	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (¬ (𝑃 = 𝑄 ∨ 𝑄 ≤ 𝑋) → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))))
134	29, 55, 133	ecase3d 1031	1 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 396   ∨ wo 844   ∧ w3a 1086   = wceq 1539   ∈ wcel 2106   ≠ wne 2943  ∃wrex 3065   class class class wbr 5074  ‘cfv 6433  (class class class)co 7275  Basecbs 16912  lecple 16969  joincjn 18029  meetcmee 18030  0.cp0 18141  Latclat 18149  OPcops 37186  Atomscatm 37277  AtLatcal 37278  HLchlt 37364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-rep 5209  ax-sep 5223  ax-nul 5230  ax-pow 5288  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-riota 7232  df-ov 7278  df-oprab 7279  df-proset 18013  df-poset 18031  df-plt 18048  df-lub 18064  df-glb 18065  df-join 18066  df-meet 18067  df-p0 18143  df-lat 18150  df-clat 18217  df-oposet 37190  df-ol 37192  df-oml 37193  df-covers 37280  df-ats 37281  df-atl 37312  df-cvlat 37336  df-hlat 37365

This theorem is referenced by:  cvrat42  37458  ps-2  37492