The Theory ord

Parents

wf_recp

gst-ax

Children

gst

Constants

connected	GS → BOOL
ordinal	GS → BOOL
$<_o	GS → GS → BOOL
$≤_o	GS → GS → BOOL
suc_o	GS → GS
successor	GS → BOOL
limit_ordinal	GS → BOOL
natural_number	GS → BOOL
$<_g_n	GS → GS → BOOL
rank	GS → GS

Fixity

Right Infix 240:

<_g_n

<_o

≤_o

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
<_o	⊢ ∀ x y• x <_o y ⇔ ordinal x ∧ ordinal y ∧ x ∈_g y
≤_o	⊢ ∀ x y • x ≤_o y ⇔ ordinal x ∧ ordinal y ∧ x ∈_g y ∨ x = y
suc_o	⊢ ∀ x• suc_o x = x ∪_g Unit x
successor	⊢ ∀ s• successor s ⇔ (∃ t• ordinal t ∧ s = suc_o t)
limit_ordinal	⊢ ∀ s • limit_ordinal s ⇔ ordinal s ∧ ¬ successor s ∧ ¬ s = ∅_g
natural_number	⊢ ∀ s • natural_number s ⇔ s = ∅_g ∨ successor s ∧ (∀ t• t ∈_g s ⇒ t = ∅_g ∨ successor t)
<_g_n	⊢ ∀ x y • x <_g_n y ⇔ natural_number x ∧ natural_number y ∧ x ∈_g y
rank	⊢ ∀ x• rank x = ⋃_g (Imagep (suc_o o rank) x)

Theorems

ordinal_∅_g	⊢ ordinal ∅_g
trans_suc_trans	⊢ ∀ x• transitive x ⇒ transitive (suc_o x)
conn_suc_conn	⊢ ∀ x• connected x ⇒ connected (suc_o x)
ord_suc_ord_thm	⊢ ∀ x• ordinal x ⇒ ordinal (suc_o 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)
GCloseSuc_o	⊢ ∀ g x• galaxy g ∧ x ∈_g g ⇒ suc_o 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 <_o y ∨ x = y ∨ y <_o x
successor_ord_thm	⊢ ∀ x• successor x ⇒ ordinal x
wf_ordinals_thm	⊢ well_founded $<_o
wf_nat_thm	⊢ well_founded $<_g_n
nat_induct_thm	⊢ ∀ s• (∀ x• (∀ y• y <_g_n x ⇒ s y) ⇒ s x) ⇒ (∀ x• s x)
nat_induct_thm2	⊢ ∀ p • (∀ x • natural_number x ∧ (∀ y• y <_g_n x ⇒ p y) ⇒ p x) ⇒ (∀ x• natural_number x ⇒ p x)
ord_nat_thm	⊢ ∀ n• natural_number n ⇒ ordinal n
mem_nat_ord_thm	⊢ ∀ n• natural_number n ⇒ (∀ m• m ∈_g n ⇒ ordinal m)
ordinal_kind_thm	⊢ ∀ n • ordinal n ⇒ n = ∅_g ∨ successor n ∨ limit_ordinal n
nat_not_lim_thm	⊢ ∀ n• natural_number n ⇒ ¬ limit_ordinal n
nat_zero_or_suc_thm	⊢ ∀ n• natural_number n ⇒ successor n ∨ n = ∅_g
mem_not_empty_thm	⊢ ∀ m n• m ∈_g n ⇒ ¬ n = ∅_g
mem_nat_not_lim_thm	⊢ ∀ m n• natural_number n ∧ m ∈_g n ⇒ ¬ limit_ordinal m
mem_nat_nat_thm	⊢ ∀ n • natural_number n ⇒ (∀ m• m ∈_g n ⇒ natural_number m)
GCloseSuc	⊢ ∀ g• galaxy g ⇒ (∀ x• x ∈_g g ⇒ suc_o x ∈_g g)
nat_in_G∅_g_thm	⊢ ∀ n• natural_number n ⇒ n ∈_g Gx ∅_g
w_exists_thm	⊢ ∃ w• ∀ z• z ∈_g w ⇔ natural_number z

Created: