Theorem cvratlem 38292

Description: Lemma for cvrat 38293. (atcvatlem 31638 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 38230	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2	1	adantr 482	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ AtLat)
3		simpr1 1195	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑋 ∈ 𝐵)
4		cvrat.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
5		eqid 2733	. . . . . 6 ⊢ (le‘𝐾) = (le‘𝐾)
6		cvrat.z	. . . . . 6 ⊢ 0 = (0.‘𝐾)
7		cvrat.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
8	4, 5, 6, 7	atlex 38186	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋)
9	8	3expia 1122	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋))
10	2, 3, 9	syl2anc 585	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋))
11	1	3ad2ant1 1134	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ AtLat)
12		simp22 1208	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃 ∈ 𝐴)
13		simp3 1139	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
14	5, 7	atcmp 38181	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 ↔ 𝑃 = 𝑟))
15	11, 12, 13, 14	syl3anc 1372	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 ↔ 𝑃 = 𝑟))
16		breq1 5152	. . . . . . . . . . . . . . . . 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 412	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋) → ¬ 𝑃(le‘𝐾)𝑟))
23		simp1 1137	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ HL)
24	4, 7	atbase 38159	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵)
25	24	3ad2ant3 1136	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐵)
26		cvrat.j	. . . . . . . . . . . . . 14 ⊢ ∨ = (join‘𝐾)
27		eqid 2733	. . . . . . . . . . . . . 14 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
28	4, 5, 26, 27, 7	cvr1 38281	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃(le‘𝐾)𝑟 ↔ 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
29	23, 25, 12, 28	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (¬ 𝑃(le‘𝐾)𝑟 ↔ 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
30	22, 29	sylibd 238	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋) → 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
31	30	imp 408	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃))
32		hllat 38233	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
33	32	3ad2ant1 1134	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ Lat)
34	4, 7	atbase 38159	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
35	12, 34	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃 ∈ 𝐵)
36	4, 26	latjcom 18400	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
37	33, 35, 25, 36	syl3anc 1372	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
38	37	adantr 482	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
39	31, 38	breqtrrd 5177	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟))
40	39	adantrrl 723	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟))
41	5, 26, 7	hlatlej1 38245	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
42	23, 12, 13, 41	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
43	42	adantr 482	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
44	5, 7	atcmp 38181	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ AtLat ∧ 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃))
45	11, 13, 12, 44	syl3anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃))
46		breq1 5152	. . . . . . . . . . . . . . . . . 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 420	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → ¬ 𝑟(le‘𝐾)𝑃)
53	52	adantrrl 723	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ¬ 𝑟(le‘𝐾)𝑃)
54		simprl 770	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → 𝑟(le‘𝐾)𝑋)
55		simp21 1207	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑋 ∈ 𝐵)
56		simp23 1209	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐴)
57	4, 7	atbase 38159	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵)
58	56, 57	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐵)
59	4, 26	latjcl 18392	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → (𝑃 ∨ 𝑄) ∈ 𝐵)
60	33, 35, 58, 59	syl3anc 1372	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ 𝐵)
61	23, 55, 60	3jca 1129	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵))
62		cvrat.s	. . . . . . . . . . . . . . . . . 18 ⊢ < = (lt‘𝐾)
63	5, 62	pltle 18286	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑋 < (𝑃 ∨ 𝑄) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)))
64	63	imp 408	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) ∧ 𝑋 < (𝑃 ∨ 𝑄)) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
65	61, 64	sylan 581	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ 𝑋 < (𝑃 ∨ 𝑄)) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
66	65	adantrl 715	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
67		hlpos 38236	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
68	67	3ad2ant1 1134	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ Poset)
69	4, 5	postr 18273	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
70	68, 25, 55, 60, 69	syl13anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
71	70	adantr 482	. . . . . . . . . . . . . 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 38253	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵) ∧ ¬ 𝑟(le‘𝐾)𝑃) → (𝑟(le‘𝐾)(𝑃 ∨ 𝑄) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
75	74	3expia 1122	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵)) → (¬ 𝑟(le‘𝐾)𝑃 → (𝑟(le‘𝐾)(𝑃 ∨ 𝑄) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟))))
76	75	impd 412	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵)) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
77	23, 13, 56, 35, 76	syl13anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
78	77	adantr 482	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
79	53, 73, 78	mp2and 698	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟))
80	4, 26	latjcl 18392	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑃 ∨ 𝑟) ∈ 𝐵)
81	33, 35, 25, 80	syl3anc 1372	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑟) ∈ 𝐵)
82	4, 5, 26	latjle12 18403	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
83	33, 35, 58, 81, 82	syl13anc 1373	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
84	83	adantr 482	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
85	43, 79, 84	mpbi2and 711	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟))
86	5, 26, 7	hlatlej1 38245	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
87	23, 12, 56, 86	syl3anc 1372	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
88	87	adantr 482	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
89	4, 5, 26	latjle12 18403	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
90	33, 35, 25, 60, 89	syl13anc 1373	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
91	90	adantr 482	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
92	88, 73, 91	mpbi2and 711	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄))
93	33, 60, 81	3jca 1129	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵))
94	93	adantr 482	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵))
95	4, 5	latasymb 18395	. . . . . . . . . . 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 5153	. . . . . . . . . . . 12 ⊢ ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → (𝑋 < (𝑃 ∨ 𝑄) ↔ 𝑋 < (𝑃 ∨ 𝑟)))
99	98	biimpcd 248	. . . . . . . . . . 11 ⊢ (𝑋 < (𝑃 ∨ 𝑄) → ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → 𝑋 < (𝑃 ∨ 𝑟)))
100	99	adantr 482	. . . . . . . . . 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 38146	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) ↔ 𝑟 = 𝑋))
104	103	biimpd 228	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
105	104	3expia 1122	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋)))
106	68, 25, 81, 55, 105	syl13anc 1373	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋)))
107	106	exp4a 433	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑟) → 𝑟 = 𝑋))))
108	107	com23 86	. . . . . . . . . 10 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → (𝑋 < (𝑃 ∨ 𝑟) → 𝑟 = 𝑋))))
109	108	imp4b 423	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ 𝑟(le‘𝐾)𝑋) → ((𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
110	109	adantrr 716	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
111	40, 102, 110	mp2and 698	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟 = 𝑋)
112		simpl3 1194	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟 ∈ 𝐴)
113	111, 112	eqeltrrd 2835	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑋 ∈ 𝐴)
114	113	exp45 440	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
115	114	3expa 1119	. . . 4 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
116	115	rexlimdva 3156	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
117	10, 116	syld 47	. 2 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋 ≠ 0 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
118	117	imp32 420	1 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ (𝑋 ≠ 0 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107   ≠ wne 2941  ∃wrex 3071   class class class wbr 5149  ‘cfv 6544  (class class class)co 7409  Basecbs 17144  lecple 17204  Posetcpo 18260  ltcplt 18261  joincjn 18264  0.cp0 18376  Latclat 18384   ⋖ ccvr 38132  Atomscatm 38133  AtLatcal 38134  HLchlt 38220

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5364  ax-pr 5428  ax-un 7725

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-rmo 3377  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fn 6547  df-f 6548  df-f1 6549  df-fo 6550  df-f1o 6551  df-fv 6552  df-riota 7365  df-ov 7412  df-oprab 7413  df-proset 18248  df-poset 18266  df-plt 18283  df-lub 18299  df-glb 18300  df-join 18301  df-meet 18302  df-p0 18378  df-lat 18385  df-clat 18452  df-oposet 38046  df-ol 38048  df-oml 38049  df-covers 38136  df-ats 38137  df-atl 38168  df-cvlat 38192  df-hlat 38221

This theorem is referenced by:  cvrat  38293