Theorem modelaxrep 45405

Description: Conditions which guarantee that a class models the Axiom of Replacement ax-rep 5213. 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 5225). 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 6516	. . . . . 6 ⊢ (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
4		dmeq 5856	. . . . . . 7 ⊢ (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔)
5	4	eleq1d 2822	. . . . . 6 ⊢ (𝑓 = 𝑔 → (dom 𝑓 ∈ 𝑀 ↔ dom 𝑔 ∈ 𝑀))
6		rneq 5889	. . . . . . 7 ⊢ (𝑓 = 𝑔 → ran 𝑓 = ran 𝑔)
7	6	sseq1d 3954	. . . . . 6 ⊢ (𝑓 = 𝑔 → (ran 𝑓 ⊆ 𝑀 ↔ ran 𝑔 ⊆ 𝑀))
8	3, 5, 7	3anbi123d 1439	. . . . 5 ⊢ (𝑓 = 𝑔 → ((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) ↔ (Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀)))
9	6	eleq1d 2822	. . . . 5 ⊢ (𝑓 = 𝑔 → (ran 𝑓 ∈ 𝑀 ↔ ran 𝑔 ∈ 𝑀))
10	8, 9	imbi12d 344	. . . 4 ⊢ (𝑓 = 𝑔 → (((Fun 𝑓 ∧ dom 𝑓 ∈ 𝑀 ∧ ran 𝑓 ⊆ 𝑀) → ran 𝑓 ∈ 𝑀) ↔ ((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)))
11	10	cbvalvw 2038	. . 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 5203	. . . . . . 7 ⊢ (Tr 𝑀 → (𝑥 ∈ 𝑀 → 𝑥 ⊆ 𝑀))
15	14	imp 406	. . . . . 6 ⊢ ((Tr 𝑀 ∧ 𝑥 ∈ 𝑀) → 𝑥 ⊆ 𝑀)
16	15	ad5ant14 758	. . . . 5 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → 𝑥 ⊆ 𝑀)
17		simp-4r 784	. . . . 5 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀))
18		simpllr 776	. . . . 5 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → ∅ ∈ 𝑀)
19		simplr 769	. . . . 5 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → 𝑥 ∈ 𝑀)
20		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑤(((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀)
21		nfra1 3262	. . . . . 6 ⊢ Ⅎ𝑤∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)
22	20, 21	nfan 1901	. . . . 5 ⊢ Ⅎ𝑤((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦))
23		nfv 1916	. . . . . 6 ⊢ Ⅎ𝑧(((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀)
24		nfcv 2899	. . . . . . 7 ⊢ Ⅎ𝑧𝑀
25		nfra1 3262	. . . . . . . 8 ⊢ Ⅎ𝑧∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)
26	24, 25	nfrexw 3286	. . . . . . 7 ⊢ Ⅎ𝑧∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)
27	24, 26	nfralw 3285	. . . . . 6 ⊢ Ⅎ𝑧∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)
28	23, 27	nfan 1901	. . . . 5 ⊢ Ⅎ𝑧((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦))
29		nfopab2 5157	. . . . 5 ⊢ Ⅎ𝑧{⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}
30		eqid 2737	. . . . 5 ⊢ {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))} = {⟨𝑤, 𝑧⟩ ∣ (𝑤 ∈ 𝑥 ∧ (𝑧 ∈ 𝑀 ∧ ∀𝑦𝜑))}
31		rsp 3226	. . . . . 6 ⊢ (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)))
32	31	adantl 481	. . . . 5 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → (𝑤 ∈ 𝑀 → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)))
33	16, 17, 18, 19, 22, 28, 29, 30, 32	modelaxreplem3 45404	. . . 4 ⊢ (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) ∧ ∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦)) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑)))
34	33	ex 412	. . 3 ⊢ ((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥 ∈ 𝑀) → (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))
35	34	ralrimiva 3130	. 2 ⊢ (((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔 ∈ 𝑀 ∧ ran 𝑔 ⊆ 𝑀) → ran 𝑔 ∈ 𝑀)) ∧ ∅ ∈ 𝑀) → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))
36	1, 12, 13, 35	syl21anc 838	1 ⊢ (𝜓 → ∀𝑥 ∈ 𝑀 (∀𝑤 ∈ 𝑀 ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (∀𝑦𝜑 → 𝑧 = 𝑦) → ∃𝑦 ∈ 𝑀 ∀𝑧 ∈ 𝑀 (𝑧 ∈ 𝑦 ↔ ∃𝑤 ∈ 𝑀 (𝑤 ∈ 𝑥 ∧ ∀𝑦𝜑))))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087  ∀wal 1540   ∈ wcel 2114  ∀wral 3052  ∃wrex 3062   ⊆ wss 3890  ∅c0 4274  {copab 5148  Tr wtr 5193  dom cdm 5628  ran crn 5629  Fun wfun 6490

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5213  ax-sep 5232  ax-nul 5242  ax-pow 5306  ax-pr 5374  ax-un 7686

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-rmo 3343  df-reu 3344  df-rab 3391  df-v 3432  df-sbc 3730  df-csb 3839  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-pw 4544  df-sn 4569  df-pr 4571  df-op 4575  df-uni 4852  df-iun 4936  df-br 5087  df-opab 5149  df-mpt 5168  df-tr 5194  df-id 5523  df-xp 5634  df-rel 5635  df-cnv 5636  df-co 5637  df-dm 5638  df-rn 5639  df-res 5640  df-ima 5641  df-iota 6452  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-en 8891  df-dom 8892  df-sdom 8893

This theorem is referenced by:  wfaxrep  45418