df-smrep

Description: Define the strong Axiom Scheme of Replacement predicate, which is true for a class that is a standard model of the strong version of the Axiom Scheme of Replacement used in wfaxrep (see comments there). Our notation includes an asterisk because we cannot guarantee that a standard model of the Axiom Scheme of Replacement will also be a standard model of this strong version. However, proving that a class is a standard model of the strong Axiom Scheme of Replacement is sufficient to prove that it is also a standard model of the ZF Axiom Scheme of Replacement.

The exact expression used in wfaxrep is unsuitable for use in a definition because it contains a wff metavariable that we cannot quantify over. Instead, this definition uses the specific instance where ph is replaced with ( Fun f /\ w e. dom f /\ ( fw ) = z ) . This allows the set f to effectively take on the role of the function-like wff, and since f is a setvar, we are free to add a universal quantifier over it. The full scheme can then be recovered from this definition using smrepsrep .

This approach works because we can use our ax-rep to guarantee the existence of a suitable f in _V for any x and function-like ph . Note that M is not guaranteed to contain a suitable f (since it might not model the necessary axioms), so we must use an unrestricted universal quantifier for f .

		Ref	Expression
	Assertion	df-smrep	Could not format assertion : No typesetting found for \|- ( M \|=. Ax-Rep* <-> A. f A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) ) with typecode \|-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cM	$class M$
1	0	wsmrep	Could not format M \|=. Ax-Rep* : No typesetting found for wff M \|=. Ax-Rep* with typecode wff
2		vf	$setvar f$
3		vx	$setvar x$
4		vw	$setvar w$
5		vy	$setvar y$
6		vz	$setvar z$
7	2	cv	$setvar f$
8	7	wfun	$wff Fun f$
9	4	cv	$setvar w$
10	7	cdm	$class dom f$
11	9 10	wcel	$wff w \in dom f$
12	9 7	cfv	$class f (w)$
13	6	cv	$setvar z$
14	12 13	wceq	$wff f (w) = z$
15	8 11 14	w3a	$wff (Fun f \land w \in dom f \land f (w) = z)$
16	15 5	wal	$wff \forall y (Fun f \land w \in dom f \land f (w) = z)$
17	5	cv	$setvar y$
18	13 17	wceq	$wff z = y$
19	16 18	wi	$wff (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
20	19 6 0	wral	$wff \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
21	20 5 0	wrex	$wff \exists y \in M \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
22	21 4 0	wral	$wff \forall w \in M \exists y \in M \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \to z = y)$
23	13 17	wcel	$wff z \in y$
24	3	cv	$setvar x$
25	9 24	wcel	$wff w \in x$
26	25 16	wa	$wff (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))$
27	26 4 0	wrex	$wff \exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z))$
28	23 27	wb	$wff (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
29	28 6 0	wral	$wff \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
30	29 5 0	wrex	$wff \exists y \in M \forall z \in M (z \in y \leftrightarrow \exists w \in M (w \in x \land \forall y (Fun f \land w \in dom f \land f (w) = z)))$
31	22 30	wi	$wff (\forall w \in M \exists y \in M \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \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 (Fun f \land w \in dom f \land f (w) = z))))$
32	31 3 0	wral	$wff \forall x \in M (\forall w \in M \exists y \in M \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \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 (Fun f \land w \in dom f \land f (w) = z))))$
33	32 2	wal	$wff \forall f \forall x \in M (\forall w \in M \exists y \in M \forall z \in M (\forall y (Fun f \land w \in dom f \land f (w) = z) \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 (Fun f \land w \in dom f \land f (w) = z))))$
34	1 33	wb	Could not format ( M \|=. Ax-Rep* <-> A. f A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) ) : No typesetting found for wff ( M \|=. Ax-Rep* <-> A. f A. x e. M ( A. w e. M E. y e. M A. z e. M ( A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) -> z = y ) -> E. y e. M A. z e. M ( z e. y <-> E. w e. M ( w e. x /\ A. y ( Fun f /\ w e. dom f /\ ( f ` w ) = z ) ) ) ) ) with typecode wff

Metamath Proof Explorer

Definition df-smrep

Detailed syntax breakdown