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 
|- ( A C_ B -> ( Fun B -> Fun A ) )

Proof

Step Hyp Ref Expression
1 relss 
 |-  ( A C_ B -> ( Rel B -> Rel A ) )
2 coss1 
 |-  ( A C_ B -> ( A o. `' A ) C_ ( B o. `' A ) )
3 cnvss 
 |-  ( A C_ B -> `' A C_ `' B )
4 coss2 
 |-  ( `' A C_ `' B -> ( B o. `' A ) C_ ( B o. `' B ) )
5 3 4 syl 
 |-  ( A C_ B -> ( B o. `' A ) C_ ( B o. `' B ) )
6 2 5 sstrd 
 |-  ( A C_ B -> ( A o. `' A ) C_ ( B o. `' B ) )
7 sstr2 
 |-  ( ( A o. `' A ) C_ ( B o. `' B ) -> ( ( B o. `' B ) C_ _I -> ( A o. `' A ) C_ _I ) )
8 6 7 syl 
 |-  ( A C_ B -> ( ( B o. `' B ) C_ _I -> ( A o. `' A ) C_ _I ) )
9 1 8 anim12d 
 |-  ( A C_ B -> ( ( Rel B /\ ( B o. `' B ) C_ _I ) -> ( Rel A /\ ( A o. `' A ) C_ _I ) ) )
10 df-fun 
 |-  ( Fun B <-> ( Rel B /\ ( B o. `' B ) C_ _I ) )
11 df-fun 
 |-  ( Fun A <-> ( Rel A /\ ( A o. `' A ) C_ _I ) )
12 9 10 11 3imtr4g 
 |-  ( A C_ B -> ( Fun B -> Fun A ) )