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

Theorem funimass3 6596
Description: A kind of contraposition law that infers an image subclass from a subclass of a preimage. Raph Levien remarks: "Likely this could be proved directly, and fvimacnv 6595 would be the special case of 𝐴 being a singleton, but it works this way round too." (Contributed by Raph Levien, 20-Nov-2006.)
Assertion
Ref Expression
funimass3 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → ((𝐹𝐴) ⊆ 𝐵𝐴 ⊆ (𝐹𝐵)))

Proof of Theorem funimass3
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 funimass4 6507 . . 3 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → ((𝐹𝐴) ⊆ 𝐵 ↔ ∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵))
2 ssel 3814 . . . . . 6 (𝐴 ⊆ dom 𝐹 → (𝑥𝐴𝑥 ∈ dom 𝐹))
3 fvimacnv 6595 . . . . . . 7 ((Fun 𝐹𝑥 ∈ dom 𝐹) → ((𝐹𝑥) ∈ 𝐵𝑥 ∈ (𝐹𝐵)))
43ex 403 . . . . . 6 (Fun 𝐹 → (𝑥 ∈ dom 𝐹 → ((𝐹𝑥) ∈ 𝐵𝑥 ∈ (𝐹𝐵))))
52, 4syl9r 78 . . . . 5 (Fun 𝐹 → (𝐴 ⊆ dom 𝐹 → (𝑥𝐴 → ((𝐹𝑥) ∈ 𝐵𝑥 ∈ (𝐹𝐵)))))
65imp31 410 . . . 4 (((Fun 𝐹𝐴 ⊆ dom 𝐹) ∧ 𝑥𝐴) → ((𝐹𝑥) ∈ 𝐵𝑥 ∈ (𝐹𝐵)))
76ralbidva 3166 . . 3 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → (∀𝑥𝐴 (𝐹𝑥) ∈ 𝐵 ↔ ∀𝑥𝐴 𝑥 ∈ (𝐹𝐵)))
81, 7bitrd 271 . 2 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → ((𝐹𝐴) ⊆ 𝐵 ↔ ∀𝑥𝐴 𝑥 ∈ (𝐹𝐵)))
9 dfss3 3809 . 2 (𝐴 ⊆ (𝐹𝐵) ↔ ∀𝑥𝐴 𝑥 ∈ (𝐹𝐵))
108, 9syl6bbr 281 1 ((Fun 𝐹𝐴 ⊆ dom 𝐹) → ((𝐹𝐴) ⊆ 𝐵𝐴 ⊆ (𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 386  wcel 2106  wral 3089  wss 3791  ccnv 5354  dom cdm 5355  cima 5358  Fun wfun 6129  cfv 6135
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2054  ax-9 2115  ax-10 2134  ax-11 2149  ax-12 2162  ax-13 2333  ax-ext 2753  ax-sep 5017  ax-nul 5025  ax-pr 5138
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2550  df-eu 2586  df-clab 2763  df-cleq 2769  df-clel 2773  df-nfc 2920  df-ne 2969  df-ral 3094  df-rex 3095  df-rab 3098  df-v 3399  df-sbc 3652  df-dif 3794  df-un 3796  df-in 3798  df-ss 3805  df-nul 4141  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-uni 4672  df-br 4887  df-opab 4949  df-id 5261  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-iota 6099  df-fun 6137  df-fn 6138  df-fv 6143
This theorem is referenced by:  funimass5  6597  funconstss  6598  fvimacnvALT  6599  fimacnv  6611  r0weon  9168  iscnp3  21456  cnpnei  21476  cnclsi  21484  cncls  21486  cncnp  21492  1stccnp  21674  txcnpi  21820  xkoco2cn  21870  xkococnlem  21871  basqtop  21923  kqnrmlem1  21955  kqnrmlem2  21956  reghmph  22005  nrmhmph  22006  elfm3  22162  rnelfm  22165  symgtgp  22313  tgpconncompeqg  22323  eltsms  22344  ucnprima  22494  plyco0  24385  plyeq0  24404  xrlimcnp  25147  rinvf1o  30011  xppreima  30028  cvmliftmolem1  31876  cvmlift2lem9  31906  cvmlift3lem6  31919  mclsppslem  32093
  Copyright terms: Public domain W3C validator