Lemma pointwiselub_isdcpomorphism' {D D' : dcpo} {I : UU} (F : I -> posetofdcpomorphisms D D') (isdirec : isdirected F) : isdcpomorphism' (pointwiselub F isdirec). Proof. unfold isdcpomorphism'. intros J v isdirecv. intros w wislub. split. - intro j. apply pointwiselub_preservesorder. apply islub_isupperbound. exact wislub. - intros d' ineqs. eapply islub_isleast. + apply pointwiselub_islubpointwise. + intro i. unfold pointwisefamily. eapply dcpomorphism_preserveslub. * exact isdirecv. * exact wislub. * intro j. eapply istrans_posetRelation. 2: { exact (ineqs j). } apply pointwiselub_islubpointwise. Qed.
Require Import UniMath.Foundations.All.