Theorem mptfnf 6704

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.

Step	Hyp	Ref	Expression
1		eueq 3669	. . 3 ⊢ (𝐵 ∈ V ↔ ∃!𝑦 𝑦 = 𝐵)
2	1	ralbii 3112	. 2 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑦 = 𝐵)
3		r19.26 3126	. . 3 ⊢ (∀𝑥 ∈ 𝐴 (∃𝑦 𝑦 = 𝐵 ∧ ∃*𝑦 𝑦 = 𝐵) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑦 = 𝐵))
4		df-eu 2597	. . . 4 ⊢ (∃!𝑦 𝑦 = 𝐵 ↔ (∃𝑦 𝑦 = 𝐵 ∧ ∃*𝑦 𝑦 = 𝐵))
5	4	ralbii 3112	. . 3 ⊢ (∀𝑥 ∈ 𝐴 ∃!𝑦 𝑦 = 𝐵 ↔ ∀𝑥 ∈ 𝐴 (∃𝑦 𝑦 = 𝐵 ∧ ∃*𝑦 𝑦 = 𝐵))
6		df-mpt 5193	. . . . . 6 ⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
7	6	fneq1i 6666	. . . . 5 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ↔ {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} Fn 𝐴)
8		df-fn 6569	. . . . 5 ⊢ ({⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} Fn 𝐴 ↔ (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ∧ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = 𝐴))
9	7, 8	bitri 278	. . . 4 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ↔ (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ∧ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = 𝐴))
10		moanimv 2647	. . . . . . 7 ⊢ (∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 → ∃*𝑦 𝑦 = 𝐵))
11	10	albii 1852	. . . . . 6 ⊢ (∀𝑥∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑦 = 𝐵))
12		funopab 6603	. . . . . 6 ⊢ (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ↔ ∀𝑥∃*𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵))
13		df-ral 3081	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 𝑦 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃*𝑦 𝑦 = 𝐵))
14	11, 12, 13	3bitr4ri 307	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∃*𝑦 𝑦 = 𝐵 ↔ Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)})
15		eqcom 2770	. . . . . 6 ⊢ ({𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)} = 𝐴 ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)})
16		dmopab 5909	. . . . . . . 8 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)}
17		19.42v 1988	. . . . . . . . 9 ⊢ (∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵))
18	17	abbii 2830	. . . . . . . 8 ⊢ {𝑥 ∣ ∃𝑦(𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)}
19	16, 18	eqtri 2786	. . . . . . 7 ⊢ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)}
20	19	eqeq1i 2768	. . . . . 6 ⊢ (dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = 𝐴 ↔ {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)} = 𝐴)
21		pm4.71 567	. . . . . . . 8 ⊢ ((𝑥 ∈ 𝐴 → ∃𝑦 𝑦 = 𝐵) ↔ (𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)))
22	21	albii 1852	. . . . . . 7 ⊢ (∀𝑥(𝑥 ∈ 𝐴 → ∃𝑦 𝑦 = 𝐵) ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)))
23		df-ral 3081	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵 ↔ ∀𝑥(𝑥 ∈ 𝐴 → ∃𝑦 𝑦 = 𝐵))
24		mptfnf.0	. . . . . . . 8 ⊢ Ⅎ𝑥𝐴
25	24	eqabf 2955	. . . . . . 7 ⊢ (𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)} ↔ ∀𝑥(𝑥 ∈ 𝐴 ↔ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)))
26	22, 23, 25	3bitr4i 306	. . . . . 6 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵 ↔ 𝐴 = {𝑥 ∣ (𝑥 ∈ 𝐴 ∧ ∃𝑦 𝑦 = 𝐵)})
27	15, 20, 26	3bitr4ri 307	. . . . 5 ⊢ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵 ↔ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = 𝐴)
28	14, 27	anbi12i 640	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 ∃*𝑦 𝑦 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵) ↔ (Fun {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} ∧ dom {⟨𝑥, 𝑦⟩ ∣ (𝑥 ∈ 𝐴 ∧ 𝑦 = 𝐵)} = 𝐴))
29		ancom 466	. . . 4 ⊢ ((∀𝑥 ∈ 𝐴 ∃*𝑦 𝑦 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵) ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑦 = 𝐵))
30	9, 28, 29	3bitr2i 302	. . 3 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ↔ (∀𝑥 ∈ 𝐴 ∃𝑦 𝑦 = 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃*𝑦 𝑦 = 𝐵))
31	3, 5, 30	3bitr4ri 307	. 2 ⊢ ((𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴 ↔ ∀𝑥 ∈ 𝐴 ∃!𝑦 𝑦 = 𝐵)
32	2, 31	bitr4i 281	1 ⊢ (∀𝑥 ∈ 𝐴 𝐵 ∈ V ↔ (𝑥 ∈ 𝐴 ↦ 𝐵) Fn 𝐴)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2147  ∃*wmo 2565  ∃!weu 2596  {cab 2741  Ⅎwnfc 2911  ∀wral 3080  Vcvv 3454  {copab 5173   ↦ cmpt 5192  dom cdm 5658  Fun wfun 6560   Fn wfn 6561

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-pr 5398

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-mpt 5193  df-id 5553  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-fun 6568  df-fn 6569

This theorem is used by:  fnmptf  6705  mptfnd  46527  fnmptif  46550  sqrtnnaa  48186  sqrtnzqaa  48187  sqrtnpoly  48216  tmachlem-extpcover  48228