Sierpinski.Hartogs

Require Export Sierpinski.Ordinals.

Require Import Coq.Init.Nat.

Definition hartogs_number_as_class (A : S) :=
  build_class (fun x => x ∈ O /\ x <= A).

Lemma hartogs_number_as_class_has_upper_bound (A : S) :
  hartogs_number_as_class A <= iter 6 𝒫 A.
Proof.

  transitivity (𝒫 (encodings A)). {

    assert (forall x : hartogs_number_as_class A, x ∈ O). {
      intros (x & is_ordinal & ?). assumption.
    }

    set (f (x : hartogs_number_as_class A) :=
           `{ y in encodings A | decode y ≃ strict_well_order_on_ordinal (element x)}
           : 𝒫 (encodings A)).
    refine (inhabits (build_injection f _)).

    intros a b H1.
    enough (H2 : strict_well_order_on_ordinal (element a) ≃ strict_well_order_on_ordinal (element b)). {
      apply isomorphic_ordinals_are_equal in H2. apply element_equality in H2.
      apply element_equality. exact H2.
    }


    enough (r : inhabited (f a)). {
      destruct r as [r].

      refine (isomorphism_relation_transitivity _ (decode (element r)) _ _ _). {
        apply isomorphism_relation_symmetry. apply (comprehension_condition r).
      }
      assert (r ∈ f b). {
        rewrite <- H1. exact _.
      }
      set (r' := element r : f b).
      replace (element r : encodings A) with (element r' : encodings A). {
        exact (comprehension_condition r').
      }
      apply element_equality. reflexivity.
    } clear b H1.

    assert (H2 : (a : S) <= A). {
      assert (H3 : a ∈ hartogs_number_as_class A) by exact _.
      unfold In_Class in H3. cbn in H3. tauto.
    } destruct H2 as [g].
    apply inhabits.

    set (g_bij := injection_as_bijection_into_image g).

    unshelve eset (y := encode (transport_relation
                                  g_bij
                                  (strict_well_order_on_ordinal (element a)))).

    exists y. unfold f. rewrite in_comprehension_iff_typed.

    refine (isomorphism_relation_transitivity
              _ (transport_relation g_bij (strict_well_order_on_ordinal (element a))) _ _ _). {
      unfold y. apply decode_encode.
    }
    apply isomorphism_relation_symmetry.
    apply transported_relation_is_isomorphic.
  }



  change (𝒫 (𝒫 A × 𝒫 (A × A)) <= iter 6 𝒫 A).
  rewrite (symmetric_cartesian_product_is_increasing A) at 1.
  apply power_set_injection_mor.
  transitivity (𝒫 (𝒫 (𝒫 (A × A)))). {
    apply subset_subrelation_injection.
    apply cartesian_product_upper_bound.
  }
  repeat apply power_set_injection_mor.
  apply subset_subrelation_injection.
  apply cartesian_product_upper_bound.
Qed.

Corollary hartogs_number_as_class_is_a_set (A : S) :
  Is_A_Set (hartogs_number_as_class A).
Proof.
  eapply small_class_is_a_set. apply hartogs_number_as_class_has_upper_bound.
Qed.

Typeclasses eauto := 3.
Program Definition hartogs_number (A : S) : O :=
  element (class_as_set (hartogs_number_as_class A)
                        (hartogs_number_as_class_is_a_set A)).
Next Obligation.
  apply transitive_set_of_ordinals_is_ordinal.
  - intros x y Hx Hy; cbn in *.
    rewrite in_class_as_set_iff in *. unfold In_Class in *; cbn in *.
    destruct Hx as [x_is_ordinal x_leq_A].
    split.
    + refine (element_of_ordinal_is_ordinal (α := x) y); assumption.
    + rewrite <- x_leq_A.
      apply subset_subrelation_injection.
      intros z z_in_y. change (x ∈ O) in x_is_ordinal.
      apply (ordinal_is_transitive (element x) y); trivial.
  - intros [x H]; cbn.
    rewrite in_class_as_set_iff in H. unfold In_Class in H; cbn in H. tauto.
Qed.
Arguments hartogs_number : simpl never.
Typeclasses eauto := 5.

Lemma hartogs_number_is_not_smaller (A : S) :
  ~ (hartogs_number A : S) <= A.
Proof.
  intros H.
  assert (hartogs_number A ∈ hartogs_number A). {
    unfold hartogs_number at 2. unfold element_value at 2.
    rewrite in_class_as_set_iff.
    unfold In_Class; cbn.
    split.
    - exact _.
    - assumption.
  }
  pose no_set_contains_itself.
  firstorder.
Qed.

Lemma hartogs_number_has_upper_bound (A : S) :
  (hartogs_number A : S) <= iter 6 𝒫 A.
Proof.
  unfold hartogs_number. cbn.
  refine (injection_relation_transitivity _ (hartogs_number_as_class A) _ _ _). {
    destruct (class_as_set_equiv_set (hartogs_number_as_class A)
                                     (hartogs_number_as_class_is_a_set A))
      as [f].
    exact (inhabits (bijection_to_injection f)).
  }
  apply hartogs_number_as_class_has_upper_bound.
Qed.