Coqで選択公理⇔ツォルンの補題を証明してみた(後編)

ページが重すぎるので分割します。
選択公理⇔ツォルンの補題の証明本体です。

前編
https://qiita.com/Meizen_OS/items/30cd4fb59ade0b94276e

中編
https://qiita.com/Meizen_OS/items/4dde1a9c8fbfa649db0a

Section AC_Zorn.

(*Zorn -> 部分集合版Zorn*)
Theorem ZornImpSbsZorn:
 (forall X R:Set, Poset X R -> 
  (forall A:Set, Sbs A X -> (forall x y:Set, In x A -> In y A -> REL R x y \/ REL R y x)
   -> exists u, In u X /\ forall x:Set, In x A -> REL R x u)
  -> exists u, In u X /\ forall v:Set, In v X -> REL R u v -> u = v)
->
 (forall X:Set,
  (forall A:Set, Sbs A X -> (forall x y:Set, In x A -> In y A -> Sbs x y \/ Sbs y x)
   -> exists u, In u X /\ forall x:Set, In x A -> Sbs x u)
  -> exists u, In u X /\ forall v:Set, In v X -> Sbs u v -> u = v).
Proof.
intros.
specialize (AxRelSbs X).
intro.
destruct H1.
specialize (RelSbsPoset X).
intro.
cut (forall A : Set,
     Sbs A X ->
     (forall x y : Set, In x A -> In y A -> REL (RelSbs X) x y \/ REL (RelSbs X) y x) ->
     exists u : Set, In u X /\ (forall x : Set, In x A -> REL (RelSbs X) x u)).
intro.
specialize (H X (RelSbs X) H3 H4).
destruct H.
destruct H.
exists x.
split.
apply H.
intros.
apply (H5 v H6).
apply (H2 x v H H6).
apply H7.

intros.
specialize (H0 A H4).
cut (forall x y : Set, In x A -> In y A -> Sbs x y \/ Sbs y x).
intro.
specialize (H0 H6).
destruct H0.
destruct H0.
exists x.
split.
apply H0.
intros.
specialize (H4 x0 H8).
apply (H2 x0 x H4 H0).
apply (H7 x0 H8).

intros.
specialize (H5 x y H6 H7).
apply H4 in H6.
apply H4 in H7.
destruct H5.
left.
apply (H2 x y H6 H7).
apply H5.
right.
apply (H2 y x H7 H6).
apply H5.
Qed.

(*部分集合版Zornのための補題*)
Theorem ExACSetUpper:forall a:Set, exists X,
 (forall f:Set, In f X <-> exists d, To f d (BCup a) /\ Sbs d a /\ forall x:Set, In x d -> In (VL f x) x) /\
 forall A:Set, Sbs A X -> (forall f g:Set, In f A -> In g A -> Sbs f g \/ Sbs g f)
 -> exists u, In u X /\ forall f:Set, In f A -> Sbs f u.
Proof.
intro.
cut (exists X, forall f:Set, In f X <-> exists d, To f d (BCup a) /\ Sbs d a /\ forall x:Set, In x d -> In (VL f x) x).
intro.
destruct H.
exists x.
split.
apply H.

intros.
specialize (AxUIff A). (*強い和集合公理*)
intro.
destruct H2.
exists x0.
split.

apply H.
cut (exists d, forall x:Set, In x d <-> exists f y, In f A /\ In (OP x y) f).
intro.
destruct H3.
exists x1.
cut (To x0 x1 (BCup a)).
intro.
split.
apply H4.
split.

unfold Sbs.
intros.
apply H3 in H5.
destruct H5.
destruct H5.
destruct H5.
apply H0 in H5.
apply H in H5.
destruct H5.
destruct H5.
destruct H7.
apply H7.
apply (ToRel x2 x4 (BCup a) z x3 H5 H6). (*順序対*)

intros.
apply H3 in H5.
destruct H5.
destruct H5.
destruct H5.
assert (F:=H5).
apply H0 in H5.
apply H in H5.
destruct H5.
destruct H5.
destruct H7.
specialize (ToRel x3 x5 (BCup a) x2 x4 H5 H6). (*順序対*)
intro.
destruct H9.
specialize (H8 x2 H9).
cut (In (OP x2 (VL x3 x2)) x0).
intro.
apply (ToVLIff x0 x1 (BCup a) x2 (VL x3 x2) H4) in H11.  (*順序対*)
destruct H11.
rewrite <- H12.
apply H8.
apply H2.

exists x3.
split.
apply F.
apply (ToVLOP x3 x5 (BCup a) x2 H5 H9). (*順序対*)

split.
intros.
apply H2 in H4.
destruct H4.
destruct H4.
assert (F:=H4).
apply H0 in H4.
apply H in H4.
destruct H4.
destruct H4.
destruct H4.
specialize (H4 z H5).
destruct H4.
destruct H4.
destruct H4.
destruct H8.
exists x4.
exists x5.
split.
apply H3.
exists x2.
exists x5.
split.
apply F.
rewrite <- H9.
apply H5.
split.
apply H8.
apply H9.

intros.
apply H3 in H4.
destruct H4.
destruct H4.
exists x4.
split.
apply H2.
exists x3.
apply H4.
intros.
apply H2 in H5.
destruct H5.
destruct H4.
destruct H5.
specialize (H1 x3 x5 H4 H5).
destruct H1.

apply H1 in H6.
apply H0 in H5.
apply H in H5.
destruct H5.
destruct H5.
apply (ToVLIff x5 x6 (BCup a) x2 x4 H5) in H6.
destruct H6.
apply (ToVLIff x5 x6 (BCup a) x2 x' H5) in H7.
destruct H7.
rewrite H10.
apply H9.

apply H1 in H7.
apply H0 in H4.
apply H in H4.
destruct H4.
destruct H4.
apply (ToVLIff x3 x6 (BCup a) x2 x4 H4) in H6.
destruct H6.
apply (ToVLIff x3 x6 (BCup a) x2 x' H4) in H7.
destruct H7.
rewrite H10.
apply H9.

apply ExSetIff. (*分出*)
exists a.
intros.
destruct H3.
destruct H3.
destruct H3.
apply H0 in H3.
apply H in H3.
destruct H3.
destruct H3.
destruct H5.
apply H5.
apply (ToRel x1 x3 (BCup a) z x2 H3 H4).

unfold Sbs.
intros.
apply H2.
exists f.
split.
apply H3.
apply H4.

apply ExSetIff.
exists (Pow (Times a (BCup a))).
intros.
apply AxPow.
unfold Sbs.
intros.
destruct H.
destruct H.
destruct H.
apply H in H0.
destruct H0.
destruct H0.
destruct H0.
destruct H3.
destruct H1.
rewrite H4.
apply TimesIff.
split.
apply H1.
apply H0.
apply H3.
Qed.

(*部分集合版Zorn -> 選択公理*)
Theorem SbsZornImpAC:
 (forall X:Set,
  (forall A:Set, Sbs A X -> (forall x y:Set, In x A -> In y A -> Sbs x y \/ Sbs y x)
   -> exists u, In u X /\ forall x:Set, In x A -> Sbs x u)
  -> exists u, In u X /\ forall v:Set, In v X -> Sbs u v -> u = v)
->
 (forall a:Set, 
 (forall x:Set, In x a -> exists w, In w x) ->
 exists f b, To f a b /\ forall x:Set, In x a ->  In (VL f x) x).
Proof.
intros.
specialize (ExACSetUpper a).
intro.
destruct H1.
destruct H1.
specialize (H x H2).
destruct H.
destruct H.
apply H1 in H.
destruct H.
exists x0.
exists (BCup a).
cut (x1 = a).
intro.
rewrite H4 in H.
split.
apply H.
apply H.

apply AxEx. (*外延*)
split.
apply H.
intro.
specialize (H0 z H4).
destruct H0.
RAA.
destruct H.
destruct H6.

cut (In (Cup x0 (Sngl (OP z x2))) x).
specialize (SbsCupL x0 (Sngl (OP z x2))).
intros.
specialize (H3 (Cup x0 (Sngl (OP z x2))) H9 H8).
cut (In (OP z x2) x0).
intro.
apply (ToRel x0 x1 (BCup a) z x2 H) in H10.
destruct H10.
contradiction.
rewrite H3.
apply AxCup.
right.
apply InSngl.

apply H1.
exists (Cup x1 (Sngl z)).
specialize (InInBCup a z x2 H0 H4).
intro.
apply (SnglTo z x2 (BCup a)) in H8.
cut (forall x3 : Set, In x3 x1 -> In x3 (Sngl z) -> VL x0 x3 = VL (Sngl (OP z x2)) x3).
intro.

split.
rewrite <- (IdCup (BCup a)).
apply (ToCup x0 x1 (BCup a) (Sngl (OP z x2)) (Sngl z) (BCup a) H H8 H9).

split.
unfold Sbs.
intros.
apply AxCup in H10.
destruct H10.
apply H6.
apply H10.
apply AxSngl in H10.
rewrite H10.
apply H4.

intros.
apply AxCup in H10.
destruct H10.
rewrite (ToCupVLL x0 x1 (BCup a)
 (Sngl (OP z x2)) (Sngl z) (BCup a) H H8 H9 x3 H10).
apply (H7 x3 H10).
rewrite (ToCupVLR x0 x1 (BCup a)
 (Sngl (OP z x2)) (Sngl z) (BCup a) H H8 H9 x3 H10).
apply AxSngl in H10.
rewrite H10.
rewrite SnglToVL.
apply H0.

intros.
apply AxSngl in H10.
rewrite H10 in H9.
contradiction.
Qed.

(*Zorn->ACの補題*)
Theorem TowerOrder:forall X R M g:Set,
 (forall A:Set, In A M <-> Sbs A X /\ forall x y:Set, In x A -> In y A -> REL R x y \/ REL R y x) ->
 To g M M ->
 (forall A:Set, In A M -> exists x, VL g A = Cup A (Sngl x)) ->
 exists T,
  (forall N:Set, In N T <->
  Sbs N M /\
  (forall A:Set, In A N -> In (VL g A) N) /\
   forall S:Set, Sbs S N  -> (forall A B:Set, In A S -> In B S -> Sbs A B \/ Sbs B A) ->In (BCup S) N) /\
 In M T /\
 In (BCap T) T /\
 forall A B:Set, In A (BCap T) -> In B (BCap T) -> Sbs A B \/ Sbs B A.
Proof.
intros.
specialize (ExPowIff (fun N =>(forall A:Set, In A N -> In (VL g A) N) /\
   forall S:Set, Sbs S N  -> (forall A B:Set, In A S -> In B S -> Sbs A B \/ Sbs B A) ->In (BCup S) N) M).
intro.
destruct H2.
exists x.
split.
apply H2.
cut (In M x).
intro T.
cut (forall S : Set,
      Sbs S (BCap x) ->
      (forall A B : Set, In A S -> In B S -> Sbs A B \/ Sbs B A) -> In (BCup S) (BCap x)).
intro T2.
cut (forall A : Set, In A (BCap x) -> In (VL g A) (BCap x)).
intro T1.
cut (Sbs (BCap x) M).
intros T0.

split.
apply T.
split.
apply H2.
split.
apply T0.
split.
apply T1.
apply T2.
cut (forall A: Set, In A (BCap x) ->
 forall B: Set, In B (BCap x) -> Sbs A B \/ Sbs B A).
intros.
apply (H3 A H4 B H5).
intro.
intro T3.
specialize (AxSS
 (fun A => forall B:Set, In B (BCap x) -> Sbs A B \/ Sbs B A) (BCap x)).
intro.
destruct H3.
cut (x0 = BCap x).
intro.
rewrite H4 in H3.
apply H3.
apply T3.

apply AxEx.
split.
intro.
apply H3 in H4.
apply H4.
cut (In x0 x).
intro.
apply (BCapSbs x x0 H4 z).

apply H2.
split.
unfold Sbs.
intros.
apply T0.
apply H3 in H4.
apply H4.
split.

intros.
apply H3.
split.
apply H3 in H4.
destruct H4.
apply (T1 A0 H4).



specialize (AxSS (fun B => Sbs (VL g A0) B \/ Sbs B A0) (BCap x)).
intro.
destruct H5.
cut (x1 = BCap x).
intro.
rewrite H6 in H5.
intros.
apply H5 in H7.
destruct H7.
destruct H8.
left.
apply H8.
right.
apply H3 in H4.
destruct H4.
apply T0 in H4.
specialize (H1 A0 H4).
destruct H1.
rewrite H1.
apply (TraSbs B A0 (Cup A0 (Sngl x2)) H8).
apply SbsCupL.


apply AxEx.
split.
intro.
apply H5 in H6.
apply H6.
cut (In x1 x).
intro.
apply (BCapSbs x x1 H6 z0).

apply H2.
split.
unfold Sbs.
intros.
apply T0.
apply H5 in H6.
apply H6.

split.
intros.
apply H5.
apply H5 in H6.
destruct H6.
split.
apply (T1 A1 H6).

assert (T4:=H6).
apply T0 in H6.
specialize (H1 A1 H6).
destruct H1.
destruct H7.
left.
rewrite H1.
apply (TraSbs (VL g A0) A1 (Cup A1 (Sngl x2)) H7).
apply SbsCupL.

apply H3 in H4.
destruct H4.
apply T1 in T4.
apply H8 in T4.
destruct T4.
rewrite H1 in H9.
apply (SbsCupSnglOr A1 A0 x2 H7) in H9.
destruct H9.
left.
rewrite H9.
apply RefSbs.
right.
rewrite H1.
rewrite <- H9.
apply RefSbs.
right.
apply H9.

intros.
apply H5.
split.
apply T2.
unfold Sbs.
intros.
apply H6 in H8.
apply H5 in H8.
apply H8.
apply H7.

specialize (Middle (Sbs (BCup S) A0)).
intro.
destruct H8.
right.
apply H8.
left.
unfold Sbs.
intros.
RAA.
apply H8.
unfold Sbs.
intros.
apply AxBCup in H11.
destruct H11.
destruct H11.
assert (T4:= H11).
apply H6 in H11.
apply H5 in H11.
destruct H11.
destruct H13.
apply H13 in H9.
cut (In z1 (BCup S)).
intro.
contradiction.
apply (InInBCup S x2 z1 H9 T4).
apply (H13 z2 H12).


intros.
apply H3.
split.
apply T2.
unfold Sbs.
intros.
apply H4 in H6.
apply H3 in H6.
apply H6.
apply H5.

intros.
specialize (Middle (exists A, In A S /\ Sbs B A)).
intros.
destruct H7.
destruct H7.
destruct H7.
right.
apply (TraSbs B x1 (BCup S) H8).
apply (SbsBCup S x1 H7).
left.
unfold Sbs.
intros.
apply AxBCup in H8.
destruct H8.
destruct H8.
assert (T4:=H8).
apply H4 in H8.
apply H3 in H8.
destruct H8.
specialize (H10 B H6).
destruct H10.
apply (H10 z0 H9).
cut (exists A : Set, In A S /\ Sbs B A).
intro.
contradiction.
exists x1.
split.
apply T4.
apply H10.



apply (BCapSbs x M T).

intros.
apply (AxInBCap x M (VL g A) T).
intros.
apply (BCapSbs x x0 H4 A) in H3.
apply H2 in H4.
destruct H4.
destruct H5.
apply (H5 A H3).

intros.
apply (AxInBCap x M (BCup S) T).
intros.
specialize (BCapSbs x x0 H5).
intro.
apply H2 in H5.
destruct H5.
destruct H7.
apply (TraSbs S (BCap x) x0 H3)  in H6.
apply (H8 S H6 H4).



apply H2.
split.
apply RefSbs.
split.
intros.
apply (ToVL g M M A H0 H3).

intros.
apply H.
split.
unfold Sbs.
intros.
apply AxBCup in H5.
destruct H5.
destruct H5.
apply H3 in H5.
apply H in H5.
destruct H5.
apply (H5 z H6).
intros.
apply AxBCup in H5.
destruct H5.
destruct H5.
apply AxBCup in H6.
destruct H6.
destruct H6.
specialize (H4 x1 x2 H5 H6).
destruct H4.
apply H3 in H6.
apply H in H6.
destruct H6.
apply H4 in H7.
apply (H9 x0 y H7 H8).
apply H3 in H5.
apply H in H5.
destruct H5.
apply H4 in H8.
apply (H9 x0 y H7 H8).
Qed.


(*Zorn -> 選択公理*)
Theorem ZornAC:
 (forall a:Set, 
 (forall x:Set, In x a -> exists w, In w x) ->
 exists f b, To f a b /\ forall x:Set, In x a ->  In (VL f x) x)
->
 (forall X R:Set, Poset X R -> 
  (forall A:Set, Sbs A X -> (forall x y:Set, In x A -> In y A -> REL R x y \/ REL R y x)
   -> exists u, In u X /\ forall x:Set, In x A -> REL R x u)
  -> exists u, In u X /\ forall v:Set, In v X -> REL R u v -> u = v).
Proof.
intros.
apply RAAF.
intro U.
cut (exists K, forall D: Set, In D K <->
 exists A, Sbs A X /\
 (forall x: Set, In x D <-> In x X /\ ~In x A /\ forall a: Set,In a A -> REL R a x) /\
 forall x y: Set, In x A -> In y A -> REL R x y \/ REL R y x).
intro.
destruct H2.
cut (forall D: Set, In D x -> exists v, In v D).
intro.
apply (H x) in H3.
destruct H3.
destruct H3.
destruct H3.
specialize (ExPowIff
 (fun A => forall x y: Set, In x A -> In y A -> REL R x y \/ REL R y x) X).
intro.
destruct H5.
cut (forall A: Set, In A x2 -> exists! y, In y x2 /\
 exists D, y = Cup A (Sngl (VL x0 D)) /\
 forall x: Set, In x D <-> In x X /\ ~In x A /\ forall a: Set,In a A -> REL R a x).
intro.
apply WDTo in H6.
destruct H6.
destruct H6.

cut (forall A : Set, In A x2 -> exists x4 : Set, VL x3 A = Cup A (Sngl x4)).
intro.
specialize (TowerOrder X R x2 x3 H5 H6 H8).
intro.
destruct H9.
destruct H9.
destruct H10.
destruct H11.
apply H9 in H11.
destruct H11.
destruct H13.
apply H14 in H12.
specialize (H13 (BCup (BCap x4)) H12).
apply SbsBCup in H13.
apply H11 in H12.
specialize (H7 (BCup (BCap x4)) H12).
destruct H7.
destruct H7.
rewrite H7 in H13.
specialize (SbsCupR (BCup (BCap x4)) (Sngl (VL x0 x5))).
specialize (InSngl (VL x0 x5)).
intros.
apply H17 in H16.
apply H13 in H16.

apply H5 in H12.
destruct H12.
cut (In x5 x).
intro.
specialize (H4 x5 H19).
apply H15 in H4.
destruct H4.
destruct H20.
contradiction.

apply H2.
exists (BCup (BCap x4)).
split.
apply H12.
split.
apply H15.
apply H18.
apply RefSbs.

intros.
specialize (H7 A H8).
destruct H7.
exists (VL x0 x4).
apply H7.

intros.
specialize (AxSS
 (fun x3 => ~ In x3 A /\ (forall a : Set, In a A -> REL R a x3)) X).
intro.
destruct H7.
exists (Cup A (Sngl (VL x0 x3))).
cut (In x3 x).
intro.
specialize (H4 x3 H8).
apply H7 in H4.

split.
split.
apply H5.
split.

unfold Sbs.
intros.
apply AxCup in H9.
destruct H9.
apply H5 in H6.
apply H6.
apply H9.
apply AxSngl in H9.
rewrite H9.
apply H4.

intros.
apply AxCup in H9.
apply AxCup in H10.
destruct H9.
destruct H10.
apply H5 in H6.
apply H6.
apply H9.
apply H10.

apply AxSngl in H10.
rewrite H10.
left.
apply H4.
apply H9.

apply AxSngl in H9.
destruct H10.
rewrite H9.
right.
apply H4.
apply H10.

apply AxSngl in H10.
left.
rewrite H10.
rewrite H9.
apply H0.
apply H4.

exists x3.
split.
reflexivity.
apply H7.
intros.
destruct H9.
destruct H10.
destruct H10.
rewrite H10.
cut (x3 = x4).
intro.
rewrite H12.
reflexivity.

apply AxEx.
split.
intro.
apply H11.
apply H7.
apply H12.
intro.
apply H7.
apply H11.
apply H12.

apply H2.
exists A.
split.
unfold Sbs.
intros.
apply H5 in H6.
apply H6.
apply H8.
split.
apply H7.
apply H5.
apply H6.


intros.
apply H2 in H3.
destruct H3.
destruct H3.
destruct H4.
specialize (H1 x0 H3 H5).
destruct H1.
destruct H1.
RAA.
apply U.
exists x1.
split.
apply H1.
intros.
RAA.
apply H7.
exists v.
apply H4.
split.
apply H8.
split.
intro.
apply H10.
specialize (H6 v H11).
apply H0.
apply H9.
apply H6.

intros.
specialize (H6 a H11).
destruct H0.
destruct H12.
destruct H13.
apply (H13 a x1 v H6 H9).


apply ExSetIff.
exists (Pow X).
intros.
destruct H2.
apply AxPow.
unfold Sbs.
intros.
apply H2 in H3.
apply H3.
Qed.

End AC_Zorn.

参考文献
[1] K. Kunen (藤田博司 訳), キューネン数学基礎論講義, 日本評論社, 2016.
[2] 彌永昌吉・彌永健一 , 集合と位相, 岩波基礎数学選書, 岩波書店, 2010.