Metamath Proof Explorer

Theorem cncfss

Description: The set of continuous functions is expanded when the codomain is expanded. (Contributed by Mario Carneiro, 30-Aug-2014)

Ref Expression
Assertion cncfss 
|- ( ( B C_ C /\ C C_ CC ) -> ( A -cn-> B ) C_ ( A -cn-> C ) )

Proof

Step Hyp Ref Expression
1 cncff 
 |-  ( f e. ( A -cn-> B ) -> f : A --> B )
2 1 adantl 
 |-  ( ( ( B C_ C /\ C C_ CC ) /\ f e. ( A -cn-> B ) ) -> f : A --> B )
3 simpll 
 |-  ( ( ( B C_ C /\ C C_ CC ) /\ f e. ( A -cn-> B ) ) -> B C_ C )
4 2 3 fssd 
 |-  ( ( ( B C_ C /\ C C_ CC ) /\ f e. ( A -cn-> B ) ) -> f : A --> C )
5 cncfcdm 
 |-  ( ( C C_ CC /\ f e. ( A -cn-> B ) ) -> ( f e. ( A -cn-> C ) <-> f : A --> C ) )
6 5 adantll 
 |-  ( ( ( B C_ C /\ C C_ CC ) /\ f e. ( A -cn-> B ) ) -> ( f e. ( A -cn-> C ) <-> f : A --> C ) )
7 4 6 mpbird 
 |-  ( ( ( B C_ C /\ C C_ CC ) /\ f e. ( A -cn-> B ) ) -> f e. ( A -cn-> C ) )
8 7 ex 
 |-  ( ( B C_ C /\ C C_ CC ) -> ( f e. ( A -cn-> B ) -> f e. ( A -cn-> C ) ) )
9 8 ssrdv 
 |-  ( ( B C_ C /\ C C_ CC ) -> ( A -cn-> B ) C_ ( A -cn-> C ) )