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

Theorem f00 6770
Description: A class is a function with empty codomain iff it and its domain are empty. (Contributed by NM, 10-Dec-2003.)
Assertion
Ref Expression
f00 (𝐹:π΄βŸΆβˆ… ↔ (𝐹 = βˆ… ∧ 𝐴 = βˆ…))

Proof of Theorem f00
StepHypRef Expression
1 ffun 6717 . . . . 5 (𝐹:π΄βŸΆβˆ… β†’ Fun 𝐹)
2 frn 6721 . . . . . . 7 (𝐹:π΄βŸΆβˆ… β†’ ran 𝐹 βŠ† βˆ…)
3 ss0 4397 . . . . . . 7 (ran 𝐹 βŠ† βˆ… β†’ ran 𝐹 = βˆ…)
42, 3syl 17 . . . . . 6 (𝐹:π΄βŸΆβˆ… β†’ ran 𝐹 = βˆ…)
5 dm0rn0 5922 . . . . . 6 (dom 𝐹 = βˆ… ↔ ran 𝐹 = βˆ…)
64, 5sylibr 233 . . . . 5 (𝐹:π΄βŸΆβˆ… β†’ dom 𝐹 = βˆ…)
7 df-fn 6543 . . . . 5 (𝐹 Fn βˆ… ↔ (Fun 𝐹 ∧ dom 𝐹 = βˆ…))
81, 6, 7sylanbrc 583 . . . 4 (𝐹:π΄βŸΆβˆ… β†’ 𝐹 Fn βˆ…)
9 fn0 6678 . . . 4 (𝐹 Fn βˆ… ↔ 𝐹 = βˆ…)
108, 9sylib 217 . . 3 (𝐹:π΄βŸΆβˆ… β†’ 𝐹 = βˆ…)
11 fdm 6723 . . . 4 (𝐹:π΄βŸΆβˆ… β†’ dom 𝐹 = 𝐴)
1211, 6eqtr3d 2774 . . 3 (𝐹:π΄βŸΆβˆ… β†’ 𝐴 = βˆ…)
1310, 12jca 512 . 2 (𝐹:π΄βŸΆβˆ… β†’ (𝐹 = βˆ… ∧ 𝐴 = βˆ…))
14 f0 6769 . . 3 βˆ…:βˆ…βŸΆβˆ…
15 feq1 6695 . . . 4 (𝐹 = βˆ… β†’ (𝐹:π΄βŸΆβˆ… ↔ βˆ…:π΄βŸΆβˆ…))
16 feq2 6696 . . . 4 (𝐴 = βˆ… β†’ (βˆ…:π΄βŸΆβˆ… ↔ βˆ…:βˆ…βŸΆβˆ…))
1715, 16sylan9bb 510 . . 3 ((𝐹 = βˆ… ∧ 𝐴 = βˆ…) β†’ (𝐹:π΄βŸΆβˆ… ↔ βˆ…:βˆ…βŸΆβˆ…))
1814, 17mpbiri 257 . 2 ((𝐹 = βˆ… ∧ 𝐴 = βˆ…) β†’ 𝐹:π΄βŸΆβˆ…)
1913, 18impbii 208 1 (𝐹:π΄βŸΆβˆ… ↔ (𝐹 = βˆ… ∧ 𝐴 = βˆ…))
Colors of variables: wff setvar class
Syntax hints:   ↔ wb 205   ∧ wa 396   = wceq 1541   βŠ† wss 3947  βˆ…c0 4321  dom cdm 5675  ran crn 5676  Fun wfun 6534   Fn wfn 6535  βŸΆwf 6536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703  ax-sep 5298  ax-nul 5305  ax-pr 5426
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2534  df-clab 2710  df-cleq 2724  df-clel 2810  df-ral 3062  df-rex 3071  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-fun 6542  df-fn 6543  df-f 6544
This theorem is referenced by:  dom0  9098  cantnff  9665  0wrd0  14486  supcvg  15798  ram0  16951  itgsubstlem  25556  uhgr0vb  28321  lfuhgr1v0e  28500  wlkv0  28897  sate0fv0  34396  prv0  34409  ismgmOLD  36706  mof0  47457  mof0ALT  47459  mofeu  47467  fdomne0  47469  f002  47473  fullthinc  47619
  Copyright terms: Public domain W3C validator