modelaxrep

Description: Conditions which guarantee that a class models the Axiom of Replacement ax-rep . Similar to Lemma II.2.4(6) of Kunen2 p. 111. The first two hypotheses are those in Kunen. The reason for the third hypothesis that our version of Replacement is different from Kunen's (which is zfrep6 ). If we assumed Regularity, we could eliminate this extra hypothesis, since under Regularity, the empty set is a member of every non-empty transitive class.

Note that, to obtain the relativization of an instance of Replacement to M , the formula A. y ph would need to be replaced with A. y e. M ch , where ch is ph with all quantifiers relativized to M . However, we can obtain this by using y e. M /\ ch for ph in this theorem, so it does establish that all instances of Replacement hold in M . (Contributed by Eric Schmidt, 29-Sep-2025)

	Ref	Expression
Hypotheses	modelaxrep.1	$⊢ ψ \to Tr M$
	modelaxrep.2	$⊢ ψ \to \forall f ((Fun f \land dom f \in M \land ran f \subseteq M) \to ran f \in M)$
	modelaxrep.3	$⊢ ψ \to \emptyset \in M$
Assertion	modelaxrep	$⊢ ψ \to \forall x \in M (\forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y) \to \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y φ)))$

Proof

Step	Hyp	Ref	Expression
1		modelaxrep.1	$⊢ ψ \to Tr M$
2		modelaxrep.2	$⊢ ψ \to \forall f ((Fun f \land dom f \in M \land ran f \subseteq M) \to ran f \in M)$
3		modelaxrep.3	$⊢ ψ \to \emptyset \in M$
4		funeq	$⊢ f = g \to (Fun f \leftrightarrow Fun g)$
5		dmeq	$⊢ f = g \to dom f = dom g$
6	5	eleq1d	$⊢ f = g \to (dom f \in M \leftrightarrow dom g \in M)$
7		rneq	$⊢ f = g \to ran f = ran g$
8	7	sseq1d	$⊢ f = g \to (ran f \subseteq M \leftrightarrow ran g \subseteq M)$
9	4 6 8	3anbi123d	$⊢ f = g \to ((Fun f \land dom f \in M \land ran f \subseteq M) \leftrightarrow (Fun g \land dom g \in M \land ran g \subseteq M))$
10	7	eleq1d	$⊢ f = g \to (ran f \in M \leftrightarrow ran g \in M)$
11	9 10	imbi12d	$⊢ f = g \to (((Fun f \land dom f \in M \land ran f \subseteq M) \to ran f \in M) \leftrightarrow ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M))$
12	11	cbvalvw	$⊢ \forall f ((Fun f \land dom f \in M \land ran f \subseteq M) \to ran f \in M) \leftrightarrow \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)$
13	2 12	sylib	$⊢ ψ \to \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)$
14		trss	$⊢ Tr M \to (x \in M \to x \subseteq M)$
15	14	imp	$⊢ (Tr M \land x \in M) \to x \subseteq M$
16	15	ad5ant14	$⊢ ((((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \land x \in M) \land \forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y)) \to x \subseteq M$
17		simp-4r	$⊢ ((((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \land x \in M) \land \forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y)) \to \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)$
18		simpllr	$⊢ ((((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \land x \in M) \land \forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y)) \to \emptyset \in M$
19		simplr	$⊢ ((((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \land x \in M) \land \forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y)) \to x \in M$
20		nfv	$⊢ Ⅎ w (((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \land x \in M)$
21		nfra1	$⊢ Ⅎ w \forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y)$
22	20 21	nfan	$⊢ Ⅎ w ((((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \land x \in M) \land \forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y))$
23		nfv	$⊢ Ⅎ z (((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \land x \in M)$
24		nfcv	$⊢ \underline{Ⅎ} z M$
25		nfra1	$⊢ Ⅎ z \forall z \in M (\forall y φ \to z = y)$
26	24 25	nfrexw	$⊢ Ⅎ z \exists y \in M \forall z \in M (\forall y φ \to z = y)$
27	24 26	nfralw	$⊢ Ⅎ z \forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y)$
28	23 27	nfan	$⊢ Ⅎ z ((((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \land x \in M) \land \forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y))$
29		nfopab2	$⊢ \underline{Ⅎ} z \{⟨w, z⟩ \| (w \in x \land (z \in M \land \forall y φ))\}$
30		eqid	$⊢ \{⟨w, z⟩ \| (w \in x \land (z \in M \land \forall y φ))\} = \{⟨w, z⟩ \| (w \in x \land (z \in M \land \forall y φ))\}$
31		rsp	$⊢ \forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y) \to (w \in M \to \exists y \in M \forall z \in M (\forall y φ \to z = y))$
32	31	adantl	$⊢ ((((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \land x \in M) \land \forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y)) \to (w \in M \to \exists y \in M \forall z \in M (\forall y φ \to z = y))$
33	16 17 18 19 22 28 29 30 32	modelaxreplem3	$⊢ ((((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \land x \in M) \land \forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y)) \to \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y φ))$
34	33	ex	$⊢ (((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \land x \in M) \to (\forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y) \to \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y φ)))$
35	34	ralrimiva	$⊢ ((Tr M \land \forall g ((Fun g \land dom g \in M \land ran g \subseteq M) \to ran g \in M)) \land \emptyset \in M) \to \forall x \in M (\forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y) \to \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y φ)))$
36	1 13 3 35	syl21anc	$⊢ ψ \to \forall x \in M (\forall w \in M \exists y \in M \forall z \in M (\forall y φ \to z = y) \to \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y φ)))$

Metamath Proof Explorer

Theorem modelaxrep

Proof