Theorem funss

Description: Subclass theorem for function predicate. (Contributed by NM, 16-Aug-1994) (Proof shortened by Mario Carneiro, 24-Jun-2014)

	Ref	Expression
Assertion	funss	⊢ ( 𝐴 ⊆ 𝐵 → ( Fun 𝐵 → Fun 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		relss	⊢ ( 𝐴 ⊆ 𝐵 → ( Rel 𝐵 → Rel 𝐴 ) )
2		coss1	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∘ ◡ 𝐴 ) ⊆ ( 𝐵 ∘ ◡ 𝐴 ) )
3		cnvss	⊢ ( 𝐴 ⊆ 𝐵 → ◡ 𝐴 ⊆ ◡ 𝐵 )
4		coss2	⊢ ( ◡ 𝐴 ⊆ ◡ 𝐵 → ( 𝐵 ∘ ◡ 𝐴 ) ⊆ ( 𝐵 ∘ ◡ 𝐵 ) )
5	3 4	syl	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐵 ∘ ◡ 𝐴 ) ⊆ ( 𝐵 ∘ ◡ 𝐵 ) )
6	2 5	sstrd	⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ∘ ◡ 𝐴 ) ⊆ ( 𝐵 ∘ ◡ 𝐵 ) )
7		sstr2	⊢ ( ( 𝐴 ∘ ◡ 𝐴 ) ⊆ ( 𝐵 ∘ ◡ 𝐵 ) → ( ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I → ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ) )
8	6 7	syl	⊢ ( 𝐴 ⊆ 𝐵 → ( ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I → ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ) )
9	1 8	anim12d	⊢ ( 𝐴 ⊆ 𝐵 → ( ( Rel 𝐵 ∧ ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I ) → ( Rel 𝐴 ∧ ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ) ) )
10		df-fun	⊢ ( Fun 𝐵 ↔ ( Rel 𝐵 ∧ ( 𝐵 ∘ ◡ 𝐵 ) ⊆ I ) )
11		df-fun	⊢ ( Fun 𝐴 ↔ ( Rel 𝐴 ∧ ( 𝐴 ∘ ◡ 𝐴 ) ⊆ I ) )
12	9 10 11	3imtr4g	⊢ ( 𝐴 ⊆ 𝐵 → ( Fun 𝐵 → Fun 𝐴 ) )