Library Continuum.Hartogs_Number

Require Export Continuum.Ordinals.

Require Import Coq.Init.Nat.

Definition hartogs_number_as_class (A : S) :=
  build_class (fun x ⇒ Is_Ordinal x ∧ 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 (∀ x : hartogs_number_as_class A, x ∈ Ordinal). {
      intros (x & is_ordinal & ?). assumption.
    }

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

    intros a b H1.
    enough (H2 : ordinal_order (element a) ≃ ordinal_order (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
                                  (ordinal_order (element a)))).

    ∃ y. unfold f. rewrite in_comprehension_iff_typed.

    refine (isomorphism_relation_transitivity
              _ (transport_relation g_bij (ordinal_order (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.
  rewrite cartesian_product_upper_bound.
  rewrite cartesian_product_upper_bound.
  reflexivity.
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 := 5.
Program Definition hartogs_number (A : S) : Ordinal :=
  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 H]; cbn.
    rewrite in_class_as_set_iff in H. unfold In_Class in H; cbn in H. tauto.
  - intros [x H] y; cbn in ×. rewrite in_class_as_set_iff in ×.
    unfold In_Class in *; cbn in ×.
    destruct H as [x_is_ordinal x_leq_A].
    split.
    + apply (element_of_ordinal_is_ordinal x y _ _).
    + rewrite <- x_leq_A.
      erewrite (element_of_ordinal_is_subset x y); try exact _.
      reflexivity.
Qed.
Arguments hartogs_number : simpl never.

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.