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
suco
GS → GS
successor
GS → BOOL
limit_ordinal
GS → BOOL
natural_number
GS → BOOL
$<gn
GS → GS → BOOL
rank
GS → GS
Fixity
Right Infix 240:
<gn <o o
Definitions
connected
⊢ ∀ s
fill• connected s
fill⇔ (∀ t u
fill• 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
fill• x ≤o y ⇔ ordinal x ∧ ordinal y ∧ x ∈g y ∨ x = y
suco
⊢ ∀ x• suco x = x ∪g Unit x
successor
⊢ ∀ s• successor s ⇔ (∃ t• ordinal t ∧ s = suco t)
limit_ordinal
⊢ ∀ s
fill• limit_ordinal s
fill⇔ ordinal s ∧ ¬ successor s ∧ ¬ s = ∅g
natural_number
⊢ ∀ s
fill• natural_number s
fill⇔ s = ∅g
fill∨ successor s
fill∧ (∀ t• t ∈g s ⇒ t = ∅g ∨ successor t)
<gn
⊢ ∀ x y
fill• x <gn y
fill⇔ natural_number x ∧ natural_number y ∧ x ∈g y
rank
⊢ ∀ x• rank x = ⋃g (Imagep (suco o rank) x)
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
fill• transitive x ∧ transitive y ⇒ transitive (x ∩g y)
tran_∪_thm
⊢ ∀ x y
fill• transitive x ∧ transitive y ⇒ transitive (x ∪g y)
conn_∩_thm
⊢ ∀ x y
fill• 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
fill• 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 $<gn
nat_induct_thm
⊢ ∀ s• (∀ x• (∀ y• y <gn x ⇒ s y) ⇒ s x) ⇒ (∀ x• s x)
nat_induct_thm2
⊢ ∀ p
fill• (∀ x
fill• natural_number x ∧ (∀ y• y <gn x ⇒ p y)
fill⇒ p x)
fill⇒ (∀ 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
fill• 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
fill• natural_number n
fill⇒ (∀ m• m ∈g n ⇒ natural_number m)
GCloseSuc
⊢ ∀ g• galaxy g ⇒ (∀ x• x ∈g g ⇒ suco 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

up quick index

privacy policy

Created:

V