Theorem fvprc 6748

Description: A function's value at a proper class is the empty set. See fvprcALT 6749 for a proof that uses ax-pow 5283 instead of ax-sep 5218 and ax-pr 5347. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5283. (Revised by BTernaryTau, 3-Aug-2024.)

Assertion

Ref	Expression
fvprc	⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

Proof of Theorem fvprc

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dtruALT2 5353	. . . . . . . . . 10 ⊢ ¬ ∀𝑦 𝑦 = 𝑥
2		exnal 1830	. . . . . . . . . . 11 ⊢ (∃𝑦 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑦 𝑥 = 𝑦)
3		equcom 2022	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
4	3	albii 1823	. . . . . . . . . . 11 ⊢ (∀𝑦 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥)
5	2, 4	xchbinx 333	. . . . . . . . . 10 ⊢ (∃𝑦 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑦 𝑦 = 𝑥)
6	1, 5	mpbir 230	. . . . . . . . 9 ⊢ ∃𝑦 ¬ 𝑥 = 𝑦
7	6	jctr 524	. . . . . . . 8 ⊢ (∅ ∈ 𝐹 → (∅ ∈ 𝐹 ∧ ∃𝑦 ¬ 𝑥 = 𝑦))
8		19.42v 1958	. . . . . . . 8 ⊢ (∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦) ↔ (∅ ∈ 𝐹 ∧ ∃𝑦 ¬ 𝑥 = 𝑦))
9	7, 8	sylibr 233	. . . . . . 7 ⊢ (∅ ∈ 𝐹 → ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦))
10		opprc1 4825	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ V → ⟨𝐴, 𝑥⟩ = ∅)
11	10	eleq1d 2823	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → (⟨𝐴, 𝑥⟩ ∈ 𝐹 ↔ ∅ ∈ 𝐹))
12		opprc1 4825	. . . . . . . . . . . . 13 ⊢ (¬ 𝐴 ∈ V → ⟨𝐴, 𝑦⟩ = ∅)
13	12	eleq1d 2823	. . . . . . . . . . . 12 ⊢ (¬ 𝐴 ∈ V → (⟨𝐴, 𝑦⟩ ∈ 𝐹 ↔ ∅ ∈ 𝐹))
14	11, 13	anbi12d 630	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ V → ((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ↔ (∅ ∈ 𝐹 ∧ ∅ ∈ 𝐹)))
15		anidm 564	. . . . . . . . . . 11 ⊢ ((∅ ∈ 𝐹 ∧ ∅ ∈ 𝐹) ↔ ∅ ∈ 𝐹)
16	14, 15	bitrdi 286	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ V → ((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ↔ ∅ ∈ 𝐹))
17	16	anbi1d 629	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ V → (((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦) ↔ (∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦)))
18	17	exbidv 1925	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → (∃𝑦((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦)))
19	11, 18	imbi12d 344	. . . . . . 7 ⊢ (¬ 𝐴 ∈ V → ((⟨𝐴, 𝑥⟩ ∈ 𝐹 → ∃𝑦((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)) ↔ (∅ ∈ 𝐹 → ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦))))
20	9, 19	mpbiri 257	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → (⟨𝐴, 𝑥⟩ ∈ 𝐹 → ∃𝑦((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)))
21		df-br 5071	. . . . . 6 ⊢ (𝐴𝐹𝑥 ↔ ⟨𝐴, 𝑥⟩ ∈ 𝐹)
22		df-br 5071	. . . . . . . . 9 ⊢ (𝐴𝐹𝑦 ↔ ⟨𝐴, 𝑦⟩ ∈ 𝐹)
23	21, 22	anbi12i 626	. . . . . . . 8 ⊢ ((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ↔ (⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹))
24	23	anbi1i 623	. . . . . . 7 ⊢ (((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦))
25	24	exbii 1851	. . . . . 6 ⊢ (∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑦((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦))
26	20, 21, 25	3imtr4g 295	. . . . 5 ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝑥 → ∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦)))
27	26	eximdv 1921	. . . 4 ⊢ (¬ 𝐴 ∈ V → (∃𝑥 𝐴𝐹𝑥 → ∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦)))
28		exnal 1830	. . . . 5 ⊢ (∃𝑥 ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦))
29		exanali 1863	. . . . . 6 ⊢ (∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦))
30	29	exbii 1851	. . . . 5 ⊢ (∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑥 ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦))
31		breq2 5074	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝐴𝐹𝑥 ↔ 𝐴𝐹𝑦))
32	31	mo4 2566	. . . . . 6 ⊢ (∃*𝑥 𝐴𝐹𝑥 ↔ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦))
33	32	notbii 319	. . . . 5 ⊢ (¬ ∃*𝑥 𝐴𝐹𝑥 ↔ ¬ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦))
34	28, 30, 33	3bitr4ri 303	. . . 4 ⊢ (¬ ∃*𝑥 𝐴𝐹𝑥 ↔ ∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦))
35	27, 34	syl6ibr 251	. . 3 ⊢ (¬ 𝐴 ∈ V → (∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥))
36		df-eu 2569	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 ↔ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥))
37	36	notbii 319	. . . 4 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 ↔ ¬ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥))
38		imnan 399	. . . 4 ⊢ ((∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥) ↔ ¬ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥))
39	37, 38	bitr4i 277	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 ↔ (∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥))
40	35, 39	sylibr 233	. 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
41		tz6.12-2 6745	. 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
42	40, 41	syl 17	1 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 395  ∀wal 1537   = wceq 1539  ∃wex 1783   ∈ wcel 2108  ∃*wmo 2538  ∃!weu 2568  Vcvv 3422  ∅c0 4253  ⟨cop 4564   class class class wbr 5070  ‘cfv 6418

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2156  ax-12 2173  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-nf 1788  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2943  df-ral 3068  df-rex 3069  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-uni 4837  df-br 5071  df-iota 6376  df-fv 6426

This theorem is referenced by:  rnfvprc  6750  dffv3  6752  fvrn0  6784  ndmfv  6786  fv2prc  6796  csbfv  6801  dffv2  6845  brfvopabrbr  6854  fvmpti  6856  fvmptnf  6879  fvmptrabfv  6888  fvunsn  7033  fvmptopab  7308  brfvopab  7310  1stval  7806  2ndval  7807  fipwuni  9115  fipwss  9118  tctr  9429  ranklim  9533  rankuni  9552  alephsing  9963  itunisuc  10106  itunitc  10108  tskmcl  10528  hashfn  14018  s1prc  14237  trclfvg  14654  trclfvcotrg  14655  dfrtrclrec2  14697  rtrclreclem4  14700  dfrtrcl2  14701  strfvss  16816  strfvi  16819  fveqprc  16820  oveqprc  16821  setsnidOLD  16839  elbasfv  16846  ressbas  16873  ressbasOLD  16874  resslemOLD  16878  firest  17060  topnval  17062  homffval  17316  comfffval  17324  oppchomfval  17340  oppchomfvalOLD  17341  oppcbasOLD  17346  xpcbas  17811  oduval  17922  oduleval  17923  lubfun  17985  glbfun  17998  odujoin  18041  odumeet  18043  oduclatb  18140  ipopos  18169  isipodrs  18170  plusffval  18247  grpidval  18260  gsum0  18283  ismnd  18303  frmdplusg  18408  frmd0  18414  efmndbas  18425  efmndbasabf  18426  efmndplusg  18434  dfgrp2e  18520  grpinvfval  18533  grpinvfvalALT  18534  grpinvfvi  18537  grpsubfval  18538  grpsubfvalALT  18539  mulgfval  18617  mulgfvalALT  18618  mulgfvi  18621  cntrval  18840  cntzval  18842  cntzrcl  18848  oppgval  18866  oppgplusfval  18867  symgval  18891  lactghmga  18928  psgnfval  19023  odfval  19055  odfvalALT  19056  oppglsm  19162  efgval  19238  mgpval  19638  mgpplusg  19639  ringidval  19654  opprval  19778  opprmulfval  19779  dvdsrval  19802  invrfval  19830  dvrfval  19841  staffval  20022  scaffval  20056  islss  20111  sralem  20354  sralemOLD  20355  sravsca  20363  sraip  20364  rlmval  20374  rlmsca2  20384  2idlval  20417  rrgval  20471  zrhval  20621  zlmlemOLD  20631  zlmvsca  20639  chrval  20641  evpmss  20703  ipffval  20765  ocvval  20784  elocv  20785  thlbas  20813  thlle  20814  thloc  20816  pjfval  20823  asclfval  20993  psrbas  21057  psr1val  21267  vr1val  21273  ply1val  21275  ply1basfvi  21322  ply1plusgfvi  21323  psr1sca2  21332  ply1sca2  21335  ply1ascl  21339  evl1fval  21404  evl1fval1  21407  toponsspwpw  21979  istps  21991  tgdif0  22050  indislem  22058  txindislem  22692  fsubbas  22926  filuni  22944  ussval  23319  isusp  23321  nmfval  23650  tnglemOLD  23703  tngds  23717  tngdsOLD  23718  tcphval  24287  deg1fval  25150  deg1fvi  25155  uc1pval  25209  mon1pval  25211  ttglemOLD  27142  vtxval  27273  iedgval  27274  vtxvalprc  27318  iedgvalprc  27319  edgval  27322  prcliscplgr  27684  wwlks  28101  wwlksn  28103  clwwlk  28248  clwwlkn  28291  clwwlknonmpo  28354  vafval  28866  bafval  28867  smfval  28868  vsfval  28896  resvsca  31431  resvlemOLD  31433  prclisacycgr  33013  mvtval  33362  mexval  33364  mexval2  33365  mdvval  33366  mrsubfval  33370  msubfval  33386  elmsubrn  33390  mvhfval  33395  mpstval  33397  msrfval  33399  mstaval  33406  mclsrcl  33423  mppsval  33434  mthmval  33437  sltval2  33786  sltintdifex  33791  fvsingle  34149  funpartfv  34174  fullfunfv  34176  rankeq1o  34400  atbase  37230  llnbase  37450  lplnbase  37475  lvolbase  37519  lhpbase  37939  mzpmfp  40485  kelac1  40804  mendbas  40925  mendplusgfval  40926  mendmulrfval  40928  mendvscafval  40931  brfvimex  41525  clsneibex  41601  neicvgbex  41611  sprssspr  44821  sprsymrelfvlem  44830  prprelprb  44857  prprspr2  44858  upwlkbprop  45188  ipolub00  46167