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

Theorem fnimaeq0 5907
Description: Images under a function never map nonempty sets to empty sets. EDITORIAL: usable in fnwe2lem2 36437. (Contributed by Stefan O'Rear, 21-Jan-2015.)
Assertion
Ref Expression
fnimaeq0 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = ∅ ↔ 𝐵 = ∅))

Proof of Theorem fnimaeq0
StepHypRef Expression
1 imadisj 5385 . 2 ((𝐹𝐵) = ∅ ↔ (dom 𝐹𝐵) = ∅)
2 incom 3761 . . . 4 (dom 𝐹𝐵) = (𝐵 ∩ dom 𝐹)
3 fndm 5885 . . . . . . 7 (𝐹 Fn 𝐴 → dom 𝐹 = 𝐴)
43sseq2d 3590 . . . . . 6 (𝐹 Fn 𝐴 → (𝐵 ⊆ dom 𝐹𝐵𝐴))
54biimpar 500 . . . . 5 ((𝐹 Fn 𝐴𝐵𝐴) → 𝐵 ⊆ dom 𝐹)
6 df-ss 3548 . . . . 5 (𝐵 ⊆ dom 𝐹 ↔ (𝐵 ∩ dom 𝐹) = 𝐵)
75, 6sylib 206 . . . 4 ((𝐹 Fn 𝐴𝐵𝐴) → (𝐵 ∩ dom 𝐹) = 𝐵)
82, 7syl5eq 2650 . . 3 ((𝐹 Fn 𝐴𝐵𝐴) → (dom 𝐹𝐵) = 𝐵)
98eqeq1d 2606 . 2 ((𝐹 Fn 𝐴𝐵𝐴) → ((dom 𝐹𝐵) = ∅ ↔ 𝐵 = ∅))
101, 9syl5bb 270 1 ((𝐹 Fn 𝐴𝐵𝐴) → ((𝐹𝐵) = ∅ ↔ 𝐵 = ∅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382   = wceq 1474  cin 3533  wss 3534  c0 3868  dom cdm 5023  cima 5026   Fn wfn 5780
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-5 1825  ax-6 1873  ax-7 1920  ax-9 1984  ax-10 2004  ax-11 2019  ax-12 2031  ax-13 2227  ax-ext 2584  ax-sep 4698  ax-nul 4707  ax-pr 4823
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1866  df-eu 2456  df-mo 2457  df-clab 2591  df-cleq 2597  df-clel 2600  df-nfc 2734  df-ral 2895  df-rex 2896  df-rab 2899  df-v 3169  df-dif 3537  df-un 3539  df-in 3541  df-ss 3548  df-nul 3869  df-if 4031  df-sn 4120  df-pr 4122  df-op 4126  df-br 4573  df-opab 4633  df-xp 5029  df-cnv 5031  df-dm 5033  df-rn 5034  df-res 5035  df-ima 5036  df-fn 5788
This theorem is referenced by:  ipodrsima  16929  mdegldg  23542  ig1peu  23647  ig1pdvds  23652  kelac1  36449
  Copyright terms: Public domain W3C validator