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!