Theorem modelaxrep 45079

Description: Conditions which guarantee that a class models the Axiom of Replacement ax-rep 5219. 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 7893). 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 𝑀, the formula ∀𝑦𝜑 would need to be replaced with ∀𝑦 ∈ 𝑀𝜒, where 𝜒 is 𝜑 with all quantifiers relativized to 𝑀. However, we can obtain this by using 𝑦 ∈ 𝑀 ∧ 𝜒 for 𝜑 in this theorem, so it does establish that all instances of Replacement hold in 𝑀. (Contributed by Eric Schmidt, 29-Sep-2025.)

Hypotheses

Ref	Expression
modelaxrep.1	⊢ (𝜓 → Tr 𝑀)
modelaxrep.2	⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))
modelaxrep.3	⊢ (𝜓 → ∅ ∈ 𝑀)

Assertion

Ref	Expression
modelaxrep	⊢ (𝜓 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))

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

Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑓)   𝜓(𝑥,𝑦,𝑧,𝑤,𝑓)

Proof of Theorem modelaxrep

Dummy variable 𝑔 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		modelaxrep.1	. 2 ⊢ (𝜓 → Tr 𝑀)
2		modelaxrep.2	. . 3 ⊢ (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀))
3		funeq 6507	. . . . . 6 ⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
4		dmeq 5848	. . . . . . 7 ⊢ (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔)
5	4	eleq1d 2816	. . . . . 6 ⊢ (𝑓 = 𝑔 → (dom 𝑓 ∈ 𝑀 ↔ dom 𝑔 ∈ 𝑀))
6		rneq 5881	. . . . . . 7 ⊢ (𝑓 = 𝑔 → ran 𝑓 = ran 𝑔)
7	6	sseq1d 3961	. . . . . 6 ⊢ (𝑓 = 𝑔 → (ran 𝑓 ⊆ 𝑀 ↔ ran 𝑔 ⊆ 𝑀))
8	3, 5, 7	3anbi123d 1438	. . . . 5 ⊢ (𝑓 = 𝑔 → ((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) ↔ (Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀)))
9	6	eleq1d 2816	. . . . 5 ⊢ (𝑓 = 𝑔 → (ran 𝑓 ∈ 𝑀 ↔ ran 𝑔 ∈ 𝑀))
10	8, 9	imbi12d 344	. . . 4 ⊢ (𝑓 = 𝑔 → (((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀) ↔ ((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)))
11	10	cbvalvw 2037	. . 3 ⊢ (∀𝑓((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀) ↔ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀))
12	2, 11	sylib 218	. 2 ⊢ (𝜓 → ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀))
13		modelaxrep.3	. 2 ⊢ (𝜓 → ∅ ∈ 𝑀)
14		trss 5210	. . . . . . 7 ⊢ (Tr 𝑀 → (𝑥 ∈ 𝑀 → 𝑥 ⊆ 𝑀))
15	14	imp 406	. . . . . 6 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → 𝑥 ⊆ 𝑀)
16	15	ad5ant14 757	. . . . 5 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → 𝑥 ⊆ 𝑀)
17		simp-4r 783	. . . . 5 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀))
18		simpllr 775	. . . . 5 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → ∅ ∈ 𝑀)
19		simplr 768	. . . . 5 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → 𝑥 ∈ 𝑀)
20		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑤(((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀)
21		nfra1 3256	. . . . . 6 ⊢ Ⅎ𝑤∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)
22	20, 21	nfan 1900	. . . . 5 ⊢ Ⅎ𝑤((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦))
23		nfv 1915	. . . . . 6 ⊢ Ⅎ𝑧(((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀)
24		nfcv 2894	. . . . . . 7 ⊢ Ⅎ𝑧𝑀
25		nfra1 3256	. . . . . . . 8 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)
26	24, 25	nfrexw 3280	. . . . . . 7 ⊢ Ⅎ𝑧∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)
27	24, 26	nfralw 3279	. . . . . 6 ⊢ Ⅎ𝑧∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)
28	23, 27	nfan 1900	. . . . 5 ⊢ Ⅎ𝑧((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦))
29		nfopab2 5164	. . . . 5 ⊢ Ⅎ𝑧{⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}
30		eqid 2731	. . . . 5 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}
31		rsp 3220	. . . . . 6 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)))
32	31	adantl 481	. . . . 5 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)))
33	16, 17, 18, 19, 22, 28, 29, 30, 32	modelaxreplem3 45078	. . . 4 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))
34	33	ex 412	. . 3 ⊢ ((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))
35	34	ralrimiva 3124	. 2 ⊢ (((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))
36	1, 12, 13, 35	syl21anc 837	1 ⊢ (𝜓 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1086  ∀wal 1539   ∈ wcel 2111  ∀wral 3047  ∃wrex 3056   ⊆ wss 3897  ∅c0 4282  {copab 5155  Tr wtr 5200  dom cdm 5619  ran crn 5620  Fun wfun 6481

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-rep 5219  ax-sep 5236  ax-nul 5246  ax-pow 5305  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rmo 3346  df-reu 3347  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-pw 4551  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-tr 5201  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6443  df-fun 6489  df-fn 6490  df-f 6491  df-f1 6492  df-fo 6493  df-f1o 6494  df-fv 6495  df-en 8876  df-dom 8877  df-sdom 8878

This theorem is referenced by:  wfaxrep  45092