proposition: Lemma wo_subset_new : forall a b x : E, is_wo_subset a b -> ~ inc x b -> is_upper_bound a b x -> is_wo_subset a (union2 b (singleton x)).
proof: Proof. ir. ufk is_wo_subset H. ufk is_upper_bound H1. ee. ufk is_well_ordered H3. ufk is_linear_subset H. ee. ufk is_linear H8. ee. uhg; dj. uhg; dj. am. uf sub; ir. cp (union2_or H11). nin H12. ap H2. am. cp (singleton_eq H12). rw H13; am. uhg; dj. ap suborder_axioms. am. am. rwi underlying_suborder H13. rwi underlying_suborder H14. cp (union2_or H13). cp (union2_or H14). nin H15. nin H16. ufi is_linear X4. ee. assert (leq (suborder b a) x0 y \/ leq (suborder b a) y x0). ap H18. rw underlying_suborder; am. rw underlying_suborder; am. nin H19. ap or_introl. rw leq_suborder_all; ee. am. am. rwi leq_suborder_all H19. ee. am. am. am. am. am. ap or_intror. rw leq_suborder_all; ee. am. am. rwi leq_suborder_all H19. ee; am. am. am. am. am. cp (singleton_eq H16). ap or_introl. rw leq_suborder_all; ee. am. am. rw H17. ap H5. am. am. am. cp (singleton_eq H15). ap or_intror. rw leq_suborder_all; ee. am. am. rw H17. nin H16. ap H5; am. cp (singleton_eq H16). rw H18. ufi axioms H; ee. ap H. am. am. am. uhg. dj. ufi is_linear_subset H10. ee. am. apply by_cases with (nonempty (intersection2 b0 b)). ir. ufi is_well_ordered X2. ee. set (b1 := intersection2 b0 b) in *. assert (sub b1 (U (suborder b a))). rw underlying_suborder. uf b1; uf sub; ir. apply intersection2_second with b0. am. cp (H16 b1 H17 H14). nin H18. sh x0. uhg; dj. uhg; dj. ap suborder_axioms. am. uf sub; ir. cp (union2_or H19). nin H20. ap H2; am. cp (singleton_eq H20). rw H21. am. am. rw underlying_suborder. apply union2_first. rwi underlying_suborder H17. ap H17. ufi is_bottom_element H18; ee. am. rw leq_suborder_all. ee. rwi underlying_suborder H21. exact H21. rwi underlying_suborder H20. ap H20. am. apply by_cases with (inc y b). ir. assert (inc y b1). uf b1; ap intersection2_inc; am. ufi is_bottom_element H18; ee. ufi is_lower_bound H18; ee. cp (H28 y H24). rwi leq_suborder_all H29. ee. am. am. am. ir. assert (inc y (union2 b (singleton x))). rwi underlying_suborder H20. ap H20. am. cp (union2_or H24). nin H25. assert False. ap H23; am. elim H26. cp (singleton_eq H25). rw H26. assert (inc x0 (union2 b (singleton x))). rwi underlying_suborder H21; exact H21. cp (union2_or H27). nin H28. ap H5. am. cp (singleton_eq H28). rw H29. ufi axioms H1; ee. ap H1; am. am. uf sub; ir. cp (union2_or H23). nin H24. ap H2; am. cp (singleton_eq H24). rw H25; am. ufi is_bottom_element H18. ee. ufi b1 H20. apply intersection2_first with b; am. ir. assert (sub b0 (singleton x)). uf sub; ir. rwi underlying_suborder H12. assert (inc x0 (union2 b (singleton x))). ap H12. am. cp (union2_or H16). nin H17. assert False. ap H14. sh x0. ap intersection2_inc; am. elim H18. am. assert (b0 = singleton x). ap extensionality. am. uf sub; ir. cp (singleton_eq H16). rw H17. nin H13. assert (inc y (singleton x)). ap H15; am. cp (singleton_eq H18). wr H19. am. rw H16. sh x. uhg; dj. uhg; dj. ap suborder_axioms. am. ufi is_linear_subset H10; ee. am. uf sub; ir. rw underlying_suborder. ap union2_second. am. rw underlying_suborder. ap union2_second. ap singleton_inc. cp (singleton_eq H20). rw H21. rw leq_suborder_all. dj. ap union2_second; ap singleton_inc. am. ufi axioms H1; ee; ap H1. am. am. ufi is_linear_subset H10; ee; am. ap singleton_inc. Qed.
imports: universe