This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑋 ∧ 𝑌 ) 𝐶 𝑌 → 𝑋 𝐶 ( 𝑋 ∨ 𝑌 ) ) )