Commit 1ebd8412 authored by Sven Wille's avatar Sven Wille

zftrash2

parent 504dac78
......@@ -75,13 +75,18 @@ theory Union : fnd:?Logic =
theory Replacement : fnd:?Logic =
include ?preAxioms ❙
include fnd:?DescriptionOperator ❙
include fnd:?NaturalDeduction ❙
axiom_schema_replacement : {E : set ⟶ set ⟶ prop} ⊦ ∀[x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z) ⇒ ∀[A] ∃[M] ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ A ∧ E x y)) ❙
lemma_schema_replacement_alt : {E : set ⟶ set ⟶ prop} ⊦ ∀[A] ∃[M] ( ∀[x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z) ⇒ ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ A ∧ E x y)) ) ❙ // this is valid in classical logic ❙
theorem_schema_replacement_alt_is_unique : {E : set ⟶ set ⟶ prop} ⊦ ∀[A] ∃![M] ( ∀[x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z) ⇒ ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ A ∧ E x y)) ) ❙
theorem_schema_replacement_unique : {E : set ⟶ set ⟶ prop} ⊦ (∀[x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z)) ⇒ (∀[A] ∃![M] ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ A ∧ E x y))) ❘ # theorem_schema_replacement_unique 1 ❙
replacePropProp : (set ⟶ set ⟶ prop) ⟶ prop ❘ = [E] (∀ [x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z)) ❘ # replacePropProp 1❙
replace : set ⟶ (set ⟶ set ⟶ prop) ⟶ set ❘ = [s,p]
replace : set ⟶ {E : set ⟶ set ⟶ prop} ⊦ (∀ [x] ∀[y] ∀[z] (E x y ∧ E x z ⇒ y ≐ z)) ⟶ set ❘ = [s,E,h] that set ([M] ∀[y] (y ∈ M ⇔ ∃ [x] (x ∈ s ∧ E x y))) (forallE (impE h (theorem_schema_replacement_unique E) ) s)
......
namespace http://mathhub.info/MitM/smglom/other_foundations/mmt_tg ❚
import fnd http://mathhub.info/MitM/Foundation ❚
theory collect : fnd:?Logic =
include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?preAxioms ❙
axiom_scheme_collection : {E : set ⟶ set ⟶ prop} ⊦ (∀ [x] ∃ [y] E x y ) ⇒ ∀ [A] ∃[B] ∀ [x] x ∈ A ⇒ ∃ [y] y ∈ B ⇒ E x y ❙
// this is not 100% related to the actual axiom. This is more of a helper function ❚
theory collectionFilter : fnd:?Logic =
include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?ZFC_Base ❙
colProp : (set ⟶ prop ) ⟶ set ⟶ set ⟶ prop ❘ = [E] ([x,y] x ≐ y ∧ E x) ❙
lemma_colProp_inj : {E : set ⟶ prop} ⊦ (∀ [x] ∀ [y] ∀ [z] colProp E x y ∧ colProp E x z ⇒ y ≐ z) ❘ # lemma_colProp_inj 1❙
collect : set ⟶ (set ⟶ prop) ⟶ set ❘= [s,E] replace s (colProp E) (lemma_colProp_inj E)❙
\ No newline at end of file
......@@ -7,5 +7,7 @@ import fnd http://mathhub.info/MitM/Foundation ❚
theory the_descriptor : fnd:?Logic =
include http://mathhub.info/MitM/smglom/other_foundations/mmt_tg?ZFC_Base ❙
the : (set ⟶ prop) ⟶ set ❘ = [p] ⋃ (⟪ | ⟫) ❙
thePropInj : {p : set ⟶ prop} {h : ⊦ ∃![y] p y} ⊦ (replacePropProp ([x : set ] [z : set ] p z )) ❘ # thePropInj 1 2 ❙
the : {p :set ⟶ prop} ⊦ (∃! [y] p y) ⟶ set ❘ = [p,h] ⋃ (replace (singleton ∅) ([x] [y] p y) (thePropInj p h))❙
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment