Theorem cvratlem 38889

Description: Lemma for cvrat 38890. (atcvatlem 32189 analog.) (Contributed by NM, 22-Nov-2011.)

Hypotheses

Ref	Expression
cvrat.b	⊢ 𝐵 = (Base‘𝐾)
cvrat.s	⊢ < = (lt‘𝐾)
cvrat.j	⊢ ∨ = (join‘𝐾)
cvrat.z	⊢ 0 = (0.‘𝐾)
cvrat.a	⊢ 𝐴 = (Atoms‘𝐾)

Assertion

Ref	Expression
cvratlem	⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ (𝑋 ≠ 0 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))

Proof of Theorem cvratlem

Dummy variable 𝑟 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hlatl 38827	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2	1	adantr 480	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ AtLat)
3		simpr1 1192	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑋 ∈ 𝐵)
4		cvrat.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
5		eqid 2728	. . . . . 6 ⊢ (le‘𝐾) = (le‘𝐾)
6		cvrat.z	. . . . . 6 ⊢ 0 = (0.‘𝐾)
7		cvrat.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
8	4, 5, 6, 7	atlex 38783	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋)
9	8	3expia 1119	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋))
10	2, 3, 9	syl2anc 583	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋))
11	1	3ad2ant1 1131	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ AtLat)
12		simp22 1205	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃 ∈ 𝐴)
13		simp3 1136	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
14	5, 7	atcmp 38778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 ↔ 𝑃 = 𝑟))
15	11, 12, 13, 14	syl3anc 1369	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 ↔ 𝑃 = 𝑟))
16		breq1 5146	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 = 𝑟 → (𝑃(le‘𝐾)𝑋 ↔ 𝑟(le‘𝐾)𝑋))
17	16	biimprd 247	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 = 𝑟 → (𝑟(le‘𝐾)𝑋 → 𝑃(le‘𝐾)𝑋))
18	15, 17	syl6bi 253	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 → (𝑟(le‘𝐾)𝑋 → 𝑃(le‘𝐾)𝑋)))
19	18	com23 86	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑃(le‘𝐾)𝑟 → 𝑃(le‘𝐾)𝑋)))
20		con3 153	. . . . . . . . . . . . . 14 ⊢ ((𝑃(le‘𝐾)𝑟 → 𝑃(le‘𝐾)𝑋) → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑃(le‘𝐾)𝑟))
21	19, 20	syl6 35	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑃(le‘𝐾)𝑟)))
22	21	impd 410	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋) → ¬ 𝑃(le‘𝐾)𝑟))
23		simp1 1134	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ HL)
24	4, 7	atbase 38756	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵)
25	24	3ad2ant3 1133	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐵)
26		cvrat.j	. . . . . . . . . . . . . 14 ⊢ ∨ = (join‘𝐾)
27		eqid 2728	. . . . . . . . . . . . . 14 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
28	4, 5, 26, 27, 7	cvr1 38878	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃(le‘𝐾)𝑟 ↔ 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
29	23, 25, 12, 28	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (¬ 𝑃(le‘𝐾)𝑟 ↔ 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
30	22, 29	sylibd 238	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋) → 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
31	30	imp 406	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃))
32		hllat 38830	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
33	32	3ad2ant1 1131	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ Lat)
34	4, 7	atbase 38756	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
35	12, 34	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃 ∈ 𝐵)
36	4, 26	latjcom 18433	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
37	33, 35, 25, 36	syl3anc 1369	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
38	37	adantr 480	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
39	31, 38	breqtrrd 5171	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟))
40	39	adantrrl 723	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟))
41	5, 26, 7	hlatlej1 38842	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
42	23, 12, 13, 41	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
43	42	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
44	5, 7	atcmp 38778	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ AtLat ∧ 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃))
45	11, 13, 12, 44	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃))
46		breq1 5146	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑃 → (𝑟(le‘𝐾)𝑋 ↔ 𝑃(le‘𝐾)𝑋))
47	46	biimpd 228	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑃 → (𝑟(le‘𝐾)𝑋 → 𝑃(le‘𝐾)𝑋))
48	45, 47	syl6bi 253	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 → (𝑟(le‘𝐾)𝑋 → 𝑃(le‘𝐾)𝑋)))
49	48	com23 86	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑟(le‘𝐾)𝑃 → 𝑃(le‘𝐾)𝑋)))
50		con3 153	. . . . . . . . . . . . . . 15 ⊢ ((𝑟(le‘𝐾)𝑃 → 𝑃(le‘𝐾)𝑋) → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑟(le‘𝐾)𝑃))
51	49, 50	syl6 35	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑟(le‘𝐾)𝑃)))
52	51	imp32 418	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → ¬ 𝑟(le‘𝐾)𝑃)
53	52	adantrrl 723	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ¬ 𝑟(le‘𝐾)𝑃)
54		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → 𝑟(le‘𝐾)𝑋)
55		simp21 1204	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑋 ∈ 𝐵)
56		simp23 1206	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐴)
57	4, 7	atbase 38756	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵)
58	56, 57	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐵)
59	4, 26	latjcl 18425	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → (𝑃 ∨ 𝑄) ∈ 𝐵)
60	33, 35, 58, 59	syl3anc 1369	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ 𝐵)
61	23, 55, 60	3jca 1126	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵))
62		cvrat.s	. . . . . . . . . . . . . . . . . 18 ⊢ < = (lt‘𝐾)
63	5, 62	pltle 18319	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑋 < (𝑃 ∨ 𝑄) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)))
64	63	imp 406	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) ∧ 𝑋 < (𝑃 ∨ 𝑄)) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
65	61, 64	sylan 579	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ 𝑋 < (𝑃 ∨ 𝑄)) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
66	65	adantrl 715	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
67		hlpos 38833	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
68	67	3ad2ant1 1131	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ Poset)
69	4, 5	postr 18306	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
70	68, 25, 55, 60, 69	syl13anc 1370	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
71	70	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
72	54, 66, 71	mp2and 698	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄))
73	72	adantrrr 724	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄))
74	4, 5, 26, 7	hlexch1 38850	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵) ∧ ¬ 𝑟(le‘𝐾)𝑃) → (𝑟(le‘𝐾)(𝑃 ∨ 𝑄) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
75	74	3expia 1119	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵)) → (¬ 𝑟(le‘𝐾)𝑃 → (𝑟(le‘𝐾)(𝑃 ∨ 𝑄) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟))))
76	75	impd 410	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵)) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
77	23, 13, 56, 35, 76	syl13anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
78	77	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
79	53, 73, 78	mp2and 698	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟))
80	4, 26	latjcl 18425	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑃 ∨ 𝑟) ∈ 𝐵)
81	33, 35, 25, 80	syl3anc 1369	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑟) ∈ 𝐵)
82	4, 5, 26	latjle12 18436	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
83	33, 35, 58, 81, 82	syl13anc 1370	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
84	83	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
85	43, 79, 84	mpbi2and 711	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟))
86	5, 26, 7	hlatlej1 38842	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
87	23, 12, 56, 86	syl3anc 1369	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
88	87	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
89	4, 5, 26	latjle12 18436	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
90	33, 35, 25, 60, 89	syl13anc 1370	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
91	90	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
92	88, 73, 91	mpbi2and 711	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄))
93	33, 60, 81	3jca 1126	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵))
94	93	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵))
95	4, 5	latasymb 18428	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵) → (((𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟) ∧ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟)))
96	94, 95	syl 17	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (((𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟) ∧ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟)))
97	85, 92, 96	mpbi2and 711	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟))
98		breq2 5147	. . . . . . . . . . . 12 ⊢ ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → (𝑋 < (𝑃 ∨ 𝑄) ↔ 𝑋 < (𝑃 ∨ 𝑟)))
99	98	biimpcd 248	. . . . . . . . . . 11 ⊢ (𝑋 < (𝑃 ∨ 𝑄) → ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → 𝑋 < (𝑃 ∨ 𝑟)))
100	99	adantr 480	. . . . . . . . . 10 ⊢ ((𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋) → ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → 𝑋 < (𝑃 ∨ 𝑟)))
101	100	ad2antll 728	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → 𝑋 < (𝑃 ∨ 𝑟)))
102	97, 101	mpd 15	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑋 < (𝑃 ∨ 𝑟))
103	4, 5, 62, 27	cvrnbtwn3 38743	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) ↔ 𝑟 = 𝑋))
104	103	biimpd 228	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
105	104	3expia 1119	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋)))
106	68, 25, 81, 55, 105	syl13anc 1370	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋)))
107	106	exp4a 431	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑟) → 𝑟 = 𝑋))))
108	107	com23 86	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → (𝑋 < (𝑃 ∨ 𝑟) → 𝑟 = 𝑋))))
109	108	imp4b 421	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ 𝑟(le‘𝐾)𝑋) → ((𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
110	109	adantrr 716	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
111	40, 102, 110	mp2and 698	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟 = 𝑋)
112		simpl3 1191	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟 ∈ 𝐴)
113	111, 112	eqeltrrd 2830	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑋 ∈ 𝐴)
114	113	exp45 438	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
115	114	3expa 1116	. . . 4 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
116	115	rexlimdva 3151	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
117	10, 116	syld 47	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋 ≠ 0 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
118	117	imp32 418	1 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ (𝑋 ≠ 0 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 395   ∧ w3a 1085   = wceq 1534   ∈ wcel 2099   ≠ wne 2936  ∃wrex 3066   class class class wbr 5143  ‘cfv 6543  (class class class)co 7415  Basecbs 17174  lecple 17234  Posetcpo 18293  ltcplt 18294  joincjn 18297  0.cp0 18409  Latclat 18417   ⋖ ccvr 38729  Atomscatm 38730  AtLatcal 38731  HLchlt 38817

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-10 2130  ax-11 2147  ax-12 2167  ax-ext 2699  ax-rep 5280  ax-sep 5294  ax-nul 5301  ax-pow 5360  ax-pr 5424  ax-un 7735

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-nf 1779  df-sb 2061  df-mo 2530  df-eu 2559  df-clab 2706  df-cleq 2720  df-clel 2806  df-nfc 2881  df-ne 2937  df-ral 3058  df-rex 3067  df-rmo 3372  df-reu 3373  df-rab 3429  df-v 3472  df-sbc 3776  df-csb 3891  df-dif 3948  df-un 3950  df-in 3952  df-ss 3962  df-nul 4320  df-if 4526  df-pw 4601  df-sn 4626  df-pr 4628  df-op 4632  df-uni 4905  df-iun 4994  df-br 5144  df-opab 5206  df-mpt 5227  df-id 5571  df-xp 5679  df-rel 5680  df-cnv 5681  df-co 5682  df-dm 5683  df-rn 5684  df-res 5685  df-ima 5686  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-riota 7371  df-ov 7418  df-oprab 7419  df-proset 18281  df-poset 18299  df-plt 18316  df-lub 18332  df-glb 18333  df-join 18334  df-meet 18335  df-p0 18411  df-lat 18418  df-clat 18485  df-oposet 38643  df-ol 38645  df-oml 38646  df-covers 38733  df-ats 38734  df-atl 38765  df-cvlat 38789  df-hlat 38818

This theorem is referenced by:  cvrat  38890