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

Theorem funss 5871
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 5172 . . 3 (𝐴𝐵 → (Rel 𝐵 → Rel 𝐴))
2 coss1 5242 . . . . 5 (𝐴𝐵 → (𝐴𝐴) ⊆ (𝐵𝐴))
3 cnvss 5259 . . . . . 6 (𝐴𝐵𝐴𝐵)
4 coss2 5243 . . . . . 6 (𝐴𝐵 → (𝐵𝐴) ⊆ (𝐵𝐵))
53, 4syl 17 . . . . 5 (𝐴𝐵 → (𝐵𝐴) ⊆ (𝐵𝐵))
62, 5sstrd 3597 . . . 4 (𝐴𝐵 → (𝐴𝐴) ⊆ (𝐵𝐵))
7 sstr2 3594 . . . 4 ((𝐴𝐴) ⊆ (𝐵𝐵) → ((𝐵𝐵) ⊆ I → (𝐴𝐴) ⊆ I ))
86, 7syl 17 . . 3 (𝐴𝐵 → ((𝐵𝐵) ⊆ I → (𝐴𝐴) ⊆ I ))
91, 8anim12d 585 . 2 (𝐴𝐵 → ((Rel 𝐵 ∧ (𝐵𝐵) ⊆ I ) → (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I )))
10 df-fun 5854 . 2 (Fun 𝐵 ↔ (Rel 𝐵 ∧ (𝐵𝐵) ⊆ I ))
11 df-fun 5854 . 2 (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴𝐴) ⊆ I ))
129, 10, 113imtr4g 285 1 (𝐴𝐵 → (Fun 𝐵 → Fun 𝐴))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  wss 3559   I cid 4989  ccnv 5078  ccom 5083  Rel wrel 5084  Fun wfun 5846
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-in 3566  df-ss 3573  df-br 4619  df-opab 4679  df-rel 5086  df-cnv 5087  df-co 5088  df-fun 5854
This theorem is referenced by:  funeq  5872  funopab4  5888  funres  5892  fun0  5917  funcnvcnv  5919  funin  5928  funres11  5929  foimacnv  6116  funsssuppss  7273  strssd  15841  strle1  15905  xpsc0  16152  xpsc1  16153  pjpm  19984  subgrfun  26083  frrlem5c  31522
  Copyright terms: Public domain W3C validator