ZFCカッコ仮

ssrzfc001.v

Require Import ssreflect ssrbool.

Axiom SET : Type.
Axiom membership : SET -> SET -> Prop.
Notation "x ∈ y" := (membership x y) (at level 100) : type_scope.

Axiom Extensionality : forall (x y: SET), (forall (z : SET), ((z ∈ x) <-> (z ∈ y))) <-> (x = y).

Axiom emptyset : SET.
Axiom EmptySetAxiom : (forall (z: SET), ~(z ∈ emptyset)).

Axiom pair : SET -> SET -> SET.
Notation "{ x , y }" := (pair x y) (at level 50) : type_scope.
Axiom PairingAxiom : forall (x y : SET), forall (z : SET), (z ∈ { x , y }) <-> (x = z) \/ (y = z).
Notation "{{ x }}" := (pair x x) (at level 49) : type_scope.

Axiom union : SET -> SET.
Notation "∪ x" := (union x) (at level 40) : type_scope.
Axiom UnionAxiom : forall (x : SET), forall (z : SET), (z ∈ (∪ x)) <-> (exists (y : SET), (z ∈ x) /\ (z ∈ y)).

Notation "x ∪ y" := (union (pair x y)) (at level 39) : type_scope.

Definition subset_of (x y : SET) : Prop :=
  forall (z : SET), (membership z x) -> (membership z y).
Notation "x ⊆ y" := (subset_of x y) (at level 101) : type_scope.


Axiom PowerSetAxiom : forall (x : SET), exists (y : SET), forall (z : SET), (z ⊆ x) -> (z ∈ y).

Axiom Comprehension : forall (phi : SET -> SET-> Prop), forall (param : SET), forall (x : SET), exists (y : SET), forall (z : SET), (z ∈ y) <-> (z ∈ x) /\ (phi z param).


Axiom ω : SET.
Definition inductive_set (x : SET) : Prop :=
  (emptyset ∈ x) /\ forall (y : SET), (y ∈ x) -> ((y ∪ {{ y }}) ∈ x).
Axiom InfinityAxiom : (inductive_set ω) /\ (forall (x : SET), (inductive_set x) -> (ω ⊆ x)).


Lemma 補題_0と1は異なる : ~(emptyset = {{ emptyset }}).
Proof.
  assert (emptyset ∈ {{emptyset}}) as H1.
  apply PairingAxiom.
  left; exact. (* assertion succeeded. *)
  assert (~(emptyset ∈ emptyset)) as H0.
  apply EmptySetAxiom. (* assertion succeeded. *)
  rewrite <- Extensionality.
  move => Habs.
  destruct H0.
  rewrite (Habs emptyset).
  exact.
Qed.