sswfaxreg

Description: A subclass of the class of well-founded sets models the Axiom of Regularity ax-reg . Lemma II.2.4(2) of Kunen2 p. 111. (Contributed by Eric Schmidt, 19-Oct-2025)

		Ref	Expression
	Assertion	sswfaxreg	$⊢ M \subseteq ⋃ R_{1} [On] \to \forall x \in M (\exists y \in M y \in x \to \exists y \in M (y \in x \land \forall z \in M (z \in y \to \neg z \in x)))$

Proof

Step	Hyp	Ref	Expression
1		inn0	$⊢ M \cap x \neq \emptyset \leftrightarrow \exists y \in M y \in x$
2		ssinss1	$⊢ M \subseteq ⋃ R_{1} [On] \to M \cap x \subseteq ⋃ R_{1} [On]$
3		vex	$⊢ x \in V$
4	3	inex2	$⊢ M \cap x \in V$
5		wffr	$⊢ E Fr ⋃ R_{1} [On]$
6		fri	$⊢ ((M \cap x \in V \land E Fr ⋃ R_{1} [On]) \land (M \cap x \subseteq ⋃ R_{1} [On] \land M \cap x \neq \emptyset)) \to \exists y \in (M \cap x) \forall z \in (M \cap x) \neg z E y$
7	4 5 6	mpanl12	$⊢ (M \cap x \subseteq ⋃ R_{1} [On] \land M \cap x \neq \emptyset) \to \exists y \in (M \cap x) \forall z \in (M \cap x) \neg z E y$
8	2 7	sylan	$⊢ (M \subseteq ⋃ R_{1} [On] \land M \cap x \neq \emptyset) \to \exists y \in (M \cap x) \forall z \in (M \cap x) \neg z E y$
9		ralin	$⊢ \forall z \in (M \cap x) \neg z E y \leftrightarrow \forall z \in M (z \in x \to \neg z E y)$
10		con2b	$⊢ (z \in x \to \neg z E y) \leftrightarrow (z E y \to \neg z \in x)$
11		epel	$⊢ z E y \leftrightarrow z \in y$
12	11	imbi1i	$⊢ (z E y \to \neg z \in x) \leftrightarrow (z \in y \to \neg z \in x)$
13	10 12	bitri	$⊢ (z \in x \to \neg z E y) \leftrightarrow (z \in y \to \neg z \in x)$
14	13	ralbii	$⊢ \forall z \in M (z \in x \to \neg z E y) \leftrightarrow \forall z \in M (z \in y \to \neg z \in x)$
15	9 14	bitri	$⊢ \forall z \in (M \cap x) \neg z E y \leftrightarrow \forall z \in M (z \in y \to \neg z \in x)$
16	15	rexbii	$⊢ \exists y \in (M \cap x) \forall z \in (M \cap x) \neg z E y \leftrightarrow \exists y \in (M \cap x) \forall z \in M (z \in y \to \neg z \in x)$
17		rexin	$⊢ \exists y \in (M \cap x) \forall z \in M (z \in y \to \neg z \in x) \leftrightarrow \exists y \in M (y \in x \land \forall z \in M (z \in y \to \neg z \in x))$
18	16 17	bitri	$⊢ \exists y \in (M \cap x) \forall z \in (M \cap x) \neg z E y \leftrightarrow \exists y \in M (y \in x \land \forall z \in M (z \in y \to \neg z \in x))$
19	8 18	sylib	$⊢ (M \subseteq ⋃ R_{1} [On] \land M \cap x \neq \emptyset) \to \exists y \in M (y \in x \land \forall z \in M (z \in y \to \neg z \in x))$
20	1 19	sylan2br	$⊢ (M \subseteq ⋃ R_{1} [On] \land \exists y \in M y \in x) \to \exists y \in M (y \in x \land \forall z \in M (z \in y \to \neg z \in x))$
21	20	ex	$⊢ M \subseteq ⋃ R_{1} [On] \to (\exists y \in M y \in x \to \exists y \in M (y \in x \land \forall z \in M (z \in y \to \neg z \in x)))$
22	21	ralrimivw	$⊢ M \subseteq ⋃ R_{1} [On] \to \forall x \in M (\exists y \in M y \in x \to \exists y \in M (y \in x \land \forall z \in M (z \in y \to \neg z \in x)))$

Metamath Proof Explorer

Theorem sswfaxreg

Proof