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 .
(Contributed by BTernaryTau, 30-Sep-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-smrep | ⊢ ( 𝑀 ⊨ Ax-Rep* ↔ ∀ 𝑓 ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cM | ⊢ 𝑀 | |
| 1 | 0 | wsmrep | ⊢ 𝑀 ⊨ Ax-Rep* |
| 2 | vf | ⊢ 𝑓 | |
| 3 | vx | ⊢ 𝑥 | |
| 4 | vw | ⊢ 𝑤 | |
| 5 | vy | ⊢ 𝑦 | |
| 6 | vz | ⊢ 𝑧 | |
| 7 | 2 | cv | ⊢ 𝑓 |
| 8 | 7 | wfun | ⊢ Fun 𝑓 |
| 9 | 4 | cv | ⊢ 𝑤 |
| 10 | 7 | cdm | ⊢ dom 𝑓 |
| 11 | 9 10 | wcel | ⊢ 𝑤 ∈ dom 𝑓 |
| 12 | 9 7 | cfv | ⊢ ( 𝑓 ‘ 𝑤 ) |
| 13 | 6 | cv | ⊢ 𝑧 |
| 14 | 12 13 | wceq | ⊢ ( 𝑓 ‘ 𝑤 ) = 𝑧 |
| 15 | 8 11 14 | w3a | ⊢ ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) |
| 16 | 15 5 | wal | ⊢ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) |
| 17 | 5 | cv | ⊢ 𝑦 |
| 18 | 13 17 | wceq | ⊢ 𝑧 = 𝑦 |
| 19 | 16 18 | wi | ⊢ ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) |
| 20 | 19 6 0 | wral | ⊢ ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) |
| 21 | 20 5 0 | wrex | ⊢ ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) |
| 22 | 21 4 0 | wral | ⊢ ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) |
| 23 | 13 17 | wcel | ⊢ 𝑧 ∈ 𝑦 |
| 24 | 3 | cv | ⊢ 𝑥 |
| 25 | 9 24 | wcel | ⊢ 𝑤 ∈ 𝑥 |
| 26 | 25 16 | wa | ⊢ ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) |
| 27 | 26 4 0 | wrex | ⊢ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) |
| 28 | 23 27 | wb | ⊢ ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) |
| 29 | 28 6 0 | wral | ⊢ ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) |
| 30 | 29 5 0 | wrex | ⊢ ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) |
| 31 | 22 30 | wi | ⊢ ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) |
| 32 | 31 3 0 | wral | ⊢ ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) |
| 33 | 32 2 | wal | ⊢ ∀ 𝑓 ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) |
| 34 | 1 33 | wb | ⊢ ( 𝑀 ⊨ Ax-Rep* ↔ ∀ 𝑓 ∀ 𝑥 ∈ 𝑀 ( ∀ 𝑤 ∈ 𝑀 ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) → 𝑧 = 𝑦 ) → ∃ 𝑦 ∈ 𝑀 ∀ 𝑧 ∈ 𝑀 ( 𝑧 ∈ 𝑦 ↔ ∃ 𝑤 ∈ 𝑀 ( 𝑤 ∈ 𝑥 ∧ ∀ 𝑦 ( Fun 𝑓 ∧ 𝑤 ∈ dom 𝑓 ∧ ( 𝑓 ‘ 𝑤 ) = 𝑧 ) ) ) ) ) |