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

Theorem funss 6585
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 5791 . . 3 (𝐴𝐵 → (Rel 𝐵 → Rel 𝐴))
2 coss1 5866 . . . . 5 (𝐴𝐵 → (𝐴𝐴) ⊆ (𝐵𝐴))
3 cnvss 5883 . . . . . 6 (𝐴𝐵𝐴𝐵)
4 coss2 5867 . . . . . 6 (𝐴𝐵 → (𝐵𝐴) ⊆ (𝐵𝐵))
53, 4syl 17 . . . . 5 (𝐴𝐵 → (𝐵𝐴) ⊆ (𝐵𝐵))
62, 5sstrd 3994 . . . 4 (𝐴𝐵 → (𝐴𝐴) ⊆ (𝐵𝐵))
7 sstr2 3990 . . . 4 ((𝐴𝐴) ⊆ (𝐵𝐵) → ((𝐵𝐵) ⊆ I → (𝐴𝐴) ⊆ I ))
86, 7syl 17 . . 3 (𝐴𝐵 → ((𝐵𝐵) ⊆ I → (𝐴𝐴) ⊆ I ))
91, 8anim12d 609 . 2 (𝐴𝐵 → ((Rel 𝐵 ∧ (𝐵𝐵) ⊆ I ) → (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I )))
10 df-fun 6563 . 2 (Fun 𝐵 ↔ (Rel 𝐵 ∧ (𝐵𝐵) ⊆ I ))
11 df-fun 6563 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
129, 10, 113imtr4g 296 1 (𝐴𝐵 → (Fun 𝐵 → Fun 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  wss 3951   I cid 5577  ccnv 5684  ccom 5689  Rel wrel 5690  Fun wfun 6555
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-ss 3968  df-br 5144  df-opab 5206  df-rel 5692  df-cnv 5693  df-co 5694  df-fun 6563
This theorem is referenced by:  funeq  6586  funopab4  6603  funres  6608  fun0  6631  funcnvcnv  6633  funin  6642  funres11  6643  foimacnv  6865  funelss  8072  funsssuppss  8215  fsuppss  9423  strle1  17195  strssd  17242  pjpm  21728  subgrfun  29298  setrecsss  49220
  Copyright terms: Public domain W3C validator