|
↦g
|
⊢ ∀ s t u v
 • (s ↦g t = u ↦g v ⇔ s = u ∧ t = v)
∧ Pairg s t ∈g Gx (s ↦g t)
|
|
fst
snd
|
⊢ ∀ s t• fst (s ↦g t) = s ∧ snd (s ↦g t) = t
|
|
×g
|
⊢ ∀ s t e
• e ∈g s ×g t
⇔ (∃ l r• l ∈g s ∧ r ∈g t ∧ e = l ↦g r)
|
|
↔g
|
⊢ ∀ s t• s ↔g t = ℘g (s ×g t)
|
|
rel
|
⊢ ∀ x• rel x ⇔ (∀ y• y ∈g x ⇒ (∃ s t• y = s ↦g t))
|
|
og
|
⊢ ∀ f g
• f og g
= Imagep
(λ p• fst (fst p) ↦g snd (snd p))
(Sep
(g ×g f)
(λ p• ∃ q r s• p = (q ↦g r) ↦g r ↦g s))
|
|
dom
|
⊢ ∀ x• dom x = Sep (Gx x) (λ w• ∃ v• w ↦g v ∈g x)
|
|
ran
|
⊢ ∀ x• ran x = Sep (Gx x) (λ w• ∃ v• v ↦g w ∈g x)
|
|
field
|
⊢ ∀ s e• e ∈g field s ⇔ e ∈g dom s ∨ e ∈g ran s
|
|
fun
|
⊢ ∀ x
• fun x
⇔ rel x
∧ (∀ s t u
• s ↦g u ∈g x ∧ s ↦g t ∈g x ⇒ u = t)
|
|
g
|
⊢ ∀ s t• s g t = Sep (s ↔g t) fun
|
|
→g
|
⊢ ∀ s t• s →g t = Sep (s g t) (λ r• dom r = s)
|
|
λg
|
⊢ ∀ f s
• $λg f s
= Sep (s ×g Imagep f s) (λ p• snd p = f (fst p))
|
|
g
|
⊢ ∀ f x
• f g x
= (if ∃ y• x ↦g y ∈g f
then ε y• x ↦g y ∈g f
else f)
|
|
id
|
⊢ ∀ s• id s = Sep (s ×g s) (λ x• fst x = snd x)
|
|
f↦gs_thm
|
⊢ ∀ s t p• p ∈g s ×g t ⇒ fst p ↦g snd p = p
|
|
v∈g×g_thm
|
⊢ ∀ p s t• p ∈g s ×g t ⇒ fst p ∈g s ∧ snd p ∈g t
|
|
↦g∈g×g_thm
|
⊢ ∀ l r s t• l ↦g r ∈g s ×g t ⇔ l ∈g s ∧ r ∈g t
|
|
↔g⊆g×g_thm
|
⊢ ∀ s t r• r ∈g s ↔g t ⇔ r ⊆g s ×g t
|
|
∅g∈g↔g_thm
|
⊢ ∀ s t• ∅g ∈g s ↔g t
|
|
f↦gs_thm1
|
⊢ ∀ p r s t
• p ∈g r ∧ r ∈g s ↔g t ⇒ fst p ↦g snd p = p
|
|
∈g↔g_thm
|
⊢ ∀ p r s t
• p ∈g r ∧ r ∈g s ↔g t ⇒ fst p ∈g s ∧ snd p ∈g t
|
|
rel_∅g_thm
|
⊢ rel ∅g
|
|
og_thm
|
⊢ ∀ f g x
• x ∈g f og g
⇔ (∃ q r s
• q ↦g r ∈g g ∧ r ↦g s ∈g f ∧ x = q ↦g s)
|
|
og_thm2
|
⊢ ∀ f g x y
• x ↦g y ∈g f og g
⇔ (∃ z• x ↦g z ∈g g ∧ z ↦g y ∈g f)
|
|
og_rel_thm
|
⊢ ∀ r s• rel r ∧ rel s ⇒ rel (r og s)
|
|
og_associative_thm
|
⊢ ∀ f g h• (f og g) og h = f og g og h
|
|
dom_∅g_thm
|
⊢ dom ∅g = ∅g
|
|
dom_thm
|
⊢ ∀ r y• y ∈g dom r ⇔ (∃ x• y ↦g x ∈g r)
|
|
ran_∅g_thm
|
⊢ ran ∅g = ∅g
|
|
ran_thm
|
⊢ ∀ r y• y ∈g ran r ⇔ (∃ x• x ↦g y ∈g r)
|
|
rel_sub_cp_thm
|
⊢ ∀ x• rel x ⇔ (∃ s t• x ⊆g s ×g t)
|
|
field_∅g_thm
|
⊢ field ∅g = ∅g
|
|
fun_∅g_thm
|
⊢ fun ∅g
|
|
og_fun_thm
|
⊢ ∀ f g• fun f ∧ fun g ⇒ fun (f og g)
|
|
ran_og_thm
|
⊢ ∀ f g• ran (f og g) ⊆g ran f
|
|
dom_og_thm
|
⊢ ∀ f g• dom (f og g) ⊆g dom g
|
|
dom_og_thm2
|
⊢ ∀ f g• ran g ⊆g dom f ⇒ dom (f og g) = dom g
|
|
∅g∈gg_thm
|
⊢ ∀ s t• ∅g ∈g s g t
|
|
∃g_thm
|
⊢ ∀ s t• ∃ f• f ∈g s g t
|
|
∅g∈g∅g→g_thm
|
⊢ ∀ s t• ∅g ∈g ∅g →g t
|
|
∃→g_thm
|
⊢ ∀ s t• (∃ x• x ∈g t) ⇒ (∃ f• f ∈g s →g t)
|
|
app_thm1
|
⊢ ∀ f x• (∃1 y• x ↦g y ∈g f) ⇒ x ↦g f g x ∈g f
|
|
app_thm2
|
⊢ ∀ f x y• fun f ∧ x ↦g y ∈g f ⇒ f g x = y
|
|
app_thm3
|
⊢ ∀ f x• fun f ∧ x ∈g dom f ⇒ x ↦g f g x ∈g f
|
|
og_g_thm
|
⊢ ∀ f g x
• fun f ∧ fun g ∧ x ∈g dom g ∧ ran g ⊆g dom f
⇒ (f og g) g x = f g g g x
|
|
g∈g_thm
|
⊢ ∀ f s t u• f ∈g s g t ∧ u ∈g dom f ⇒ f g u ∈g t
|
|
g∈g_thm1
|
⊢ ∀ f s t u• f ∈g s →g t ∧ u ∈g s ⇒ f g u ∈g t
|
|
∈gg⇒∈g→g_thm
|
⊢ ∀ f s t u• f ∈g s g t ⇒ f ∈g dom f →g t
|
|
id_thm1
|
⊢ ∀ s x• x ∈g id s ⇔ (∃ y• y ∈g s ∧ x = y ↦g y)
|
|
id_ap_thm
|
⊢ ∀ s x• x ∈g s ⇒ id s g x = x
|
|
id∈gg_thm1
|
⊢ ∀ s t u• s ⊆g t ∩g u ⇒ id s ∈g t g u
|
|
id∈gg_thm2
|
⊢ ∀ s t u• s ⊆g t ⇒ id s ∈g t g t
|
|
id_clauses
|
⊢ ∀ s
• rel (id s)
∧ fun (id s)
∧ dom (id s) = s
∧ ran (id s) = s
|
