proposition: Lemma ultrafilter_extension: forall {X:Type} (F:Filter X), exists U:Filter X, Included (filter_family F) (filter_family U) /\ ultrafilter U.
proof: Proof. intros. pose (PO := { F':Filter X | Included (filter_family F) (filter_family F') }). pose (PO_ord := fun (F1' F2':PO) => Included (filter_family (proj1_sig F1')) (filter_family (proj1_sig F2'))). assert (exists U:PO, premaximal PO_ord U). { apply ZornsLemmaForPreorders. - constructor. + red; intro. destruct x. red; simpl. auto with sets. + red; intros. destruct x, y, z. red in H; simpl in H. red in H0; simpl in H0. red; simpl. auto with sets. - intros. destruct (classic_dec (Inhabited S)) as [Hnonempty|Hempty]. + unshelve refine (let H0:=_ in let H1:=_ in let H2:=_ in let H3:=_ in let ub:=Build_Filter X (IndexedUnion (fun F':{F':PO | In S F'} => filter_family (proj1_sig (proj1_sig F')))) H0 H1 H2 H3 in _); [ | clearbody H0 | clearbody H0 H1 | clearbody H0 H1 H2 | clearbody H0 H1 H2 H3 ]. * intros. destruct H0 as [F1']. destruct H1 as [F2']. destruct F1' as [[F1']]. destruct F2' as [[F2']]. simpl in H0. simpl in H1. destruct (H (exist _ F1' i) (exist _ F2' i1)); trivial. -- red in H2; simpl in H2. apply H2 in H0. exists (exist _ (exist _ F2' i1) i2). simpl. apply filter_intersection; trivial. -- red in H2; simpl in H2. apply H2 in H1. exists (exist _ (exist _ F1' i) i0). simpl. apply filter_intersection; trivial. * intros. destruct H1 as [[[F1']]]. simpl in H1. exists (exist _ (exist _ F1' i) i0). simpl. apply filter_upward_closed with x; trivial. * destruct Hnonempty. exists (exist _ x H2). simpl. apply filter_full. * red; intro. inversion_clear H3 as [F']. contradict H4. apply filter_empty. * assert (Included (filter_family F) (filter_family ub)). { simpl. red; intros. destruct Hnonempty. exists (exist _ x0 H5). simpl. destruct x0 as [F']. simpl. auto. } exists (exist _ ub H4). intros. red; simpl. red; intros. exists (exist _ y H5). simpl. trivial. + assert (Included (filter_family F) (filter_family F)). { auto with sets. } exists (exist _ F H0). intros. contradiction Hempty. exists y; trivial. } destruct H as [[U]]. exists U; split; trivial. red; intros. classical_right. assert (forall S':Ensemble X, In (filter_family U) S' -> Inhabited (Intersection S' (Ensembles.Complement S))). { intros. apply NNPP; red; intro. contradiction H0. apply filter_upward_closed with S'; trivial. red; intros. apply NNPP; red; intro. contradiction H2. exists x. auto with sets. } unshelve refine (let H2:=_ in let H3:=_ in let H4:=_ in let Uext := Build_Filter_from_basis (Im (filter_family U) (fun S':Ensemble X => Intersection S' (Ensembles.Complement S))) H2 H3 H4 in _). - exists (Ensembles.Complement S). exists Full_set. + apply filter_full. + apply Extensionality_Ensembles; split; auto with sets. - red; intros. inversion_clear H3 as [S']. destruct (H1 S' H4) as [x]. rewrite <- H5 in H3. destruct H3. - intros. destruct H4. destruct H5. exists (Intersection y y0). split; auto with sets. exists (Intersection x x0). + apply filter_intersection; trivial. + subst. apply Extensionality_Ensembles; split; red; intros. * destruct H6, H6, H7. auto with sets. * destruct H6, H6. auto with sets. - assert (Included (filter_family U) (filter_family Uext)). { red; intros. apply filter_upward_closed with (Intersection x (Ensembles.Complement S)). - assert (filter_basis Uext (Im (filter_family U) (fun S':Ensemble X => Intersection S' (Ensembles.Complement S)))). { apply filter_from_basis_basis. } destruct H6. apply filter_basis_elements0. exists x; trivial. - auto with sets. } assert (Included (filter_family F) (filter_family Uext)). { auto with sets. } assert (PO_ord (exist _ U i) (exist _ Uext H6)). { red. exact H5. } apply H in H7. apply H7. change (In (filter_family Uext) (Ensembles.Complement S)). assert (filter_basis Uext (Im (filter_family U) (fun S':Ensemble X => Intersection S' (Ensembles.Complement S)))). { apply filter_from_basis_basis. } destruct H8. apply filter_basis_elements0. exists Full_set. + apply filter_full. + rewrite Intersection_Full_set. reflexivity. Qed.
imports: ZornsLemma(DecidableDec FiniteIntersections FunctionProperties) ZornsLemma(FiniteIntersections) ZornsLemma(ZornsLemma)