| Parents |
| wf_relp | basic_hol |
| Constants |
|
$∈g
|
GS → GS → BOOL |
|
$⊆g
|
GS → GS → BOOL |
|
ManyOne
|
('a → 'b → BOOL) → BOOL |
|
℘g
|
GS → GS |
|
⋃g
|
GS → GS |
|
RelIm
|
(GS → GS → BOOL) → GS → GS |
|
Sep
|
GS → (GS → BOOL) → GS |
|
galaxy
|
GS → BOOL |
|
Gx
|
GS → GS |
|
transitive
|
GS → BOOL |
|
∅g
|
GS |
|
Imagep
|
(GS → GS) → GS → GS |
|
Pairg
|
GS → GS → GS |
|
Unit
|
GS → GS |
|
$∪g
|
GS → GS → GS |
|
⋂g
|
GS → GS |
|
$∩g
|
GS → GS → GS |
| Types |
|
GS
|
| Fixity |
| Right Infix 230: |
⊆g | ∈g |
Right Infix 240: |
∩g | ∪g |
| Axioms |
|
gs_ext_axiom
|
⊢ ∀ s t• s = t ⇔ (∀ e• e ∈g s ⇔ e ∈g t) |
|
gs_wf_axiom
|
⊢ well_founded $∈g |
|
Ontology_axiom
|
⊢ ∀ s
 • ∃ g • s ∈g g ∧ (∀ t • t ∈g g ⇒ t ⊆g g ∧ (∃ p • (∀ v• v ∈g p ⇔ v ⊆g t) ∧ p ∈g g) ∧ (∃ u • (∀ v • v ∈g u ⇔ (∃ w• v ∈g w ∧ w ∈g t)) ∧ u ∈g g) ∧ (∀ rel • ManyOne rel ⇒ (∃ r • (∀ v • v ∈g r ⇔ (∃ w• w ∈g t ∧ rel w v)) ∧ (r ⊆g g ⇒ r ∈g g))))
|
| Definitions |
|
⊆g
|
⊢ ∀ s t• s ⊆g t ⇔ (∀ e• e ∈g s ⇒ e ∈g t) |
|
ManyOne
|
⊢ ∀ r• ManyOne r ⇔ (∀ x y z• r x y ∧ r x z ⇒ y = z) |
|
℘g
|
⊢ ∀ s t• t ∈g ℘g s ⇔ t ⊆g s |
|
⋃g
|
⊢ ∀ s t• t ∈g ⋃g s ⇔ (∃ e• t ∈g e ∧ e ∈g s) |
|
RelIm
|
⊢ ∀ rel s t • ManyOne rel ⇒ (t ∈g RelIm rel s ⇔ (∃ e• e ∈g s ∧ rel e t))
|
|
Sep
|
⊢ ∀ s p e• e ∈g Sep s p ⇔ e ∈g s ∧ p e |
|
galaxy
|
⊢ ∀ s • galaxy s ⇔ (∃ x• x ∈g s) ∧ (∀ t • t ∈g s ⇒ t ⊆g s ∧ ℘g t ∈g s ∧ ⋃g t ∈g s ∧ (∀ rel • ManyOne rel ⇒ RelIm rel t ⊆g s ⇒ RelIm rel t ∈g s))
|
|
Gx
|
⊢ ∀ s t • t ∈g Gx s ⇔ (∀ g• galaxy g ∧ s ∈g g ⇒ t ∈g g)
|
|
transitive
|
⊢ ∀ s• transitive s ⇔ (∀ e• e ∈g s ⇒ e ⊆g s) |
|
∅g
|
⊢ ∀ s• ¬ s ∈g ∅g |
|
Imagep
|
⊢ ∀ f s x• x ∈g Imagep f s ⇔ (∃ e• e ∈g s ∧ x = f e) |
|
Pairg
|
⊢ ∀ s t e• e ∈g Pairg s t ⇔ e = s ∨ e = t |
|
Unit
|
⊢ ∀ s• Unit s = Pairg s s |
|
∪g
|
⊢ ∀ s t e• e ∈g s ∪g t ⇔ e ∈g s ∨ e ∈g t |
|
⋂g
|
⊢ ∀ s • ⋂g s = Sep (⋃g s) (λ x• ∀ t• t ∈g s ⇒ x ∈g t)
|
|
∩g
|
⊢ ∀ s t• s ∩g t = Sep s (λ x• x ∈g t) |
| Theorems |
|
gs_wf_min_thm
|
⊢ ∀ x
• (∃ y• y ∈g x) ⇒ (∃ z• z ∈g x ∧ ¬ (∃ v• v ∈g z ∧ v ∈g x))
|
|
gs_wf_ind_thm
|
⊢ ∀ s• (∀ x• (∀ y• y ∈g x ⇒ s y) ⇒ s x) ⇒ (∀ x• s x) |
|
⊆g_eq_thm
|
⊢ ∀ A B• A = B ⇔ A ⊆g B ∧ B ⊆g A |
|
⊆g_refl_thm
|
⊢ ∀ A• A ⊆g A |
|
∈g⊆g_thm
|
⊢ ∀ e A B• e ∈g A ∧ A ⊆g B ⇒ e ∈g B |
|
⊆g_trans_thm
|
⊢ ∀ A B C• A ⊆g B ∧ B ⊆g C ⇒ A ⊆g C |
|
∈g⋃g_thm
|
⊢ ∀ s t• t ∈g s ⇒ t ⊆g ⋃g s |
|
galaxies_∃_thm
|
⊢ ∀ s• ∃ g• s ∈g g ∧ galaxy g |
|
t_in_Gx_t_thm
|
⊢ ∀ t• t ∈g Gx t |
|
Gx_⊆g_galaxy
|
⊢ ∀ s g• galaxy g ∧ s ∈g g ⇒ Gx s ⊆g g |
|
galaxy_Gx
|
⊢ ∀ s• galaxy (Gx s) |
|
GalaxiesTransitive_thm
|
⊢ ∀ s• galaxy s ⇒ transitive s |
|
GCloseSep
|
⊢ ∀ g• galaxy g ⇒ (∀ s• s ∈g g ⇒ (∀ p• Sep s p ∈g g)) |
|
Gx_transitive_thm
|
⊢ ∀ s• transitive (Gx s) |
|
Gx_mono_thm
|
⊢ ∀ s t• s ⊆g t ⇒ Gx s ⊆g Gx t |
|
Gx_mono_thm2
|
⊢ ∀ s t• s ∈g t ⇒ Gx s ⊆g Gx t |
|
t_sub_Gx_t_thm
|
⊢ ∀ t• t ⊆g Gx t |
|
Gx_mono_thm3
|
⊢ ∀ s t• s ⊆g t ⇒ s ⊆g Gx t |
|
Gx_trans_thm2
|
⊢ ∀ s t• s ∈g t ⇒ s ∈g Gx t |
|
Gx_trans_thm3
|
⊢ ∀ s t u• s ∈g t ∧ t ∈g Gx u ⇒ s ∈g Gx u |
|
G∅gC
|
⊢ ∀ g• galaxy g ⇒ ∅g ∈g g |
|
∅g⊆g_thm
|
⊢ ∀ s• ∅g ⊆g t |
|
⋃g∅g_thm
|
⊢ ⋃g ∅g = ∅g |
|
GImagepC
|
⊢ ∀ g • galaxy g ⇒ (∀ s • s ∈g g ⇒ (∀ f• Imagep f s ⊆g g ⇒ Imagep f s ∈g g))
|
|
Pairg_eq_thm
|
⊢ ∀ s t u v
• Pairg s t = Pairg u v ⇔ s = u ∧ t = v ∨ s = v ∧ t = u
|
|
GClosePairg
|
⊢ ∀ g • galaxy g ⇒ (∀ s t• s ∈g g ∧ t ∈g g ⇒ Pairg s t ∈g g)
|
|
GCloseUnit
|
⊢ ∀ g• galaxy g ⇒ (∀ s• s ∈g g ⇒ Unit s ∈g g) |
|
⊆g∪g_thm
|
⊢ ∀ A B• A ⊆g A ∪g B ∧ B ⊆g A ∪g B |
|
∪g⊆g_thm1
|
⊢ ∀ A B C• A ⊆g C ∧ B ⊆g C ⇒ A ∪g B ⊆g C |
|
∪g⊆g_thm2
|
⊢ ∀ A B C D• A ⊆g C ∧ B ⊆g D ⇒ A ∪g B ⊆g C ∪g D |
|
∪g∅g_clauses
|
⊢ ∀ A• A ∪g ∅g = A ∧ ∅g ∪g A = A |
|
GClose∪g
|
⊢ ∀ g • galaxy g ⇒ (∀ s t• s ∈g g ∧ t ∈g g ⇒ s ∪g t ∈g g)
|
|
⋂g_thm
|
⊢ ∀ x s e • x ∈g s ⇒ (e ∈g ⋂g s ⇔ (∀ y• y ∈g s ⇒ e ∈g y))
|
|
⋂g⊆g_thm
|
⊢ ∀ s t• s ∈g t ⇒ ⋂g t ⊆g s |
|
⊆g⋂g_thm
|
⊢ ∀ A B • A ∈g B ⇒ (∀ C• (∀ D• D ∈g B ⇒ C ⊆g D) ⇒ C ⊆g ⋂g B)
|
|
⋂g∅g_thm
|
⊢ ⋂g ∅g = ∅g |
|
GClose⋂g
|
⊢ ∀ g• galaxy g ⇒ (∀ s• s ∈g g ⇒ ⋂g s ∈g g) |
|
GClose∩g
|
⊢ ∀ g • galaxy g ⇒ (∀ s t• s ∈g g ∧ t ∈g g ⇒ s ∩g t ∈g g)
|
|
∩g_thm
|
⊢ ∀ s t e• e ∈g s ∩g t ⇔ e ∈g s ∧ e ∈g t |
|
⊆g∩g_thm
|
⊢ ∀ A B• A ∩g B ⊆g A ∧ A ∩g B ⊆g B |
|
∩g⊆g_thm1
|
⊢ ∀ A B C• A ⊆g C ∧ B ⊆g C ⇒ A ∩g B ⊆g C |
|
∩g⊆g_thm2
|
⊢ ∀ A B C D• A ⊆g C ∧ B ⊆g D ⇒ A ∩g B ⊆g C ∩g D |
|
∩g⊆g_thm3
|
⊢ ∀ A B C• C ⊆g A ∧ C ⊆g B ⇒ C ⊆g A ∩g B |
|
gst_opext_clauses
|
⊢ ∀ s t x f u v e p
• ¬ s ∈g ∅g ∧ (t ∈g ℘g s ⇔ t ⊆g s) ∧ (t ∈g ⋃g s ⇔ (∃ e• t ∈g e ∧ e ∈g s)) ∧ (x ∈g Imagep f s ⇔ (∃ e• e ∈g s ∧ x = f e)) ∧ (Pairg s t = Pairg u v ⇔ s = u ∧ t = v ∨ s = v ∧ t = u) ∧ (e ∈g Pairg s t ⇔ e = s ∨ e = t) ∧ (Unit s = Unit t ⇔ s = t) ∧ (e ∈g Unit s ⇔ e = s) ∧ (Pairg s t = Unit u ⇔ s = u ∧ t = u) ∧ (Unit s = Pairg t u ⇔ s = t ∧ s = u) ∧ (e ∈g Sep s p ⇔ e ∈g s ∧ p e) ∧ (e ∈g s ∪g t ⇔ e ∈g s ∨ e ∈g t) ∧ (e ∈g s ∩g t ⇔ e ∈g s ∧ e ∈g t)
|
|
gst_relext_clauses
|
⊢ ∀ s t
• (s = t ⇔ (∀ e• e ∈g s ⇔ e ∈g t)) ∧ (s ⊆g t ⇔ (∀ e• e ∈g s ⇒ e ∈g t))
|
