Theorem fvprc 6687

Description: A function's value at a proper class is the empty set. See fvprcALT 6688 for a proof that uses ax-pow 5243 instead of ax-sep 5177 and ax-pr 5307. (Contributed by NM, 20-May-1998.) Avoid ax-pow 5243. (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 5313	. . . . . . . . . 10 ⊢ ¬ ∀𝑦 𝑦 = 𝑥
2		exnal 1834	. . . . . . . . . . 11 ⊢ (∃𝑦 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑦 𝑥 = 𝑦)
3		equcom 2028	. . . . . . . . . . . 12 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)
4	3	albii 1827	. . . . . . . . . . 11 ⊢ (∀𝑦 𝑥 = 𝑦 ↔ ∀𝑦 𝑦 = 𝑥)
5	2, 4	xchbinx 337	. . . . . . . . . 10 ⊢ (∃𝑦 ¬ 𝑥 = 𝑦 ↔ ¬ ∀𝑦 𝑦 = 𝑥)
6	1, 5	mpbir 234	. . . . . . . . 9 ⊢ ∃𝑦 ¬ 𝑥 = 𝑦
7	6	jctr 528	. . . . . . . 8 ⊢ (∅ ∈ 𝐹 → (∅ ∈ 𝐹 ∧ ∃𝑦 ¬ 𝑥 = 𝑦))
8		19.42v 1962	. . . . . . . 8 ⊢ (∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦) ↔ (∅ ∈ 𝐹 ∧ ∃𝑦 ¬ 𝑥 = 𝑦))
9	7, 8	sylibr 237	. . . . . . 7 ⊢ (∅ ∈ 𝐹 → ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦))
10		opprc1 4794	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ V → ⟨𝐴, 𝑥⟩ = ∅)
11	10	eleq1d 2815	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → (⟨𝐴, 𝑥⟩ ∈ 𝐹 ↔ ∅ ∈ 𝐹))
12		opprc1 4794	. . . . . . . . . . . . 13 ⊢ (¬ 𝐴 ∈ V → ⟨𝐴, 𝑦⟩ = ∅)
13	12	eleq1d 2815	. . . . . . . . . . . 12 ⊢ (¬ 𝐴 ∈ V → (⟨𝐴, 𝑦⟩ ∈ 𝐹 ↔ ∅ ∈ 𝐹))
14	11, 13	anbi12d 634	. . . . . . . . . . 11 ⊢ (¬ 𝐴 ∈ V → ((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ↔ (∅ ∈ 𝐹 ∧ ∅ ∈ 𝐹)))
15		anidm 568	. . . . . . . . . . 11 ⊢ ((∅ ∈ 𝐹 ∧ ∅ ∈ 𝐹) ↔ ∅ ∈ 𝐹)
16	14, 15	bitrdi 290	. . . . . . . . . 10 ⊢ (¬ 𝐴 ∈ V → ((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ↔ ∅ ∈ 𝐹))
17	16	anbi1d 633	. . . . . . . . 9 ⊢ (¬ 𝐴 ∈ V → (((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦) ↔ (∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦)))
18	17	exbidv 1929	. . . . . . . 8 ⊢ (¬ 𝐴 ∈ V → (∃𝑦((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦)))
19	11, 18	imbi12d 348	. . . . . . 7 ⊢ (¬ 𝐴 ∈ V → ((⟨𝐴, 𝑥⟩ ∈ 𝐹 → ∃𝑦((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)) ↔ (∅ ∈ 𝐹 → ∃𝑦(∅ ∈ 𝐹 ∧ ¬ 𝑥 = 𝑦))))
20	9, 19	mpbiri 261	. . . . . 6 ⊢ (¬ 𝐴 ∈ V → (⟨𝐴, 𝑥⟩ ∈ 𝐹 → ∃𝑦((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦)))
21		df-br 5040	. . . . . 6 ⊢ (𝐴𝐹𝑥 ↔ ⟨𝐴, 𝑥⟩ ∈ 𝐹)
22		df-br 5040	. . . . . . . . 9 ⊢ (𝐴𝐹𝑦 ↔ ⟨𝐴, 𝑦⟩ ∈ 𝐹)
23	21, 22	anbi12i 630	. . . . . . . 8 ⊢ ((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ↔ (⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹))
24	23	anbi1i 627	. . . . . . 7 ⊢ (((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦))
25	24	exbii 1855	. . . . . 6 ⊢ (∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑦((⟨𝐴, 𝑥⟩ ∈ 𝐹 ∧ ⟨𝐴, 𝑦⟩ ∈ 𝐹) ∧ ¬ 𝑥 = 𝑦))
26	20, 21, 25	3imtr4g 299	. . . . 5 ⊢ (¬ 𝐴 ∈ V → (𝐴𝐹𝑥 → ∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦)))
27	26	eximdv 1925	. . . 4 ⊢ (¬ 𝐴 ∈ V → (∃𝑥 𝐴𝐹𝑥 → ∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦)))
28		exnal 1834	. . . . 5 ⊢ (∃𝑥 ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦) ↔ ¬ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦))
29		exanali 1867	. . . . . 6 ⊢ (∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦))
30	29	exbii 1855	. . . . 5 ⊢ (∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦) ↔ ∃𝑥 ¬ ∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦))
31		breq2 5043	. . . . . . 7 ⊢ (𝑥 = 𝑦 → (𝐴𝐹𝑥 ↔ 𝐴𝐹𝑦))
32	31	mo4 2565	. . . . . 6 ⊢ (∃*𝑥 𝐴𝐹𝑥 ↔ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦))
33	32	notbii 323	. . . . 5 ⊢ (¬ ∃*𝑥 𝐴𝐹𝑥 ↔ ¬ ∀𝑥∀𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) → 𝑥 = 𝑦))
34	28, 30, 33	3bitr4ri 307	. . . 4 ⊢ (¬ ∃*𝑥 𝐴𝐹𝑥 ↔ ∃𝑥∃𝑦((𝐴𝐹𝑥 ∧ 𝐴𝐹𝑦) ∧ ¬ 𝑥 = 𝑦))
35	27, 34	syl6ibr 255	. . 3 ⊢ (¬ 𝐴 ∈ V → (∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥))
36		df-eu 2568	. . . . 5 ⊢ (∃!𝑥 𝐴𝐹𝑥 ↔ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥))
37	36	notbii 323	. . . 4 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 ↔ ¬ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥))
38		imnan 403	. . . 4 ⊢ ((∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥) ↔ ¬ (∃𝑥 𝐴𝐹𝑥 ∧ ∃*𝑥 𝐴𝐹𝑥))
39	37, 38	bitr4i 281	. . 3 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 ↔ (∃𝑥 𝐴𝐹𝑥 → ¬ ∃*𝑥 𝐴𝐹𝑥))
40	35, 39	sylibr 237	. 2 ⊢ (¬ 𝐴 ∈ V → ¬ ∃!𝑥 𝐴𝐹𝑥)
41		tz6.12-2 6684	. 2 ⊢ (¬ ∃!𝑥 𝐴𝐹𝑥 → (𝐹‘𝐴) = ∅)
42	40, 41	syl 17	1 ⊢ (¬ 𝐴 ∈ V → (𝐹‘𝐴) = ∅)

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 399  ∀wal 1541   = wceq 1543  ∃wex 1787   ∈ wcel 2112  ∃*wmo 2537  ∃!weu 2567  Vcvv 3398  ∅c0 4223  ⟨cop 4533   class class class wbr 5039  ‘cfv 6358

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2018  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2708  ax-sep 5177  ax-nul 5184  ax-pr 5307

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2728  df-clel 2809  df-ne 2933  df-ral 3056  df-rex 3057  df-rab 3060  df-v 3400  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4224  df-if 4426  df-sn 4528  df-pr 4530  df-op 4534  df-uni 4806  df-br 5040  df-iota 6316  df-fv 6366

This theorem is referenced by:  rnfvprc  6689  dffv3  6691  fvrn0  6723  ndmfv  6725  fv2prc  6735  csbfv  6740  dffv2  6784  brfvopabrbr  6793  fvmpti  6795  fvmptnf  6818  fvmptrabfv  6827  fvunsn  6972  fvmptopab  7244  brfvopab  7246  1stval  7741  2ndval  7742  fipwuni  9020  fipwss  9023  tctr  9334  ranklim  9425  rankuni  9444  alephsing  9855  itunisuc  9998  itunitc  10000  tskmcl  10420  hashfn  13907  s1prc  14126  trclfvg  14543  trclfvcotrg  14544  dfrtrclrec2  14586  rtrclreclem4  14589  dfrtrcl2  14590  strfvss  16688  strfvi  16718  setsnid  16720  elbasfv  16727  ressbas  16738  resslem  16741  firest  16891  topnval  16893  homffval  17147  comfffval  17155  oppchomfval  17171  oppchomfvalOLD  17172  oppcbas  17176  xpcbas  17639  oduval  17750  oduleval  17751  lubfun  17812  glbfun  17825  odujoin  17868  odumeet  17870  oduclatb  17967  ipopos  17996  isipodrs  17997  plusffval  18074  grpidval  18087  gsum0  18110  ismnd  18130  frmdplusg  18235  frmd0  18241  efmndbas  18252  efmndbasabf  18253  efmndplusg  18261  dfgrp2e  18347  grpinvfval  18360  grpinvfvalALT  18361  grpinvfvi  18364  grpsubfval  18365  grpsubfvalALT  18366  mulgfval  18444  mulgfvalALT  18445  mulgfvi  18448  cntrval  18667  cntzval  18669  cntzrcl  18675  oppgval  18693  oppgplusfval  18694  symgval  18715  lactghmga  18751  psgnfval  18846  odfval  18878  odfvalALT  18879  oppglsm  18985  efgval  19061  mgpval  19461  mgpplusg  19462  ringidval  19472  opprval  19596  opprmulfval  19597  dvdsrval  19617  invrfval  19645  dvrfval  19656  staffval  19837  scaffval  19871  islss  19925  sralem  20168  sravsca  20173  sraip  20174  rlmval  20182  rlmsca2  20192  2idlval  20225  rrgval  20279  zrhval  20428  zlmlem  20437  zlmvsca  20442  chrval  20444  evpmss  20502  ipffval  20564  ocvval  20583  elocv  20584  thlbas  20612  thlle  20613  thloc  20615  pjfval  20622  asclfval  20792  psrbas  20857  psr1val  21061  vr1val  21067  ply1val  21069  ply1basfvi  21116  ply1plusgfvi  21117  psr1sca2  21126  ply1sca2  21129  ply1ascl  21133  evl1fval  21198  evl1fval1  21201  toponsspwpw  21773  istps  21785  tgdif0  21843  indislem  21851  txindislem  22484  fsubbas  22718  filuni  22736  ussval  23111  isusp  23113  nmfval  23440  tnglem  23492  tngds  23500  tcphval  24069  deg1fval  24932  deg1fvi  24937  uc1pval  24991  mon1pval  24993  ttglem  26921  vtxval  27045  iedgval  27046  vtxvalprc  27090  iedgvalprc  27091  edgval  27094  prcliscplgr  27456  wwlks  27873  wwlksn  27875  clwwlk  28020  clwwlkn  28063  clwwlknonmpo  28126  vafval  28638  bafval  28639  smfval  28640  vsfval  28668  resvsca  31202  resvlem  31203  prclisacycgr  32780  mvtval  33129  mexval  33131  mexval2  33132  mdvval  33133  mrsubfval  33137  msubfval  33153  elmsubrn  33157  mvhfval  33162  mpstval  33164  msrfval  33166  mstaval  33173  mclsrcl  33190  mppsval  33201  mthmval  33204  sltval2  33545  sltintdifex  33550  fvsingle  33908  funpartfv  33933  fullfunfv  33935  rankeq1o  34159  atbase  36989  llnbase  37209  lplnbase  37234  lvolbase  37278  lhpbase  37698  mzpmfp  40213  kelac1  40532  mendbas  40653  mendplusgfval  40654  mendmulrfval  40656  mendsca  40658  mendvscafval  40659  brfvimex  41254  clsneibex  41330  neicvgbex  41340  sprssspr  44549  sprsymrelfvlem  44558  prprelprb  44585  prprspr2  44586  upwlkbprop  44916  ipolub00  45895