The Theory ord
 Parents
 wf_recp gst-ax
 Children
 gst
 Constants
 connected GS → BOOL ordinal GS → BOOL \$
 Fixity
 Right Infix 240:
 Definitions
 connected ⊢ ∀ s • connected s ⇔ (∀ t u • t ∈g s ∧ u ∈g s ⇒ t ∈g u ∨ t = u ∨ u ∈g t) ordinal ⊢ ∀ s• ordinal s ⇔ transitive s ∧ connected s
 Theorems
 ordinal_∅g ⊢ ordinal ∅g trans_suc_trans ⊢ ∀ x• transitive x ⇒ transitive (suco x) conn_suc_conn ⊢ ∀ x• connected x ⇒ connected (suco x) ord_suc_ord_thm ⊢ ∀ x• ordinal x ⇒ ordinal (suco x) conn_sub_conn ⊢ ∀ x• connected x ⇒ (∀ y• y ⊆g x ⇒ connected y) conn_mem_ord ⊢ ∀ x• ordinal x ⇒ (∀ y• y ∈g x ⇒ connected y) wf_l1 ⊢ ∀ x• ¬ x ∈g x wf_l2 ⊢ ∀ x y• ¬ (x ∈g y ∧ y ∈g x) wf_l3 ⊢ ∀ x y z• ¬ (x ∈g y ∧ y ∈g z ∧ z ∈g x) tran_mem_ord ⊢ ∀ x• ordinal x ⇒ (∀ y• y ∈g x ⇒ transitive y) ord_mem_ord ⊢ ∀ x• ordinal x ⇒ (∀ y• y ∈g x ⇒ ordinal y) GCloseSuco ⊢ ∀ g x• galaxy g ∧ x ∈g g ⇒ suco x ∈g g tran_∩_thm ⊢ ∀ x y • transitive x ∧ transitive y ⇒ transitive (x ∩g y) tran_∪_thm ⊢ ∀ x y • transitive x ∧ transitive y ⇒ transitive (x ∪g y) conn_∩_thm ⊢ ∀ x y • connected x ∧ connected y ⇒ connected (x ∩g y) ord_∩_thm ⊢ ∀ x y• ordinal x ∧ ordinal y ⇒ ordinal (x ∩g y) trich_for_ords_thm ⊢ ∀ x y • ordinal x ∧ ordinal y ⇒ x