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

Theorem funss 6367
Description: Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994.) (Proof shortened by Mario Carneiro, 24-Jun-2014.)
Assertion
Ref Expression
funss (𝐴𝐵 → (Fun 𝐵 → Fun 𝐴))

Proof of Theorem funss
StepHypRef Expression
1 relss 5649 . . 3 (𝐴𝐵 → (Rel 𝐵 → Rel 𝐴))
2 coss1 5719 . . . . 5 (𝐴𝐵 → (𝐴𝐴) ⊆ (𝐵𝐴))
3 cnvss 5736 . . . . . 6 (𝐴𝐵𝐴𝐵)
4 coss2 5720 . . . . . 6 (𝐴𝐵 → (𝐵𝐴) ⊆ (𝐵𝐵))
53, 4syl 17 . . . . 5 (𝐴𝐵 → (𝐵𝐴) ⊆ (𝐵𝐵))
62, 5sstrd 3975 . . . 4 (𝐴𝐵 → (𝐴𝐴) ⊆ (𝐵𝐵))
7 sstr2 3972 . . . 4 ((𝐴𝐴) ⊆ (𝐵𝐵) → ((𝐵𝐵) ⊆ I → (𝐴𝐴) ⊆ I ))
86, 7syl 17 . . 3 (𝐴𝐵 → ((𝐵𝐵) ⊆ I → (𝐴𝐴) ⊆ I ))
91, 8anim12d 610 . 2 (𝐴𝐵 → ((Rel 𝐵 ∧ (𝐵𝐵) ⊆ I ) → (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I )))
10 df-fun 6350 . 2 (Fun 𝐵 ↔ (Rel 𝐵 ∧ (𝐵𝐵) ⊆ I ))
11 df-fun 6350 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
129, 10, 113imtr4g 298 1 (𝐴𝐵 → (Fun 𝐵 → Fun 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398  wss 3934   I cid 5452  ccnv 5547  ccom 5552  Rel wrel 5553  Fun wfun 6342
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1905  ax-6 1964  ax-7 2009  ax-8 2110  ax-9 2118  ax-10 2139  ax-11 2154  ax-12 2170  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1534  df-ex 1775  df-nf 1779  df-sb 2064  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-in 3941  df-ss 3950  df-br 5058  df-opab 5120  df-rel 5555  df-cnv 5556  df-co 5557  df-fun 6350
This theorem is referenced by:  funeq  6368  funopab4  6385  funres  6390  fun0  6412  funcnvcnv  6414  funin  6423  funres11  6424  foimacnv  6625  funelss  7738  funsssuppss  7848  strssd  16525  strle1  16584  pjpm  20844  subgrfun  27055  setrecsss  44794
  Copyright terms: Public domain W3C validator