>>924
∈-loopは、ZFC-AFA
(ZFCから基礎の公理を取り除いて代わりに別の公理AFAを入れた理論）
なら存在するけど
https://en.wikipedia.org/wiki/Non-well-founded_set_theory

>∈-loopが決して出てこないのは基礎の公理の帰結などではなく

いや、基礎の公理からだけど
「ZFCから基礎の公理を除いたもの」から∈-loopが出てこないなら
基礎の公理が証明できることになるけど、そんなことないから