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 44945
Description: Conditions which guarantee that a class models the Axiom of Replacement ax-rep 5284. 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 7977). 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 6587 . . . . . 6 (𝑓 = 𝑔 → (Fun 𝑓 ↔ Fun 𝑔))
4 dmeq 5916 . . . . . . 7 (𝑓 = 𝑔 → dom 𝑓 = dom 𝑔)
54eleq1d 2823 . . . . . 6 (𝑓 = 𝑔 → (dom 𝑓𝑀 ↔ dom 𝑔𝑀))
6 rneq 5949 . . . . . . 7 (𝑓 = 𝑔 → ran 𝑓 = ran 𝑔)
76sseq1d 4026 . . . . . 6 (𝑓 = 𝑔 → (ran 𝑓𝑀 ↔ ran 𝑔𝑀))
83, 5, 73anbi123d 1435 . . . . 5 (𝑓 = 𝑔 → ((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) ↔ (Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀)))
96eleq1d 2823 . . . . 5 (𝑓 = 𝑔 → (ran 𝑓𝑀 ↔ ran 𝑔𝑀))
108, 9imbi12d 344 . . . 4 (𝑓 = 𝑔 → (((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) → ran 𝑓𝑀) ↔ ((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)))
1110cbvalvw 2032 . . 3 (∀𝑓((Fun 𝑓 ∧ dom 𝑓𝑀 ∧ ran 𝑓𝑀) → ran 𝑓𝑀) ↔ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀))
122, 11sylib 218 . 2 (𝜓 → ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀))
13 modelaxrep.3 . 2 (𝜓 → ∅ ∈ 𝑀)
14 trss 5275 . . . . . . 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 1911 . . . . . 6 𝑤(((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀)
21 nfra1 3281 . . . . . 6 𝑤𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)
2220, 21nfan 1896 . . . . 5 𝑤((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀) ∧ ∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦))
23 nfv 1911 . . . . . 6 𝑧(((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀)
24 nfcv 2902 . . . . . . 7 𝑧𝑀
25 nfra1 3281 . . . . . . . 8 𝑧𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)
2624, 25nfrexw 3310 . . . . . . 7 𝑧𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)
2724, 26nfralw 3308 . . . . . 6 𝑧𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)
2823, 27nfan 1896 . . . . 5 𝑧((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀) ∧ ∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦))
29 nfopab2 5218 . . . . 5 𝑧{⟨𝑤, 𝑧⟩ ∣ (𝑤𝑥 ∧ (𝑧𝑀 ∧ ∀𝑦𝜑))}
30 eqid 2734 . . . . 5 {⟨𝑤, 𝑧⟩ ∣ (𝑤𝑥 ∧ (𝑧𝑀 ∧ ∀𝑦𝜑))} = {⟨𝑤, 𝑧⟩ ∣ (𝑤𝑥 ∧ (𝑧𝑀 ∧ ∀𝑦𝜑))}
31 rsp 3244 . . . . . 6 (∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦) → (𝑤𝑀 → ∃𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)))
3231adantl 481 . . . . 5 (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀) ∧ ∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)) → (𝑤𝑀 → ∃𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)))
3316, 17, 18, 19, 22, 28, 29, 30, 32modelaxreplem3 44944 . . . 4 (((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀) ∧ ∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦)) → ∃𝑦𝑀𝑧𝑀 (𝑧𝑦 ↔ ∃𝑤𝑀 (𝑤𝑥 ∧ ∀𝑦𝜑)))
3433ex 412 . . 3 ((((Tr 𝑀 ∧ ∀𝑔((Fun 𝑔 ∧ dom 𝑔𝑀 ∧ ran 𝑔𝑀) → ran 𝑔𝑀)) ∧ ∅ ∈ 𝑀) ∧ 𝑥𝑀) → (∀𝑤𝑀𝑦𝑀𝑧𝑀 (∀𝑦𝜑𝑧 = 𝑦) → ∃𝑦𝑀𝑧𝑀 (𝑧𝑦 ↔ ∃𝑤𝑀 (𝑤𝑥 ∧ ∀𝑦𝜑))))
3534ralrimiva 3143 . 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 1086  wal 1534  wcel 2105  wral 3058  wrex 3067  wss 3962  c0 4338  {copab 5209  Tr wtr 5264  dom cdm 5688  ran crn 5689  Fun wfun 6556
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-en 8984  df-dom 8985  df-sdom 8986
This theorem is referenced by:  wfaxrep  44949
  Copyright terms: Public domain W3C validator