Theorem cvratlem 39404

Description: Lemma for cvrat 39405. (atcvatlem 32414 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 39342	. . . . 5 ⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat)
2	1	adantr 480	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝐾 ∈ AtLat)
3		simpr1 1193	. . . 4 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → 𝑋 ∈ 𝐵)
4		cvrat.b	. . . . . 6 ⊢ 𝐵 = (Base‘𝐾)
5		eqid 2735	. . . . . 6 ⊢ (le‘𝐾) = (le‘𝐾)
6		cvrat.z	. . . . . 6 ⊢ 0 = (0.‘𝐾)
7		cvrat.a	. . . . . 6 ⊢ 𝐴 = (Atoms‘𝐾)
8	4, 5, 6, 7	atlex 39298	. . . . 5 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋)
9	8	3expia 1120	. . . 4 ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋))
10	2, 3, 9	syl2anc 584	. . 3 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → (𝑋 ≠ 0 → ∃𝑟 ∈ 𝐴 𝑟(le‘𝐾)𝑋))
11	1	3ad2ant1 1132	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ AtLat)
12		simp22 1206	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃 ∈ 𝐴)
13		simp3 1137	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐴)
14	5, 7	atcmp 39293	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 ↔ 𝑃 = 𝑟))
15	11, 12, 13, 14	syl3anc 1370	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃(le‘𝐾)𝑟 ↔ 𝑃 = 𝑟))
16		breq1 5151	. . . . . . . . . . . . . . . . 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 1135	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ HL)
24	4, 7	atbase 39271	. . . . . . . . . . . . . 14 ⊢ (𝑟 ∈ 𝐴 → 𝑟 ∈ 𝐵)
25	24	3ad2ant3 1134	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑟 ∈ 𝐵)
26		cvrat.j	. . . . . . . . . . . . . 14 ⊢ ∨ = (join‘𝐾)
27		eqid 2735	. . . . . . . . . . . . . 14 ⊢ ( ⋖ ‘𝐾) = ( ⋖ ‘𝐾)
28	4, 5, 26, 27, 7	cvr1 39393	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃(le‘𝐾)𝑟 ↔ 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
29	23, 25, 12, 28	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (¬ 𝑃(le‘𝐾)𝑟 ↔ 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
30	22, 29	sylibd 239	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → ((𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋) → 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃)))
31	30	imp 406	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑟 ∨ 𝑃))
32		hllat 39345	. . . . . . . . . . . . 13 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat)
33	32	3ad2ant1 1132	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ Lat)
34	4, 7	atbase 39271	. . . . . . . . . . . . 13 ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵)
35	12, 34	syl 17	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃 ∈ 𝐵)
36	4, 26	latjcom 18505	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
37	33, 35, 25, 36	syl3anc 1370	. . . . . . . . . . 11 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
38	37	adantr 480	. . . . . . . . . 10 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → (𝑃 ∨ 𝑟) = (𝑟 ∨ 𝑃))
39	31, 38	breqtrrd 5176	. . . . . . . . 9 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ ¬ 𝑃(le‘𝐾)𝑋)) → 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟))
40	39	adantrrl 724	. . . . . . . 8 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟))
41	5, 26, 7	hlatlej1 39357	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
42	23, 12, 13, 41	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
43	42	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑟))
44	5, 7	atcmp 39293	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ AtLat ∧ 𝑟 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃))
45	11, 13, 12, 44	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑃 ↔ 𝑟 = 𝑃))
46		breq1 5151	. . . . . . . . . . . . . . . . . 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 771	. . . . . . . . . . . . . 14 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → 𝑟(le‘𝐾)𝑋)
55		simp21 1205	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑋 ∈ 𝐵)
56		simp23 1207	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐴)
57	4, 7	atbase 39271	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑄 ∈ 𝐴 → 𝑄 ∈ 𝐵)
58	56, 57	syl 17	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑄 ∈ 𝐵)
59	4, 26	latjcl 18497	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵) → (𝑃 ∨ 𝑄) ∈ 𝐵)
60	33, 35, 58, 59	syl3anc 1370	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑄) ∈ 𝐵)
61	23, 55, 60	3jca 1127	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵))
62		cvrat.s	. . . . . . . . . . . . . . . . . 18 ⊢ < = (lt‘𝐾)
63	5, 62	pltle 18391	. . . . . . . . . . . . . . . . 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 39348	. . . . . . . . . . . . . . . . 17 ⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset)
68	67	3ad2ant1 1132	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝐾 ∈ Poset)
69	4, 5	postr 18378	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)))
70	68, 25, 55, 60, 69	syl13anc 1371	. . . . . . . . . . . . . . 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 39365	. . . . . . . . . . . . . . . 16 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵) ∧ ¬ 𝑟(le‘𝐾)𝑃) → (𝑟(le‘𝐾)(𝑃 ∨ 𝑄) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
75	74	3expia 1120	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵)) → (¬ 𝑟(le‘𝐾)𝑃 → (𝑟(le‘𝐾)(𝑃 ∨ 𝑄) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟))))
76	75	impd 410	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ HL ∧ (𝑟 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ∈ 𝐵)) → ((¬ 𝑟(le‘𝐾)𝑃 ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) → 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)))
77	23, 13, 56, 35, 76	syl13anc 1371	. . . . . . . . . . . . 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 18497	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵) → (𝑃 ∨ 𝑟) ∈ 𝐵)
81	33, 35, 25, 80	syl3anc 1370	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑃 ∨ 𝑟) ∈ 𝐵)
82	4, 5, 26	latjle12 18508	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑄 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑟) ∧ 𝑄(le‘𝐾)(𝑃 ∨ 𝑟)) ↔ (𝑃 ∨ 𝑄)(le‘𝐾)(𝑃 ∨ 𝑟)))
83	33, 35, 58, 81, 82	syl13anc 1371	. . . . . . . . . . . 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 39357	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
87	23, 12, 56, 86	syl3anc 1370	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
88	87	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑃(le‘𝐾)(𝑃 ∨ 𝑄))
89	4, 5, 26	latjle12 18508	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Lat ∧ (𝑃 ∈ 𝐵 ∧ 𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑄) ∈ 𝐵)) → ((𝑃(le‘𝐾)(𝑃 ∨ 𝑄) ∧ 𝑟(le‘𝐾)(𝑃 ∨ 𝑄)) ↔ (𝑃 ∨ 𝑟)(le‘𝐾)(𝑃 ∨ 𝑄)))
90	33, 35, 25, 60, 89	syl13anc 1371	. . . . . . . . . . . 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 1127	. . . . . . . . . . . 12 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵))
94	93	adantr 480	. . . . . . . . . . 11 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → (𝐾 ∈ Lat ∧ (𝑃 ∨ 𝑄) ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵))
95	4, 5	latasymb 18500	. . . . . . . . . . 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 5152	. . . . . . . . . . . 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 39258	. . . . . . . . . . . . . . 15 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) ↔ 𝑟 = 𝑋))
104	103	biimpd 229	. . . . . . . . . . . . . 14 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵) ∧ 𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟)) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋))
105	104	3expia 1120	. . . . . . . . . . . . 13 ⊢ ((𝐾 ∈ Poset ∧ (𝑟 ∈ 𝐵 ∧ (𝑃 ∨ 𝑟) ∈ 𝐵 ∧ 𝑋 ∈ 𝐵)) → (𝑟( ⋖ ‘𝐾)(𝑃 ∨ 𝑟) → ((𝑟(le‘𝐾)𝑋 ∧ 𝑋 < (𝑃 ∨ 𝑟)) → 𝑟 = 𝑋)))
106	68, 25, 81, 55, 105	syl13anc 1371	. . . . . . . . . . . 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 1192	. . . . . . 7 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑟 ∈ 𝐴)
113	111, 112	eqeltrrd 2840	. . . . . 6 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) ∧ (𝑟(le‘𝐾)𝑋 ∧ (𝑋 < (𝑃 ∨ 𝑄) ∧ ¬ 𝑃(le‘𝐾)𝑋))) → 𝑋 ∈ 𝐴)
114	113	exp45 438	. . . . 5 ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
115	114	3expa 1117	. . . 4 ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ 𝑟 ∈ 𝐴) → (𝑟(le‘𝐾)𝑋 → (𝑋 < (𝑃 ∨ 𝑄) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴))))
116	115	rexlimdva 3153	. . 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 1537   ∈ wcel 2106   ≠ wne 2938  ∃wrex 3068   class class class wbr 5148  ‘cfv 6563  (class class class)co 7431  Basecbs 17245  lecple 17305  Posetcpo 18365  ltcplt 18366  joincjn 18369  0.cp0 18481  Latclat 18489   ⋖ ccvr 39244  Atomscatm 39245  AtLatcal 39246  HLchlt 39332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-rep 5285  ax-sep 5302  ax-nul 5312  ax-pow 5371  ax-pr 5438  ax-un 7754

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-mo 2538  df-eu 2567  df-clab 2713  df-cleq 2727  df-clel 2814  df-nfc 2890  df-ne 2939  df-ral 3060  df-rex 3069  df-rmo 3378  df-reu 3379  df-rab 3434  df-v 3480  df-sbc 3792  df-csb 3909  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-pw 4607  df-sn 4632  df-pr 4634  df-op 4638  df-uni 4913  df-iun 4998  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5583  df-xp 5695  df-rel 5696  df-cnv 5697  df-co 5698  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702  df-iota 6516  df-fun 6565  df-fn 6566  df-f 6567  df-f1 6568  df-fo 6569  df-f1o 6570  df-fv 6571  df-riota 7388  df-ov 7434  df-oprab 7435  df-proset 18352  df-poset 18371  df-plt 18388  df-lub 18404  df-glb 18405  df-join 18406  df-meet 18407  df-p0 18483  df-lat 18490  df-clat 18557  df-oposet 39158  df-ol 39160  df-oml 39161  df-covers 39248  df-ats 39249  df-atl 39280  df-cvlat 39304  df-hlat 39333

This theorem is referenced by:  cvrat  39405