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

Step	Hyp	Ref	Expression
1		relss 5791	. . 3 ⊢ (𝐴 ⊆ 𝐵 → (Rel 𝐵 → Rel 𝐴))
2		coss1 5866	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ ◡𝐴) ⊆ (𝐵 ∘ ◡𝐴))
3		cnvss 5883	. . . . . 6 ⊢ (𝐴 ⊆ 𝐵 → ◡𝐴 ⊆ ◡𝐵)
4		coss2 5867	. . . . . 6 ⊢ (◡𝐴 ⊆ ◡𝐵 → (𝐵 ∘ ◡𝐴) ⊆ (𝐵 ∘ ◡𝐵))
5	3, 4	syl 17	. . . . 5 ⊢ (𝐴 ⊆ 𝐵 → (𝐵 ∘ ◡𝐴) ⊆ (𝐵 ∘ ◡𝐵))
6	2, 5	sstrd 3994	. . . 4 ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∘ ◡𝐴) ⊆ (𝐵 ∘ ◡𝐵))
7		sstr2 3990	. . . 4 ⊢ ((𝐴 ∘ ◡𝐴) ⊆ (𝐵 ∘ ◡𝐵) → ((𝐵 ∘ ◡𝐵) ⊆ I → (𝐴 ∘ ◡𝐴) ⊆ I ))
8	6, 7	syl 17	. . 3 ⊢ (𝐴 ⊆ 𝐵 → ((𝐵 ∘ ◡𝐵) ⊆ I → (𝐴 ∘ ◡𝐴) ⊆ I ))
9	1, 8	anim12d 609	. 2 ⊢ (𝐴 ⊆ 𝐵 → ((Rel 𝐵 ∧ (𝐵 ∘ ◡𝐵) ⊆ I ) → (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I )))
10		df-fun 6563	. 2 ⊢ (Fun 𝐵 ↔ (Rel 𝐵 ∧ (𝐵 ∘ ◡𝐵) ⊆ I ))
11		df-fun 6563	. 2 ⊢ (Fun 𝐴 ↔ (Rel 𝐴 ∧ (𝐴 ∘ ◡𝐴) ⊆ I ))
12	9, 10, 11	3imtr4g 296	1 ⊢ (𝐴 ⊆ 𝐵 → (Fun 𝐵 → Fun 𝐴))

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