mathlib3

feat(set_theory/zfc/basic): even more lemmas

#18311

Open