Theorem cvratlem 40302

Description: Lemma for cvrat 40303. (atcvatlem 32874 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 40241	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2	1	adantr 486	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ AtLat)
3		simpr1 1213	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑋 ∈ 𝐵)
4		cvrat.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
5		eqid 2762	. . . . . 6 ⊢ (le‘𝐾) = (le‘𝐾)
6		cvrat.z	. . . . . 6 ⊢ 0 = (0.‘𝐾)
7		cvrat.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
8	4, 5, 6, 7	atlex 40197	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋)
9	8	3expia 1139	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋))
10	2, 3, 9	syl2anc 596	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋))
11	1	3ad2ant1 1151	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ AtLat)
12		simp22 1226	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃 ∈ 𝐴)
13		simp3 1156	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
14	5, 7	atcmp 40192	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 ↔ 𝑃 = 𝑟))
15	11, 12, 13, 14	syl3anc 1398	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 ↔ 𝑃 = 𝑟))
16		breq1 5110	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 = 𝑟 → (𝑃(le‘𝐾)𝑋 ↔ 𝑟(le‘𝐾)𝑋))
17	16	biimprd 251	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 = 𝑟 → (𝑟(le‘𝐾)𝑋 → 𝑃(le‘𝐾)𝑋))
18	15, 17	biimtrdi 256	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 → (𝑟(le‘𝐾)𝑋 → 𝑃(le‘𝐾)𝑋)))
19	18	com23 87	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑃(le‘𝐾)𝑟 → 𝑃(le‘𝐾)𝑋)))
20		con3 154	. . . . . . . . . . . . . 14 ⊢ ((𝑃(le‘𝐾)𝑟 → 𝑃(le‘𝐾)𝑋) → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑃(le‘𝐾)𝑟))
21	19, 20	syl6 36	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑃(le‘𝐾)𝑟)))
22	21	impd 416	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋) → ¬ 𝑃(le‘𝐾)𝑟))
23		simp1 1154	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ HL)
24	4, 7	atbase 40170	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵)
25	24	3ad2ant3 1153	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐵)
26		cvrat.j	. . . . . . . . . . . . . 14 ⊢ ∨ = (join‘𝐾)
27		eqid 2762	. . . . . . . . . . . . . 14 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
28	4, 5, 26, 27, 7	cvr1 40291	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃(le‘𝐾)𝑟 ↔ 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
29	23, 25, 12, 28	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (¬ 𝑃(le‘𝐾)𝑟 ↔ 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
30	22, 29	sylibd 242	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋) → 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
31	30	imp 412	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃))
32		hllat 40244	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
33	32	3ad2ant1 1151	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ Lat)
34	4, 7	atbase 40170	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
35	12, 34	syl 18	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃 ∈ 𝐵)
36	4, 26	latjcom 18541	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
37	33, 35, 25, 36	syl3anc 1398	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
38	37	adantr 486	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
39	31, 38	breqtrrd 5137	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟))
40	39	adantrrl 737	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟))
41	5, 26, 7	hlatlej1 40256	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
42	23, 12, 13, 41	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
43	42	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
44	5, 7	atcmp 40192	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ AtLat ∧ 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃))
45	11, 13, 12, 44	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃))
46		breq1 5110	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑃 → (𝑟(le‘𝐾)𝑋 ↔ 𝑃(le‘𝐾)𝑋))
47	46	biimpd 232	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑃 → (𝑟(le‘𝐾)𝑋 → 𝑃(le‘𝐾)𝑋))
48	45, 47	biimtrdi 256	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 → (𝑟(le‘𝐾)𝑋 → 𝑃(le‘𝐾)𝑋)))
49	48	com23 87	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑟(le‘𝐾)𝑃 → 𝑃(le‘𝐾)𝑋)))
50		con3 154	. . . . . . . . . . . . . . 15 ⊢ ((𝑟(le‘𝐾)𝑃 → 𝑃(le‘𝐾)𝑋) → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑟(le‘𝐾)𝑃))
51	49, 50	syl6 36	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (¬ 𝑃(le‘𝐾)𝑋 → ¬ 𝑟(le‘𝐾)𝑃)))
52	51	imp32 424	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → ¬ 𝑟(le‘𝐾)𝑃)
53	52	adantrrl 737	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ¬ 𝑟(le‘𝐾)𝑃)
54		simprl 783	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → 𝑟(le‘𝐾)𝑋)
55		simp21 1225	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑋 ∈ 𝐵)
56		simp23 1227	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐴)
57	4, 7	atbase 40170	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵)
58	56, 57	syl 18	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐵)
59	4, 26	latjcl 18533	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → (𝑃 ∨ 𝑄) ∈ 𝐵)
60	33, 35, 58, 59	syl3anc 1398	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ 𝐵)
61	23, 55, 60	3jca 1146	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵))
62		cvrat.s	. . . . . . . . . . . . . . . . . 18 ⊢ < = (lt‘𝐾)
63	5, 62	pltle 18425	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑋 < (𝑃 ∨ 𝑄) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)))
64	63	imp 412	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) ∧ 𝑋 < (𝑃 ∨ 𝑄)) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
65	61, 64	sylan 592	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ 𝑋 < (𝑃 ∨ 𝑄)) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
66	65	adantrl 729	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
67		hlpos 40247	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
68	67	3ad2ant1 1151	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ Poset)
69	4, 5	postr 18414	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
70	68, 25, 55, 60, 69	syl13anc 1399	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
71	70	adantr 486	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
72	54, 66, 71	mp2and 712	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄))
73	72	adantrrr 738	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄))
74	4, 5, 26, 7	hlexch1 40263	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵) ∧ ¬ 𝑟(le‘𝐾)𝑃) → (𝑟(le‘𝐾)(𝑃 ∨ 𝑄) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
75	74	3expia 1139	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵)) → (¬ 𝑟(le‘𝐾)𝑃 → (𝑟(le‘𝐾)(𝑃 ∨ 𝑄) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟))))
76	75	impd 416	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵)) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
77	23, 13, 56, 35, 76	syl13anc 1399	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
78	77	adantr 486	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
79	53, 73, 78	mp2and 712	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟))
80	4, 26	latjcl 18533	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑃 ∨ 𝑟) ∈ 𝐵)
81	33, 35, 25, 80	syl3anc 1398	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑟) ∈ 𝐵)
82	4, 5, 26	latjle12 18544	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
83	33, 35, 58, 81, 82	syl13anc 1399	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
84	83	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
85	43, 79, 84	mpbi2and 725	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟))
86	5, 26, 7	hlatlej1 40256	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
87	23, 12, 56, 86	syl3anc 1398	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
88	87	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
89	4, 5, 26	latjle12 18544	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
90	33, 35, 25, 60, 89	syl13anc 1399	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
91	90	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
92	88, 73, 91	mpbi2and 725	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄))
93	33, 60, 81	3jca 1146	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵))
94	93	adantr 486	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵))
95	4, 5	latasymb 18536	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵) → (((𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟) ∧ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟)))
96	94, 95	syl 18	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (((𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟) ∧ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟)))
97	85, 92, 96	mpbi2and 725	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟))
98		breq2 5111	. . . . . . . . . . . 12 ⊢ ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → (𝑋 < (𝑃 ∨ 𝑄) ↔ 𝑋 < (𝑃 ∨ 𝑟)))
99	98	biimpcd 252	. . . . . . . . . . 11 ⊢ (𝑋 < (𝑃 ∨ 𝑄) → ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → 𝑋 < (𝑃 ∨ 𝑟)))
100	99	adantr 486	. . . . . . . . . 10 ⊢ ((𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋) → ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → 𝑋 < (𝑃 ∨ 𝑟)))
101	100	ad2antll 742	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → 𝑋 < (𝑃 ∨ 𝑟)))
102	97, 101	mpd 16	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑋 < (𝑃 ∨ 𝑟))
103	4, 5, 62, 27	cvrnbtwn3 40157	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) ↔ 𝑟 = 𝑋))
104	103	biimpd 232	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
105	104	3expia 1139	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋)))
106	68, 25, 81, 55, 105	syl13anc 1399	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋)))
107	106	exp4a 437	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑟) → 𝑟 = 𝑋))))
108	107	com23 87	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → (𝑋 < (𝑃 ∨ 𝑟) → 𝑟 = 𝑋))))
109	108	imp4b 427	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ 𝑟(le‘𝐾)𝑋) → ((𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
110	109	adantrr 730	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
111	40, 102, 110	mp2and 712	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟 = 𝑋)
112		simpl3 1212	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟 ∈ 𝐴)
113	111, 112	eqeltrrd 2863	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑋 ∈ 𝐴)
114	113	exp45 444	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
115	114	3expa 1136	. . . 4 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
116	115	rexlimdva 3165	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
117	10, 116	syld 48	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋 ≠ 0 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
118	117	imp32 424	1 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ (𝑋 ≠ 0 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2145   ≠ wne 2957  ∃wrex 3088   class class class wbr 5107  ‘cfv 6537  (class class class)co 7417  Basecbs 17307  lecple 17355  Posetcpo 18401  ltcplt 18402  joincjn 18405  0.cp0 18515  Latclat 18525   ⋖ ccvr 40143  Atomscatm 40144  AtLatcal 40145  HLchlt 40231

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2215  ax-ext 2734  ax-rep 5236  ax-sep 5255  ax-nul 5267  ax-pow 5334  ax-pr 5402  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rmo 3367  df-reu 3368  df-rab 3415  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4283  df-if 4486  df-pw 4562  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4871  df-iun 4956  df-br 5108  df-opab 5172  df-mpt 5191  df-id 5554  df-xp 5665  df-rel 5666  df-cnv 5667  df-co 5668  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-riota 7374  df-ov 7420  df-oprab 7421  df-proset 18388  df-poset 18407  df-plt 18422  df-lub 18438  df-glb 18439  df-join 18440  df-meet 18441  df-p0 18517  df-lat 18526  df-clat 18593  df-oposet 40057  df-ol 40059  df-oml 40060  df-covers 40147  df-ats 40148  df-atl 40179  df-cvlat 40203  df-hlat 40232

This theorem is used by:  cvrat  40303