Transitive collapse fixes transitive subsets

ID: transitive-collapse-fixes-transitive-subsets

If has a well-founded extensional inherited membership relation and is a transitive set, its Mostowski collapse theorem map fixes every member of . The recursion and well-founded relation induction give this pointwise. If also , then .

New to topics? Read the docs here!