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

Theorem mptfnf 6479
Description: The maps-to notation defines a function with domain. (Contributed by Scott Fenton, 21-Mar-2011.) (Revised by Thierry Arnoux, 10-May-2017.)
Hypothesis
Ref Expression
mptfnf.0 𝑥𝐴
Assertion
Ref Expression
mptfnf (∀𝑥𝐴 𝐵 ∈ V ↔ (𝑥𝐴𝐵) Fn 𝐴)

Proof of Theorem mptfnf
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 eueq 3702 . . 3 (𝐵 ∈ V ↔ ∃!𝑦 𝑦 = 𝐵)
21ralbii 3169 . 2 (∀𝑥𝐴 𝐵 ∈ V ↔ ∀𝑥𝐴 ∃!𝑦 𝑦 = 𝐵)
3 r19.26 3174 . . 3 (∀𝑥𝐴 (∃𝑦 𝑦 = 𝐵 ∧ ∃*𝑦 𝑦 = 𝐵) ↔ (∀𝑥𝐴𝑦 𝑦 = 𝐵 ∧ ∀𝑥𝐴 ∃*𝑦 𝑦 = 𝐵))
4 df-eu 2649 . . . 4 (∃!𝑦 𝑦 = 𝐵 ↔ (∃𝑦 𝑦 = 𝐵 ∧ ∃*𝑦 𝑦 = 𝐵))
54ralbii 3169 . . 3 (∀𝑥𝐴 ∃!𝑦 𝑦 = 𝐵 ↔ ∀𝑥𝐴 (∃𝑦 𝑦 = 𝐵 ∧ ∃*𝑦 𝑦 = 𝐵))
6 df-mpt 5143 . . . . . 6 (𝑥𝐴𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)}
76fneq1i 6446 . . . . 5 ((𝑥𝐴𝐵) Fn 𝐴 ↔ {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} Fn 𝐴)
8 df-fn 6354 . . . . 5 ({⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} Fn 𝐴 ↔ (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ∧ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = 𝐴))
97, 8bitri 276 . . . 4 ((𝑥𝐴𝐵) Fn 𝐴 ↔ (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ∧ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = 𝐴))
10 moanimv 2701 . . . . . . 7 (∃*𝑦(𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐴 → ∃*𝑦 𝑦 = 𝐵))
1110albii 1813 . . . . . 6 (∀𝑥∃*𝑦(𝑥𝐴𝑦 = 𝐵) ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦 𝑦 = 𝐵))
12 funopab 6386 . . . . . 6 (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ↔ ∀𝑥∃*𝑦(𝑥𝐴𝑦 = 𝐵))
13 df-ral 3147 . . . . . 6 (∀𝑥𝐴 ∃*𝑦 𝑦 = 𝐵 ↔ ∀𝑥(𝑥𝐴 → ∃*𝑦 𝑦 = 𝐵))
1411, 12, 133bitr4ri 305 . . . . 5 (∀𝑥𝐴 ∃*𝑦 𝑦 = 𝐵 ↔ Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)})
15 eqcom 2831 . . . . . 6 ({𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 = 𝐵)} = 𝐴𝐴 = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 = 𝐵)})
16 dmopab 5782 . . . . . . . 8 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 = 𝐵)}
17 19.42v 1947 . . . . . . . . 9 (∃𝑦(𝑥𝐴𝑦 = 𝐵) ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
1817abbii 2890 . . . . . . . 8 {𝑥 ∣ ∃𝑦(𝑥𝐴𝑦 = 𝐵)} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 = 𝐵)}
1916, 18eqtri 2848 . . . . . . 7 dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 = 𝐵)}
2019eqeq1i 2829 . . . . . 6 (dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = 𝐴 ↔ {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 = 𝐵)} = 𝐴)
21 pm4.71 558 . . . . . . . 8 ((𝑥𝐴 → ∃𝑦 𝑦 = 𝐵) ↔ (𝑥𝐴 ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦 = 𝐵)))
2221albii 1813 . . . . . . 7 (∀𝑥(𝑥𝐴 → ∃𝑦 𝑦 = 𝐵) ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦 = 𝐵)))
23 df-ral 3147 . . . . . . 7 (∀𝑥𝐴𝑦 𝑦 = 𝐵 ↔ ∀𝑥(𝑥𝐴 → ∃𝑦 𝑦 = 𝐵))
24 mptfnf.0 . . . . . . . 8 𝑥𝐴
2524abeq2f 3017 . . . . . . 7 (𝐴 = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 = 𝐵)} ↔ ∀𝑥(𝑥𝐴 ↔ (𝑥𝐴 ∧ ∃𝑦 𝑦 = 𝐵)))
2622, 23, 253bitr4i 304 . . . . . 6 (∀𝑥𝐴𝑦 𝑦 = 𝐵𝐴 = {𝑥 ∣ (𝑥𝐴 ∧ ∃𝑦 𝑦 = 𝐵)})
2715, 20, 263bitr4ri 305 . . . . 5 (∀𝑥𝐴𝑦 𝑦 = 𝐵 ↔ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = 𝐴)
2814, 27anbi12i 626 . . . 4 ((∀𝑥𝐴 ∃*𝑦 𝑦 = 𝐵 ∧ ∀𝑥𝐴𝑦 𝑦 = 𝐵) ↔ (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} ∧ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥𝐴𝑦 = 𝐵)} = 𝐴))
29 ancom 461 . . . 4 ((∀𝑥𝐴 ∃*𝑦 𝑦 = 𝐵 ∧ ∀𝑥𝐴𝑦 𝑦 = 𝐵) ↔ (∀𝑥𝐴𝑦 𝑦 = 𝐵 ∧ ∀𝑥𝐴 ∃*𝑦 𝑦 = 𝐵))
309, 28, 293bitr2i 300 . . 3 ((𝑥𝐴𝐵) Fn 𝐴 ↔ (∀𝑥𝐴𝑦 𝑦 = 𝐵 ∧ ∀𝑥𝐴 ∃*𝑦 𝑦 = 𝐵))
313, 5, 303bitr4ri 305 . 2 ((𝑥𝐴𝐵) Fn 𝐴 ↔ ∀𝑥𝐴 ∃!𝑦 𝑦 = 𝐵)
322, 31bitr4i 279 1 (∀𝑥𝐴 𝐵 ∈ V ↔ (𝑥𝐴𝐵) Fn 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 207  wa 396  wal 1528   = wceq 1530  wex 1773  wcel 2106  ∃*wmo 2613  ∃!weu 2648  {cab 2802  wnfc 2965  wral 3142  Vcvv 3499  {copab 5124  cmpt 5142  dom cdm 5553  Fun wfun 6345   Fn wfn 6346
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2152  ax-12 2167  ax-ext 2796  ax-sep 5199  ax-nul 5206  ax-pr 5325
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2615  df-eu 2649  df-clab 2803  df-cleq 2817  df-clel 2897  df-nfc 2967  df-ral 3147  df-rab 3151  df-v 3501  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4470  df-sn 4564  df-pr 4566  df-op 4570  df-br 5063  df-opab 5125  df-mpt 5143  df-id 5458  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-fun 6353  df-fn 6354
This theorem is referenced by:  fnmptf  6480  mptfnd  41374
  Copyright terms: Public domain W3C validator