Theorem cvratlem 39541

Description: Lemma for cvrat 39542. (atcvatlem 32367 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 39480	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2	1	adantr 480	. . . 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 39436	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋)
9	8	3expia 1121	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋))
10	2, 3, 9	syl2anc 584	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋))
11	1	3ad2ant1 1133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ AtLat)
12		simp22 1208	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃 ∈ 𝐴)
13		simp3 1138	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
14	5, 7	atcmp 39431	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 ↔ 𝑃 = 𝑟))
15	11, 12, 13, 14	syl3anc 1373	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 ↔ 𝑃 = 𝑟))
16		breq1 5096	. . . . . . . . . . . . . . . . 17 ⊢ (𝑃 = 𝑟 → (𝑃(le‘𝐾)𝑋 ↔ 𝑟(le‘𝐾)𝑋))
17	16	biimprd 248	. . . . . . . . . . . . . . . 16 ⊢ (𝑃 = 𝑟 → (𝑟(le‘𝐾)𝑋 → 𝑃(le‘𝐾)𝑋))
18	15, 17	biimtrdi 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 1136	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ HL)
24	4, 7	atbase 39409	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵)
25	24	3ad2ant3 1135	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐵)
26		cvrat.j	. . . . . . . . . . . . . 14 ⊢ ∨ = (join‘𝐾)
27		eqid 2733	. . . . . . . . . . . . . 14 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
28	4, 5, 26, 27, 7	cvr1 39530	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃(le‘𝐾)𝑟 ↔ 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
29	23, 25, 12, 28	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (¬ 𝑃(le‘𝐾)𝑟 ↔ 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
30	22, 29	sylibd 239	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋) → 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
31	30	imp 406	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃))
32		hllat 39483	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
33	32	3ad2ant1 1133	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ Lat)
34	4, 7	atbase 39409	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
35	12, 34	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃 ∈ 𝐵)
36	4, 26	latjcom 18355	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
37	33, 35, 25, 36	syl3anc 1373	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
38	37	adantr 480	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
39	31, 38	breqtrrd 5121	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟))
40	39	adantrrl 724	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟))
41	5, 26, 7	hlatlej1 39495	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
42	23, 12, 13, 41	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
43	42	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
44	5, 7	atcmp 39431	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ AtLat ∧ 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃))
45	11, 13, 12, 44	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃))
46		breq1 5096	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑟 = 𝑃 → (𝑟(le‘𝐾)𝑋 ↔ 𝑃(le‘𝐾)𝑋))
47	46	biimpd 229	. . . . . . . . . . . . . . . . 17 ⊢ (𝑟 = 𝑃 → (𝑟(le‘𝐾)𝑋 → 𝑃(le‘𝐾)𝑋))
48	45, 47	biimtrdi 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 724	. . . . . . . . . . . 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 39409	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵)
58	56, 57	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐵)
59	4, 26	latjcl 18347	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → (𝑃 ∨ 𝑄) ∈ 𝐵)
60	33, 35, 58, 59	syl3anc 1373	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ 𝐵)
61	23, 55, 60	3jca 1128	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵))
62		cvrat.s	. . . . . . . . . . . . . . . . . 18 ⊢ < = (lt‘𝐾)
63	5, 62	pltle 18239	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) → (𝑋 < (𝑃 ∨ 𝑄) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)))
64	63	imp 406	. . . . . . . . . . . . . . . 16 ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵) ∧ 𝑋 < (𝑃 ∨ 𝑄)) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
65	61, 64	sylan 580	. . . . . . . . . . . . . . 15 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ 𝑋 < (𝑃 ∨ 𝑄)) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
66	65	adantrl 716	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → 𝑋(le‘𝐾)(𝑃 ∨ 𝑄))
67		hlpos 39486	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
68	67	3ad2ant1 1133	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ Poset)
69	4, 5	postr 18228	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
70	68, 25, 55, 60, 69	syl13anc 1374	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
71	70	adantr 480	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
72	54, 66, 71	mp2and 699	. . . . . . . . . . . . 13 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄))
73	72	adantrrr 725	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄))
74	4, 5, 26, 7	hlexch1 39502	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵) ∧ ¬ 𝑟(le‘𝐾)𝑃) → (𝑟(le‘𝐾)(𝑃 ∨ 𝑄) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
75	74	3expia 1121	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵)) → (¬ 𝑟(le‘𝐾)𝑃 → (𝑟(le‘𝐾)(𝑃 ∨ 𝑄) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟))))
76	75	impd 410	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵)) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
77	23, 13, 56, 35, 76	syl13anc 1374	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
78	77	adantr 480	. . . . . . . . . . . 12 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
79	53, 73, 78	mp2and 699	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟))
80	4, 26	latjcl 18347	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑃 ∨ 𝑟) ∈ 𝐵)
81	33, 35, 25, 80	syl3anc 1373	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑟) ∈ 𝐵)
82	4, 5, 26	latjle12 18358	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
83	33, 35, 58, 81, 82	syl13anc 1374	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
84	83	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
85	43, 79, 84	mpbi2and 712	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟))
86	5, 26, 7	hlatlej1 39495	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
87	23, 12, 56, 86	syl3anc 1373	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
88	87	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
89	4, 5, 26	latjle12 18358	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
90	33, 35, 25, 60, 89	syl13anc 1374	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
91	90	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
92	88, 73, 91	mpbi2and 712	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄))
93	33, 60, 81	3jca 1128	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵))
94	93	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵))
95	4, 5	latasymb 18350	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵) → (((𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟) ∧ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟)))
96	94, 95	syl 17	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (((𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟) ∧ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟)))
97	85, 92, 96	mpbi2and 712	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟))
98		breq2 5097	. . . . . . . . . . . 12 ⊢ ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → (𝑋 < (𝑃 ∨ 𝑄) ↔ 𝑋 < (𝑃 ∨ 𝑟)))
99	98	biimpcd 249	. . . . . . . . . . 11 ⊢ (𝑋 < (𝑃 ∨ 𝑄) → ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → 𝑋 < (𝑃 ∨ 𝑟)))
100	99	adantr 480	. . . . . . . . . 10 ⊢ ((𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋) → ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → 𝑋 < (𝑃 ∨ 𝑟)))
101	100	ad2antll 729	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑟) → 𝑋 < (𝑃 ∨ 𝑟)))
102	97, 101	mpd 15	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑋 < (𝑃 ∨ 𝑟))
103	4, 5, 62, 27	cvrnbtwn3 39396	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) ↔ 𝑟 = 𝑋))
104	103	biimpd 229	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
105	104	3expia 1121	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋)))
106	68, 25, 81, 55, 105	syl13anc 1374	. . . . . . . . . . . 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 717	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → ((𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
111	40, 102, 110	mp2and 699	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟 = 𝑋)
112		simpl3 1194	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟 ∈ 𝐴)
113	111, 112	eqeltrrd 2834	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑋 ∈ 𝐴)
114	113	exp45 438	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
115	114	3expa 1118	. . . 4 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
116	115	rexlimdva 3134	. . 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 206   ∧ wa 395   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113   ≠ wne 2929  ∃wrex 3057   class class class wbr 5093  ‘cfv 6486  (class class class)co 7352  Basecbs 17122  lecple 17170  Posetcpo 18215  ltcplt 18216  joincjn 18219  0.cp0 18329  Latclat 18339   ⋖ ccvr 39382  Atomscatm 39383  AtLatcal 39384  HLchlt 39470

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-rmo 3347  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-riota 7309  df-ov 7355  df-oprab 7356  df-proset 18202  df-poset 18221  df-plt 18236  df-lub 18252  df-glb 18253  df-join 18254  df-meet 18255  df-p0 18331  df-lat 18340  df-clat 18407  df-oposet 39296  df-ol 39298  df-oml 39299  df-covers 39386  df-ats 39387  df-atl 39418  df-cvlat 39442  df-hlat 39471

This theorem is referenced by:  cvrat  39542