MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zfrep6 Structured version   Visualization version   GIF version

Theorem zfrep6 7332
Description: A version of the Axiom of Replacement. Normally 𝜑 would have free variables 𝑥 and 𝑦. Axiom 6 of [Kunen] p. 12. The Separation Scheme ax-sep 4941 cannot be derived from this version and must be stated as a separate axiom in an axiom system (such as Kunen's) that uses this version in place of our ax-rep 4930. (Contributed by NM, 10-Oct-2003.)
Assertion
Ref Expression
zfrep6 (∀𝑥𝑧 ∃!𝑦𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑)
Distinct variable groups:   𝜑,𝑤   𝑥,𝑦,𝑧,𝑤
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧)

Proof of Theorem zfrep6
StepHypRef Expression
1 euex 2591 . . . . . . 7 (∃!𝑦𝜑 → ∃𝑦𝜑)
21ralimi 3099 . . . . . 6 (∀𝑥𝑧 ∃!𝑦𝜑 → ∀𝑥𝑧𝑦𝜑)
3 rabid2 3266 . . . . . 6 (𝑧 = {𝑥𝑧 ∣ ∃𝑦𝜑} ↔ ∀𝑥𝑧𝑦𝜑)
42, 3sylibr 225 . . . . 5 (∀𝑥𝑧 ∃!𝑦𝜑𝑧 = {𝑥𝑧 ∣ ∃𝑦𝜑})
5 19.42v 2048 . . . . . . 7 (∃𝑦(𝑥𝑧𝜑) ↔ (𝑥𝑧 ∧ ∃𝑦𝜑))
65abbii 2882 . . . . . 6 {𝑥 ∣ ∃𝑦(𝑥𝑧𝜑)} = {𝑥 ∣ (𝑥𝑧 ∧ ∃𝑦𝜑)}
7 dmopab 5503 . . . . . 6 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = {𝑥 ∣ ∃𝑦(𝑥𝑧𝜑)}
8 df-rab 3064 . . . . . 6 {𝑥𝑧 ∣ ∃𝑦𝜑} = {𝑥 ∣ (𝑥𝑧 ∧ ∃𝑦𝜑)}
96, 7, 83eqtr4i 2797 . . . . 5 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = {𝑥𝑧 ∣ ∃𝑦𝜑}
104, 9syl6reqr 2818 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 → dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} = 𝑧)
11 vex 3353 . . . 4 𝑧 ∈ V
1210, 11syl6eqel 2852 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V)
13 eumo 2592 . . . . . . 7 (∃!𝑦𝜑 → ∃*𝑦𝜑)
1413imim2i 16 . . . . . 6 ((𝑥𝑧 → ∃!𝑦𝜑) → (𝑥𝑧 → ∃*𝑦𝜑))
15 moanimv 2653 . . . . . 6 (∃*𝑦(𝑥𝑧𝜑) ↔ (𝑥𝑧 → ∃*𝑦𝜑))
1614, 15sylibr 225 . . . . 5 ((𝑥𝑧 → ∃!𝑦𝜑) → ∃*𝑦(𝑥𝑧𝜑))
1716alimi 1906 . . . 4 (∀𝑥(𝑥𝑧 → ∃!𝑦𝜑) → ∀𝑥∃*𝑦(𝑥𝑧𝜑))
18 df-ral 3060 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 ↔ ∀𝑥(𝑥𝑧 → ∃!𝑦𝜑))
19 funopab 6103 . . . 4 (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ ∀𝑥∃*𝑦(𝑥𝑧𝜑))
2017, 18, 193imtr4i 283 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
21 funrnex 7331 . . 3 (dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V → (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V))
2212, 20, 21sylc 65 . 2 (∀𝑥𝑧 ∃!𝑦𝜑 → ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V)
23 nfra1 3088 . . 3 𝑥𝑥𝑧 ∃!𝑦𝜑
2410eleq2d 2830 . . . 4 (∀𝑥𝑧 ∃!𝑦𝜑 → (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ 𝑥𝑧))
25 opabid 5143 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ (𝑥𝑧𝜑))
26 vex 3353 . . . . . . . . . 10 𝑥 ∈ V
27 vex 3353 . . . . . . . . . 10 𝑦 ∈ V
2826, 27opelrn 5526 . . . . . . . . 9 (⟨𝑥, 𝑦⟩ ∈ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → 𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
2925, 28sylbir 226 . . . . . . . 8 ((𝑥𝑧𝜑) → 𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)})
3029ex 401 . . . . . . 7 (𝑥𝑧 → (𝜑𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}))
3130impac 548 . . . . . 6 ((𝑥𝑧𝜑) → (𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
3231eximi 1929 . . . . 5 (∃𝑦(𝑥𝑧𝜑) → ∃𝑦(𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
337abeq2i 2878 . . . . 5 (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ↔ ∃𝑦(𝑥𝑧𝜑))
34 df-rex 3061 . . . . 5 (∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑 ↔ ∃𝑦(𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∧ 𝜑))
3532, 33, 343imtr4i 283 . . . 4 (𝑥 ∈ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑)
3624, 35syl6bir 245 . . 3 (∀𝑥𝑧 ∃!𝑦𝜑 → (𝑥𝑧 → ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
3723, 36ralrimi 3104 . 2 (∀𝑥𝑧 ∃!𝑦𝜑 → ∀𝑥𝑧𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑)
38 nfopab1 4878 . . . . . 6 𝑥{⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
3938nfrn 5537 . . . . 5 𝑥ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4039nfeq2 2923 . . . 4 𝑥 𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
41 nfcv 2907 . . . . 5 𝑦𝑤
42 nfopab2 4879 . . . . . 6 𝑦{⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4342nfrn 5537 . . . . 5 𝑦ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}
4441, 43rexeqf 3283 . . . 4 (𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → (∃𝑦𝑤 𝜑 ↔ ∃𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
4540, 44ralbid 3130 . . 3 (𝑤 = ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} → (∀𝑥𝑧𝑦𝑤 𝜑 ↔ ∀𝑥𝑧𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑))
4645spcegv 3446 . 2 (ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)} ∈ V → (∀𝑥𝑧𝑦 ∈ ran {⟨𝑥, 𝑦⟩ ∣ (𝑥𝑧𝜑)}𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑))
4722, 37, 46sylc 65 1 (∀𝑥𝑧 ∃!𝑦𝜑 → ∃𝑤𝑥𝑧𝑦𝑤 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wal 1650   = wceq 1652  wex 1874  wcel 2155  ∃*wmo 2563  ∃!weu 2581  {cab 2751  wral 3055  wrex 3056  {crab 3059  Vcvv 3350  cop 4340  {copab 4871  dom cdm 5277  ran crn 5278  Fun wfun 6062
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-8 2157  ax-9 2164  ax-10 2183  ax-11 2198  ax-12 2211  ax-13 2352  ax-ext 2743  ax-rep 4930  ax-sep 4941  ax-nul 4949  ax-pr 5062  ax-un 7147
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 874  df-3an 1109  df-tru 1656  df-ex 1875  df-nf 1879  df-sb 2063  df-mo 2565  df-eu 2582  df-clab 2752  df-cleq 2758  df-clel 2761  df-nfc 2896  df-ne 2938  df-ral 3060  df-rex 3061  df-reu 3062  df-rab 3064  df-v 3352  df-sbc 3597  df-csb 3692  df-dif 3735  df-un 3737  df-in 3739  df-ss 3746  df-nul 4080  df-if 4244  df-sn 4335  df-pr 4337  df-op 4341  df-uni 4595  df-iun 4678  df-br 4810  df-opab 4872  df-mpt 4889  df-id 5185  df-xp 5283  df-rel 5284  df-cnv 5285  df-co 5286  df-dm 5287  df-rn 5288  df-res 5289  df-ima 5290  df-iota 6031  df-fun 6070  df-fn 6071  df-f 6072  df-f1 6073  df-fo 6074  df-f1o 6075  df-fv 6076
This theorem is referenced by:  bnj865  31441
  Copyright terms: Public domain W3C validator