proposition: Lemma wo_subset_increasing_union : forall a f : E, axioms a -> increasing_ds_family a f -> (forall b : E, inc b f -> is_wo_subset a b) -> is_wo_subset a (union f).
proof: Proof. ir. uhg. dj. uhg; dj. am. uhg; ir. cp (union_exists H3). nin H4; ee. cp (H1 x0 H5). ufi is_wo_subset H6. ee. ufi is_linear_subset H6; ee. ap H8; am. uhg; dj. ap suborder_axioms. am. am. rwi underlying_suborder H5. rwi underlying_suborder H6. cp (union_exists H5). nin H7. cp (union_exists H6). nin H8. ee. ufi increasing_ds_family H0. cp (H0 _ _ H10 H9). nin H11. assert (inc y x0). ufi downward_saturated H11. ee. ap H13; am. cp (H1 x0 H10). ufi is_wo_subset H13. ee. ufi is_linear_subset H13; ee. ufi is_linear H16; ee. assert (inc x (U (suborder x0 a))). rw underlying_suborder. am. assert (inc y (U (suborder x0 a))). rw underlying_suborder. am. cp (H17 x y H18 H19). nin H20. ap or_introl. rwi leq_suborder_all H20. rw leq_suborder_all. ee; am. am. am. am. am. ap or_intror. rwi leq_suborder_all H20. rw leq_suborder_all. ee; am. am. am. am. am. assert (inc x x1). ufi downward_saturated H11. ee. ap H13; am. cp (H1 x1 H9). ufi is_wo_subset H13. ee. ufi is_linear_subset H13; ee. ufi is_linear H16; ee. assert (inc x (U (suborder x1 a))). rw underlying_suborder. am. assert (inc y (U (suborder x1 a))). rw underlying_suborder. am. cp (H17 x y H18 H19). nin H20. ap or_introl. rwi leq_suborder_all H20. rw leq_suborder_all. ee; am. am. am. am. am. ap or_intror. rwi leq_suborder_all H20. rw leq_suborder_all. ee; am. am. am. am. am. uhg; dj. ufi is_linear_subset H2; ee. am. nin H5. assert (inc y (union f)). rwi underlying_suborder H4. ap H4. am. cp (union_exists H6). nin H7. ee. assert (is_wo_subset a x). ap H1; am. ufi is_wo_subset H9. ee. assert (nonempty (intersection2 b x)). sh y. ap intersection2_inc. am. am. set (z := choose_bottom_element (suborder x a) (intersection2 b x)). assert (is_bottom_element (suborder x a) (intersection2 b x) z). uf z. ap wo_choose_bottom. am. uf sub; ir. cp (intersection2_second H12). rw underlying_suborder. am. am. sh z. ufi is_bottom_element H12. ee. assert (sub (union f) (U a)). uf sub; ir. cp (union_exists H14). nin H15; ee. assert (is_wo_subset a x1). ap H1; am. ufi is_wo_subset H17; ee. ufi is_linear_subset H17; ee. ap H19. am. uf is_bottom_element; dj. ufi is_lower_bound H12; uf is_lower_bound; ee. ap suborder_axioms. am. am. am. rw underlying_suborder. apply union_inc with x. rwi underlying_suborder H16; am. am. ir. assert (inc y0 (union f)). rwi underlying_suborder H4. ap H4; am. cp (union_exists H19). nin H20; ee. ufi increasing_ds_family H0. cp (H0 x x0 H8 H21). nin H22. assert (leq (suborder x a) z y0). ap H17. ap intersection2_inc. am. ufi downward_saturated H22. ee. ap H24; am. rw leq_suborder_all. rwi leq_suborder_all H23. ee. apply union_inc with x. am. am. apply union_inc with x. am. am. am. am. ufi is_linear_subset H9; ee. am. am. am. ufi is_linear H3. ee. assert (leq (suborder (union f) a) z y0 \/ leq (suborder (union f) a) y0 z). ap H23. rw underlying_suborder. apply union_inc with x. apply intersection2_second with b. am. am. rw underlying_suborder. am. nin H24. am. assert (inc z x). apply intersection2_second with b. exact H13. assert (inc y0 x). ufi downward_saturated H22. ee. apply H28 with z. am. am. rwi leq_suborder_all H24; ee. am. am. am. assert (leq (suborder x a) z y0). ap H17. ap intersection2_inc. am. am. rw leq_suborder_all; ee. apply union_inc with x. am. am. apply union_inc with x. am. am. rwi leq_suborder_all H27; ee. am. am. ufi is_linear_subset H9; ee. exact H28. am. am. apply intersection2_first with x. am. Qed.
imports: universe