The Theory gst-ax
 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))

privacy policy

Created:

V