Theorem funss 6535

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

Step	Hyp	Ref	Expression
1		relss 5744	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴))
2		coss1 5819	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ ◡𝐴) ⊆ (𝐵 ∘ ◡𝐴))
3		cnvss 5836	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
4		coss2 5820	. . . . . 6 ⊢ (◡𝐴 ⊆ ◡𝐵 → (𝐵 ∘ ◡𝐴) ⊆ (𝐵 ∘ ◡𝐵))
5	3, 4	syl 17	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ∘ ◡𝐴) ⊆ (𝐵 ∘ ◡𝐵))
6	2, 5	sstrd 3957	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ ◡𝐴) ⊆ (𝐵 ∘ ◡𝐵))
7		sstr2 3953	. . . 4 ⊢ ((𝐴 ∘ ◡𝐴) ⊆ (𝐵 ∘ ◡𝐵) → ((𝐵 ∘ ◡𝐵) ⊆ I → (𝐴 ∘ ◡𝐴) ⊆ I ))
8	6, 7	syl 17	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝐵 ∘ ◡𝐵) ⊆ I → (𝐴 ∘ ◡𝐴) ⊆ I ))
9	1, 8	anim12d 609	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((Rel 𝐵 ∧ (𝐵 ∘ ◡𝐵) ⊆ I ) → (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )))
10		df-fun 6513	. 2 ⊢ (Fun 𝐵 ↔ (Rel 𝐵 ∧ (𝐵 ∘ ◡𝐵) ⊆ I ))
11		df-fun 6513	. 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
12	9, 10, 11	3imtr4g 296	1 ⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))

Syntax hints:   → wi 4   ∧ wa 395   ⊆ wss 3914   I cid 5532  ^◡ccnv 5637   ∘ ccom 5642  Rel wrel 5643  Fun wfun 6505

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 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ss 3931  df-br 5108  df-opab 5170  df-rel 5645  df-cnv 5646  df-co 5647  df-fun 6513

This theorem is referenced by:  funeq  6536  funopab4  6553  funres  6558  fun0  6581  funcnvcnv  6583  funin  6592  funres11  6593  foimacnv  6817  funelss  8026  funsssuppss  8169  fsuppss  9334  strle1  17128  strssd  17175  pjpm  21617  subgrfun  29208  setrecsss  49690