Users' Mathboxes Mathbox for Eric Schmidt < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  modelaxrep Structured version   Visualization version   GIF version

Theorem modelaxrep 44974
Description: Conditions which guarantee that a class models the Axiom of Replacement ax-rep 5277. 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 7975). 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.
StepHypRef Expression
1 modelaxrep.1 . 2 (𝜓 → Tr 𝑀)
2 modelaxrep.2 . . 3 (𝜓 → ∀𝑓((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) → ran 𝑓𝑀))
3 funeq 6584 . . . . . 6 (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
4 dmeq 5912 . . . . . . 7 (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔)
54eleq1d 2825 . . . . . 6 (𝑓 = 𝑔 → (dom 𝑓𝑀 ↔ dom 𝑔𝑀))
6 rneq 5945 . . . . . . 7 (𝑓 = 𝑔 → ran 𝑓 = ran 𝑔)
76sseq1d 4014 . . . . . 6 (𝑓 = 𝑔 → (ran 𝑓𝑀 ↔ ran 𝑔𝑀))
83, 5, 73anbi123d 1438 . . . . 5 (𝑓 = 𝑔 → ((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) ↔ (Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀)))
96eleq1d 2825 . . . . 5 (𝑓 = 𝑔 → (ran 𝑓𝑀 ↔ ran 𝑔𝑀))
108, 9imbi12d 344 . . . 4 (𝑓 = 𝑔 → (((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) → ran 𝑓𝑀) ↔ ((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)))
1110cbvalvw 2035 . . 3 (∀𝑓((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) → ran 𝑓𝑀) ↔ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀))
122, 11sylib 218 . 2 (𝜓 → ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀))
13 modelaxrep.3 . 2 (𝜓 → ∅ ∈ 𝑀)
14 trss 5268 . . . . . . 7 (Tr 𝑀 → (𝑥𝑀𝑥𝑀))
1514imp 406 . . . . . 6 ((Tr 𝑀𝑥𝑀) → 𝑥𝑀)
1615ad5ant14 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 1914 . . . . . 6 𝑤(((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀)
21 nfra1 3283 . . . . . 6 𝑤𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)
2220, 21nfan 1899 . . . . 5 𝑤((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀) ∧ ∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦))
23 nfv 1914 . . . . . 6 𝑧(((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀)
24 nfcv 2904 . . . . . . 7 𝑧𝑀
25 nfra1 3283 . . . . . . . 8 𝑧𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)
2624, 25nfrexw 3312 . . . . . . 7 𝑧𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)
2724, 26nfralw 3310 . . . . . 6 𝑧𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)
2823, 27nfan 1899 . . . . 5 𝑧((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀) ∧ ∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦))
29 nfopab2 5212 . . . . 5 𝑧{⟨𝑤, 𝑧⟩ ∣ (𝑤𝑥 ∧ (𝑧𝑀 ∧ ∀𝑦𝜑))}
30 eqid 2736 . . . . 5 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝑥 ∧ (𝑧𝑀 ∧ ∀𝑦𝜑))} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝑥 ∧ (𝑧𝑀 ∧ ∀𝑦𝜑))}
31 rsp 3246 . . . . . 6 (∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦) → (𝑤𝑀 → ∃𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)))
3231adantl 481 . . . . 5 (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀) ∧ ∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)) → (𝑤𝑀 → ∃𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)))
3316, 17, 18, 19, 22, 28, 29, 30, 32modelaxreplem3 44973 . . . 4 (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀) ∧ ∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)) → ∃𝑦𝑀𝑧𝑀 (𝑧𝑦 ↔ ∃𝑤𝑀 (𝑤𝑥 ∧ ∀𝑦𝜑)))
3433ex 412 . . 3 ((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀) → (∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦) → ∃𝑦𝑀𝑧𝑀 (𝑧𝑦 ↔ ∃𝑤𝑀 (𝑤𝑥 ∧ ∀𝑦𝜑))))
3534ralrimiva 3145 . 2 (((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) → ∀𝑥𝑀 (∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦) → ∃𝑦𝑀𝑧𝑀 (𝑧𝑦 ↔ ∃𝑤𝑀 (𝑤𝑥 ∧ ∀𝑦𝜑))))
361, 12, 13, 35syl21anc 838 1 (𝜓 → ∀𝑥𝑀 (∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦) → ∃𝑦𝑀𝑧𝑀 (𝑧𝑦 ↔ ∃𝑤𝑀 (𝑤𝑥 ∧ ∀𝑦𝜑))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 206  wa 395  w3a 1087  wal 1538  wcel 2108  wral 3060  wrex 3069  wss 3950  c0 4332  {copab 5203  Tr wtr 5257  dom cdm 5683  ran crn 5684  Fun wfun 6553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-rep 5277  ax-sep 5294  ax-nul 5304  ax-pow 5363  ax-pr 5430  ax-un 7751
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-if 4525  df-pw 4600  df-sn 4625  df-pr 4627  df-op 4631  df-uni 4906  df-iun 4991  df-br 5142  df-opab 5204  df-mpt 5224  df-tr 5258  df-id 5576  df-xp 5689  df-rel 5690  df-cnv 5691  df-co 5692  df-dm 5693  df-rn 5694  df-res 5695  df-ima 5696  df-iota 6512  df-fun 6561  df-fn 6562  df-f 6563  df-f1 6564  df-fo 6565  df-f1o 6566  df-fv 6567  df-en 8982  df-dom 8983  df-sdom 8984
This theorem is referenced by:  wfaxrep  44987
  Copyright terms: Public domain W3C validator