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

Theorem fvimacnv 7067
Description: The argument of a function value belongs to the preimage of any class containing the function value. Raph Levien remarks: "This proof is unsatisfying, because it seems to me that funimass2 6641 could probably be strengthened to a biconditional." (Contributed by Raph Levien, 20-Nov-2006.)
Assertion
Ref Expression
fvimacnv ((Fun 𝐹𝐴 ∈ dom 𝐹) → ((𝐹𝐴) ∈ 𝐵𝐴 ∈ (𝐹𝐵)))

Proof of Theorem fvimacnv
StepHypRef Expression
1 funfvop 7064 . . . . 5 ((Fun 𝐹𝐴 ∈ dom 𝐹) → ⟨𝐴, (𝐹𝐴)⟩ ∈ 𝐹)
2 fvex 6915 . . . . . . 7 (𝐹𝐴) ∈ V
3 opelcnvg 5887 . . . . . . 7 (((𝐹𝐴) ∈ V ∧ 𝐴 ∈ dom 𝐹) → (⟨(𝐹𝐴), 𝐴⟩ ∈ 𝐹 ↔ ⟨𝐴, (𝐹𝐴)⟩ ∈ 𝐹))
42, 3mpan 688 . . . . . 6 (𝐴 ∈ dom 𝐹 → (⟨(𝐹𝐴), 𝐴⟩ ∈ 𝐹 ↔ ⟨𝐴, (𝐹𝐴)⟩ ∈ 𝐹))
54adantl 480 . . . . 5 ((Fun 𝐹𝐴 ∈ dom 𝐹) → (⟨(𝐹𝐴), 𝐴⟩ ∈ 𝐹 ↔ ⟨𝐴, (𝐹𝐴)⟩ ∈ 𝐹))
61, 5mpbird 256 . . . 4 ((Fun 𝐹𝐴 ∈ dom 𝐹) → ⟨(𝐹𝐴), 𝐴⟩ ∈ 𝐹)
7 elimasng 6097 . . . . . 6 (((𝐹𝐴) ∈ V ∧ 𝐴 ∈ dom 𝐹) → (𝐴 ∈ (𝐹 “ {(𝐹𝐴)}) ↔ ⟨(𝐹𝐴), 𝐴⟩ ∈ 𝐹))
82, 7mpan 688 . . . . 5 (𝐴 ∈ dom 𝐹 → (𝐴 ∈ (𝐹 “ {(𝐹𝐴)}) ↔ ⟨(𝐹𝐴), 𝐴⟩ ∈ 𝐹))
98adantl 480 . . . 4 ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐴 ∈ (𝐹 “ {(𝐹𝐴)}) ↔ ⟨(𝐹𝐴), 𝐴⟩ ∈ 𝐹))
106, 9mpbird 256 . . 3 ((Fun 𝐹𝐴 ∈ dom 𝐹) → 𝐴 ∈ (𝐹 “ {(𝐹𝐴)}))
112snss 4794 . . . . 5 ((𝐹𝐴) ∈ 𝐵 ↔ {(𝐹𝐴)} ⊆ 𝐵)
12 imass2 6111 . . . . 5 ({(𝐹𝐴)} ⊆ 𝐵 → (𝐹 “ {(𝐹𝐴)}) ⊆ (𝐹𝐵))
1311, 12sylbi 216 . . . 4 ((𝐹𝐴) ∈ 𝐵 → (𝐹 “ {(𝐹𝐴)}) ⊆ (𝐹𝐵))
1413sseld 3981 . . 3 ((𝐹𝐴) ∈ 𝐵 → (𝐴 ∈ (𝐹 “ {(𝐹𝐴)}) → 𝐴 ∈ (𝐹𝐵)))
1510, 14syl5com 31 . 2 ((Fun 𝐹𝐴 ∈ dom 𝐹) → ((𝐹𝐴) ∈ 𝐵𝐴 ∈ (𝐹𝐵)))
16 fvimacnvi 7066 . . . 4 ((Fun 𝐹𝐴 ∈ (𝐹𝐵)) → (𝐹𝐴) ∈ 𝐵)
1716ex 411 . . 3 (Fun 𝐹 → (𝐴 ∈ (𝐹𝐵) → (𝐹𝐴) ∈ 𝐵))
1817adantr 479 . 2 ((Fun 𝐹𝐴 ∈ dom 𝐹) → (𝐴 ∈ (𝐹𝐵) → (𝐹𝐴) ∈ 𝐵))
1915, 18impbid 211 1 ((Fun 𝐹𝐴 ∈ dom 𝐹) → ((𝐹𝐴) ∈ 𝐵𝐴 ∈ (𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 394  wcel 2098  Vcvv 3473  wss 3949  {csn 4632  cop 4638  ccnv 5681  dom cdm 5682  cima 5685  Fun wfun 6547  cfv 6553
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-12 2166  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2529  df-eu 2558  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-uni 4913  df-br 5153  df-opab 5215  df-id 5580  df-xp 5688  df-rel 5689  df-cnv 5690  df-co 5691  df-dm 5692  df-rn 5693  df-res 5694  df-ima 5695  df-iota 6505  df-fun 6555  df-fn 6556  df-fv 6561
This theorem is referenced by:  funimass3  7068  elpreima  7072  iinpreima  7083  isr0  23669  rnelfmlem  23884  rnelfm  23885  fmfnfmlem2  23887  fmfnfmlem4  23889  fmfnfm  23890  metustid  24491  metustsym  24492  metustexhalf  24493  xppreima  32461  rhmpreimaidl  33166  dstfrvel  34134  ballotlemrv  34180  bj-fvimacnv0  36806  bj-isrvec  36814  grpokerinj  37407  diaintclN  40571  dibintclN  40680  dihintcl  40857  aks6d1c2lem4  41638  aks6d1c6lem2  41683  arearect  42692  areaquad  42693
  Copyright terms: Public domain W3C validator