(* Modern local reconstruction of the semantic content of PM *54.43.
   This does not formalize PM's ramified type theory or class machinery.
   Only the default Rocq prelude; no imports, Classical, choice, or axioms. *)
Set Implicit Arguments.
Section PrincipiaProof.
Context {X : Type}.

Definition EqualSets (S T : X -> Prop) : Prop := forall z, S z <-> T z.
Definition Singleton (a : X) : X -> Prop := fun z => z = a.
Definition One (S : X -> Prop) : Prop := exists a, EqualSets S (Singleton a).
Definition Two (S : X -> Prop) : Prop :=
  exists a b, a <> b /\ forall z, S z <-> (z = a \/ z = b).
Definition Union (S T : X -> Prop) : X -> Prop := fun z => S z \/ T z.
Definition Disjoint (S T : X -> Prop) : Prop :=
  forall z, S z -> T z -> False.

(* Semantic analogue of *51.231. *)
Theorem singleton_disjoint_iff_distinct (a b : X) :
  Disjoint (Singleton a) (Singleton b) <-> a <> b.
Proof.
  split.
  - intros h hab. exact (h a eq_refl hab).
  - intros hab z hza hzb. apply hab.
    exact (eq_trans (eq_sym hza) hzb).
Qed.

(* Semantic analogue of *54.26. *)
Theorem singleton_union_two_iff_distinct (a b : X) :
  Two (Union (Singleton a) (Singleton b)) <-> a <> b.
Proof.
  split.
  - intros [c [d [hcd hm]]] hab.
    assert (hc : c = a).
    { destruct (proj2 (hm c) (or_introl eq_refl)) as [hca | hcb].
      - exact hca.
      - exact (eq_trans hcb (eq_sym hab)). }
    assert (hd : d = a).
    { destruct (proj2 (hm d) (or_intror eq_refl)) as [hda | hdb].
      - exact hda.
      - exact (eq_trans hdb (eq_sym hab)). }
    exact (hcd (eq_trans hc (eq_sym hd))).
  - intro hab. exists a, b. split.
    + exact hab.
    + intro z. unfold Union, Singleton. split; intro h; exact h.
Qed.

Theorem disjoint_congr (S T A B : X -> Prop)
  (hS : EqualSets S A) (hT : EqualSets T B) :
  Disjoint S T <-> Disjoint A B.
Proof.
  split.
  - intros h z hA hB.
    exact (h z (proj2 (hS z) hA) (proj2 (hT z) hB)).
  - intros h z hS' hT'.
    exact (h z (proj1 (hS z) hS') (proj1 (hT z) hT')).
Qed.

Theorem union_congr (S T A B : X -> Prop)
  (hS : EqualSets S A) (hT : EqualSets T B) :
  EqualSets (Union S T) (Union A B).
Proof.
  intro z. split.
  - intros [h | h].
    + left. exact (proj1 (hS z) h).
    + right. exact (proj1 (hT z) h).
  - intros [h | h].
    + left. exact (proj2 (hS z) h).
    + right. exact (proj2 (hT z) h).
Qed.

Theorem two_congr (S T : X -> Prop) (hST : EqualSets S T) :
  Two S <-> Two T.
Proof.
  split.
  - intros [a [b [hab hm]]]. exists a, b. split.
    + exact hab.
    + intro z. split.
      * intro ht. exact (proj1 (hm z) (proj2 (hST z) ht)).
      * intro hz. exact (proj1 (hST z) (proj2 (hm z) hz)).
  - intros [a [b [hab hm]]]. exists a, b. split.
    + exact hab.
    + intro z. split.
      * intro hs. exact (proj1 (hm z) (proj1 (hST z) hs)).
      * intro hz. exact (proj2 (hST z) (proj2 (hm z) hz)).
Qed.

(* Eliminate the given singleton witnesses within Prop. *)
Theorem pm_54_43 (S T : X -> Prop) :
  One S -> One T -> (Disjoint S T <-> Two (Union S T)).
Proof.
  intros [a hSa] [b hTb].
  pose proof (disjoint_congr hSa hTb) as hd.
  pose proof (two_congr (union_congr hSa hTb)) as ht.
  split.
  - intro h. apply (proj2 ht).
    apply (proj2 (singleton_union_two_iff_distinct a b)).
    apply (proj1 (singleton_disjoint_iff_distinct a b)).
    exact (proj1 hd h).
  - intro h. apply (proj2 hd).
    apply (proj2 (singleton_disjoint_iff_distinct a b)).
    apply (proj1 (singleton_union_two_iff_distinct a b)).
    exact (proj1 ht h).
Qed.

(* Checked negative control: coincident singletons cannot have two members. *)
Theorem equal_singletons_not_two (a : X) :
  ~ Two (Union (Singleton a) (Singleton a)).
Proof.
  intro h.
  exact (proj1 (singleton_union_two_iff_distinct a a) h eq_refl).
Qed.
End PrincipiaProof.

Set Printing All Assumptions.
Print Typing Flags.
Print Assumptions singleton_disjoint_iff_distinct.
Print Assumptions singleton_union_two_iff_distinct.
Print Assumptions disjoint_congr.
Print Assumptions union_congr.
Print Assumptions two_congr.
Print Assumptions pm_54_43.
Print Assumptions equal_singletons_not_two.