Theorem cvrexchlem

Description: Lemma for cvrexch . ( cvexchlem analog.) (Contributed by NM, 18-Nov-2011)

	Ref	Expression
Hypotheses	cvrexch.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
	cvrexch.j	⊢ ∨ = ( join ‘ 𝐾 )
	cvrexch.m	⊢ ∧ = ( meet ‘ 𝐾 )
	cvrexch.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
Assertion	cvrexchlem	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		cvrexch.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		cvrexch.j	⊢ ∨ = ( join ‘ 𝐾 )
3		cvrexch.m	⊢ ∧ = ( meet ‘ 𝐾 )
4		cvrexch.c	⊢ 𝐶 = ( ⋖ ‘ 𝐾 )
5		hllat	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Lat )
6	1 3	latmcl	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
7	5 6	syl3an1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
8		eqid	⊢ ( lt ‘ 𝐾 ) = ( lt ‘ 𝐾 )
9	1 8 4	cvrlt	⊢ ( ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ) → ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) 𝑌 )
10	9	ex	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) 𝑌 ) )
11	7 10	syld3an2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) 𝑌 ) )
12		eqid	⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
13		eqid	⊢ ( Atoms ‘ 𝐾 ) = ( Atoms ‘ 𝐾 )
14	1 12 8 13	hlrelat1	⊢ ( ( 𝐾 ∈ HL ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) 𝑌 → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) )
15	7 14	syld3an2	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) 𝑌 → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) )
16	11 15	syld	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) )
17	16	imp	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ) → ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) )
18		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ HL )
19	18	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝐾 ∈ Lat )
20	1 13	atbase	⊢ ( 𝑝 ∈ ( Atoms ‘ 𝐾 ) → 𝑝 ∈ 𝐵 )
21	20	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑝 ∈ 𝐵 )
22		simpl2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑋 ∈ 𝐵 )
23		simpl3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑌 ∈ 𝐵 )
24	1 12 3	latlem12	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑝 ∈ 𝐵 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ↔ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) )
25	19 21 22 23 24	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ↔ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) )
26	25	biimpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑝 ( le ‘ 𝐾 ) 𝑋 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) )
27	26	expcomd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ( le ‘ 𝐾 ) 𝑌 → ( 𝑝 ( le ‘ 𝐾 ) 𝑋 → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) ) )
28		con3	⊢ ( ( 𝑝 ( le ‘ 𝐾 ) 𝑋 → 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) → ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) )
29	27 28	syl6	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( 𝑝 ( le ‘ 𝐾 ) 𝑌 → ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) → ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ) )
30	29	com23	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) → ( 𝑝 ( le ‘ 𝐾 ) 𝑌 → ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ) )
31	30	a1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) → ( 𝑝 ( le ‘ 𝐾 ) 𝑌 → ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) ) ) )
32	31	imp4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) → ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ) )
33		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → 𝑝 ∈ ( Atoms ‘ 𝐾 ) )
34	1 12 2 4 13	cvr1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
35	18 22 33 34	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) 𝑋 ↔ 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
36	32 35	sylibd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) → 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) ) )
37	36	imp	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) ) → 𝑋 𝐶 ( 𝑋 ∨ 𝑝 ) )
38		simpl1	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝐾 ∈ HL )
39	38	hllatd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝐾 ∈ Lat )
40		simpl2	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
41		simpl3	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
42	39 40 41 6	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 )
43		simpr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
44	1 2	latjass	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∈ 𝐵 ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) ) → ( ( 𝑋 ∨ ( 𝑋 ∧ 𝑌 ) ) ∨ 𝑝 ) = ( 𝑋 ∨ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ) )
45	39 40 42 43 44	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑋 ∨ ( 𝑋 ∧ 𝑌 ) ) ∨ 𝑝 ) = ( 𝑋 ∨ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ) )
46	1 2 3	latabs1	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 )
47	5 46	syl3an1	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 )
48	47	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑋 ∨ ( 𝑋 ∧ 𝑌 ) ) = 𝑋 )
49	48	oveq1d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑋 ∨ ( 𝑋 ∧ 𝑌 ) ) ∨ 𝑝 ) = ( 𝑋 ∨ 𝑝 ) )
50	45 49	eqtr3d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑋 ∨ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ) = ( 𝑋 ∨ 𝑝 ) )
51	50	adantr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) ) → ( 𝑋 ∨ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ) = ( 𝑋 ∨ 𝑝 ) )
52	1 12 8 2	latnle	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ↔ ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ) )
53	39 42 43 52	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ↔ ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ) )
54	1 12 3	latmle2	⊢ ( ( 𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 )
55	39 40 41 54	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 )
56	55	biantrurd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 ( le ‘ 𝐾 ) 𝑌 ↔ ( ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) )
57	1 12 2	latjle12	⊢ ( ( 𝐾 ∈ Lat ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( ( ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑌 ) )
58	39 42 43 41 57	syl13anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( ( 𝑋 ∧ 𝑌 ) ( le ‘ 𝐾 ) 𝑌 ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑌 ) )
59	56 58	bitrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( 𝑝 ( le ‘ 𝐾 ) 𝑌 ↔ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑌 ) )
60	53 59	anbi12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑌 ) ) )
61		hlpos	⊢ ( 𝐾 ∈ HL → 𝐾 ∈ Poset )
62	38 61	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → 𝐾 ∈ Poset )
63	1 2	latjcl	⊢ ( ( 𝐾 ∈ Lat ∧ ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∈ 𝐵 )
64	39 42 43 63	syl3anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∈ 𝐵 )
65	42 41 64	3jca	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∈ 𝐵 ) )
66	1 12 8 4	cvrnbtwn2	⊢ ( ( 𝐾 ∈ Poset ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ) → ( ( ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑌 ) ↔ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑌 ) )
67	66	biimpd	⊢ ( ( 𝐾 ∈ Poset ∧ ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ) → ( ( ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑌 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑌 ) )
68	67	3exp	⊢ ( 𝐾 ∈ Poset → ( ( ( 𝑋 ∧ 𝑌 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → ( ( ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑌 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑌 ) ) ) )
69	62 65 68	sylc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → ( ( ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑌 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑌 ) ) )
70	69	com23	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( ( 𝑋 ∧ 𝑌 ) ( lt ‘ 𝐾 ) ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ∧ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ( le ‘ 𝐾 ) 𝑌 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑌 ) ) )
71	60 70	sylbid	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑌 ) ) )
72	71	com23	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → ( ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑌 ) ) )
73	72	imp32	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) ) → ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) = 𝑌 )
74	73	oveq2d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) ) → ( 𝑋 ∨ ( ( 𝑋 ∧ 𝑌 ) ∨ 𝑝 ) ) = ( 𝑋 ∨ 𝑌 ) )
75	51 74	eqtr3d	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ 𝐵 ) ∧ ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) ) → ( 𝑋 ∨ 𝑝 ) = ( 𝑋 ∨ 𝑌 ) )
76	20 75	sylanl2	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) ) → ( 𝑋 ∨ 𝑝 ) = ( 𝑋 ∨ 𝑌 ) )
77	37 76	breqtrd	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ∧ ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) ) ) → 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) )
78	77	expr	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) ∧ ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ) → ( ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) → 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) )
79	78	an32s	⊢ ( ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ) ∧ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ) → ( ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) → 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) )
80	79	rexlimdva	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ) → ( ∃ 𝑝 ∈ ( Atoms ‘ 𝐾 ) ( ¬ 𝑝 ( le ‘ 𝐾 ) ( 𝑋 ∧ 𝑌 ) ∧ 𝑝 ( le ‘ 𝐾 ) 𝑌 ) → 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) )
81	17 80	mpd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 ) → 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) )
82	81	ex	⊢ ( ( 𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) )