Theorem

Let X be an object such that X is an ordinal. Let x, A and B be objects. Assume x∈A, A∈B and B∈X. Then we have x∈B.

Background

The following background is necessary to understand this theorem.

(.) Let A and x be objects. Then x∈A is a proposition.

(.) Let x be an object. Then "x is an ordinal" is a proposition.

Background for Proof

The following background is necessary for the proof.

(.) Let x and y be objects. Then x=y is a proposition.

(.) Let φ be a proposition. Then ¬φ is a proposition.

(.) Let φ and ψ be propositions. Then φ⊃ψ is a proposition.

(.) Let φ and ψ be propositions. Then φ∧ψ is a proposition.

(.) Let φ and ψ be propositions. Then φ∨ψ is a proposition.

(.) Let φ and ψ be propositions. Assume φ⊃ψ and φ. Then we know ψ.

(.) Let A be an object. Then ℘(A) is an object.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Then "∀a∈A⋅φ(a)" is a proposition.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Then "∃a∈A⋅φ(a)" is a proposition.

(.) Let φ and ψ be propositions. Assume φ and ψ. Then we know φ∧ψ.

(.) Let φ and ψ be propositions. Assume φ∧ψ. Then we know φ.

(.) Let φ and ψ be propositions. Assume φ∧ψ. Then we know ψ.

(.) Let A be an object. Let φ(a) be a proposition depending on a member a of A. Assume ∀a∈A⋅φ(a). Let a be a member of A. Then we know φ(a).

(.) Let x be an object. Then "x is nonempty" is a proposition.

(.) Let A be an object. Then A is strictly totally ordered by membership is the proposition given by (∀a∈A⋅∀b∈A⋅∀c∈A⋅(a∈b∧b∈c⊃a∈c)∧∀a∈A⋅∀b∈A⋅(a=b∨a∈b∨b∈a))∧∀a∈A⋅¬a∈a.

(.) Let x be an object. Then "x is a transitive set" is a proposition.

(.) Let A be an object. Then A is well-ordered by membership is the proposition given by "A is strictly totally ordered by membership"∧∀X∈℘(A)⋅("X is nonempty"⊃∃x∈X⋅∀Y∈X⋅(x=Y∨x∈Y)).

(.) Let x be an object. Then x is an ordinal is the proposition given by "x is a transitive set"∧"x is well-ordered by membership".

(.) Let X be an object such that X is an ordinal. Let x and A be objects. Assume A∈X and x∈A. Then we know x∈X.

Proof

Using A∈B and x∈A, it is enough to show x∈A∧A∈B⊃x∈B. We will show ∀Y∈X⋅(x∈A∧A∈Y⊃x∈Y). It is enough to show ∀Y∈X⋅∀Z∈X⋅(x∈Y∧Y∈Z⊃x∈Z). We will show ∀x∈X⋅∀Y∈X⋅∀Z∈X⋅(x∈Y∧Y∈Z⊃x∈Z). It is enough to show ∀x∈X⋅∀Y∈X⋅∀Z∈X⋅(x∈Y∧Y∈Z⊃x∈Z)∧∀Y∈X⋅∀Z∈X⋅(Y=Z∨Y∈Z∨Z∈Y). We will show (∀x∈X⋅∀Y∈X⋅∀Z∈X⋅(x∈Y∧Y∈Z⊃x∈Z)∧∀Y∈X⋅∀Z∈X⋅(Y=Z∨Y∈Z∨Z∈Y))∧∀Y∈X⋅¬Y∈Y. It is enough to show X is strictly totally ordered by membership. We will show "X is strictly totally ordered by membership"∧∀Y∈℘(X)⋅("Y is nonempty"⊃∃x∈Y⋅∀X∈Y⋅(x=X∨x∈X)). It is enough to show X is well-ordered by membership. We know "X is a transitive set"∧"X is well-ordered by membership". Using this, we are done.

Click here to modify variable names (JavaScript Must Be Enabled).