List of theorems referencing the symbol ULT_MEMBS


(25) Theorem 14: [Ultimate members lemma] S •incin Ult_membs(S)
(26) Theorem 15: [Ultimate members lemma 2] Ult_membs(S) = S + {v: x in S, v in Ult_membs(x)}
(27) Theorem 16: [Key property of ultimate members set] ((X in S) & (Y in X)) •imp (Y in Ult_membs(S))
(28) Theorem 17: [An ordinal is its own set of ultimate members] (Ord(S)) •imp (Ult_membs(S) = S)
(29) Theorem 18: [Ultimate members of a singleton] Ult_membs({S}) = {S} + Ult_membs(S)
(30) Theorem 19: [Ultimate members of an ordinal singleton] Ord(S) •imp (Ult_membs({S}) = S + {S})
(34) Theorem 22: [Monotonicity of ultimate members set] (Y in Ult_membs(S)) •imp (Ult_membs(Y) •incin Ult_membs(S))
(35) Theorem 23: [Members of ultimate members are also subsets] (Y in Ult_membs(S)) •imp (Y •incin Ult_membs(S))
(36) Theorem transfinite_member_induction1: [Ultimate members and transfinite induction] P(mt_thryvar) & (mt_thryvar in Ult_membs({n})) & ((K in mt_thryvar) •imp (not P(K)))
(281) Theorem 234: [acyclicity of the closure of membership] X notin Ult_membs(X)
(282) Theorem 235: [acyclicity of the closure of membership,2] ((X in Ult_membs({Y})) & (Y in Ult_membs({X}))) •imp (X = Y)
(283) Theorem 236: [existence of an in-maximal set in any finite set] (EXISTS v | Finite(F) •imp (((F = 0) or (v in F)) & ({y in (F-{v}) | v in Ult_membs({y})} = 0)))