Definition df-smrep 36003

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 46077 (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 46077 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 𝜑 is replaced with (Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧). This allows the set 𝑓 to effectively take on the role of the function-like wff, and since 𝑓 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 36007.

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

(Contributed by BTernaryTau, 30-Sep-2026.)

Assertion

Ref	Expression
df-smrep	⊢ (𝑀 ⊨ Ax-Rep* ↔ ∀𝑓∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))))

Distinct variable group:   𝑓,𝑀,𝑤,𝑥,𝑦,𝑧

Detailed syntax breakdown of Definition df-smrep

Step	Hyp	Ref	Expression
1		cM	. . 3 class 𝑀
2	1	wsmrep 36001	. 2 wff 𝑀 ⊨ Ax-Rep*
3		vf	. . . . . . . . . . . . 13 setvar 𝑓
4	3	cv 1568	. . . . . . . . . . . 12 class 𝑓
5	4	wfun 6532	. . . . . . . . . . 11 wff Fun 𝑓
6		vw	. . . . . . . . . . . . 13 setvar 𝑤
7	6	cv 1568	. . . . . . . . . . . 12 class 𝑤
8	4	cdm 5650	. . . . . . . . . . . 12 class dom 𝑓
9	7, 8	wcel 2144	. . . . . . . . . . 11 wff 𝑤 ∈ dom 𝑓
10	7, 4	cfv 6538	. . . . . . . . . . . 12 class (𝑓‘𝑤)
11		vz	. . . . . . . . . . . . 13 setvar 𝑧
12	11	cv 1568	. . . . . . . . . . . 12 class 𝑧
13	10, 12	wceq 1569	. . . . . . . . . . 11 wff (𝑓‘𝑤) = 𝑧
14	5, 9, 13	w3a 1103	. . . . . . . . . 10 wff (Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)
15		vy	. . . . . . . . . 10 setvar 𝑦
16	14, 15	wal 1567	. . . . . . . . 9 wff ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)
17	11, 15	weq 1994	. . . . . . . . 9 wff 𝑧 = 𝑦
18	16, 17	wi 4	. . . . . . . 8 wff (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦)
19	18, 11, 1	wral 3076	. . . . . . 7 wff ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦)
20	19, 15, 1	wrex 3086	. . . . . 6 wff ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦)
21	20, 6, 1	wral 3076	. . . . 5 wff ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦)
22	11, 15	wel 2145	. . . . . . . 8 wff 𝑧 ∈ 𝑦
23		vx	. . . . . . . . . . 11 setvar 𝑥
24	6, 23	wel 2145	. . . . . . . . . 10 wff 𝑤 ∈ 𝑥
25	24, 16	wa 401	. . . . . . . . 9 wff (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))
26	25, 6, 1	wrex 3086	. . . . . . . 8 wff ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))
27	22, 26	wb 209	. . . . . . 7 wff (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))
28	27, 11, 1	wral 3076	. . . . . 6 wff ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))
29	28, 15, 1	wrex 3086	. . . . 5 wff ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))
30	21, 29	wi 4	. . . 4 wff (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))))
31	30, 23, 1	wral 3076	. . 3 wff ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))))
32	31, 3	wal 1567	. 2 wff ∀𝑓∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧))))
33	2, 32	wb 209	1 wff (𝑀 ⊨ Ax-Rep* ↔ ∀𝑓∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧) → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦(Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ (𝑓‘𝑤) = 𝑧)))))

This definition is used by:  smrepsrep  36007  vsmrep  36009