This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝐴 ) )