Metamath Proof Explorer

Theorem fiss

Description: Subset relationship for function fi . (Contributed by Jeff Hankins, 7-Oct-2009) (Revised by Mario Carneiro, 24-Nov-2013)

Ref Expression
Assertion fiss 
|- ( ( B e. V /\ A C_ B ) -> ( fi ` A ) C_ ( fi ` B ) )

Proof

Step Hyp Ref Expression
1 sstr2 
 |-  ( A C_ B -> ( B C_ y -> A C_ y ) )
2 1 adantl 
 |-  ( ( B e. V /\ A C_ B ) -> ( B C_ y -> A C_ y ) )
3 2 anim1d 
 |-  ( ( B e. V /\ A C_ B ) -> ( ( B C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) -> ( A C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) ) )
4 3 ss2abdv 
 |-  ( ( B e. V /\ A C_ B ) -> { y | ( B C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } C_ { y | ( A C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } )
5 intss 
 |-  ( { y | ( B C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } C_ { y | ( A C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } -> |^| { y | ( A C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } C_ |^| { y | ( B C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } )
6 4 5 syl 
 |-  ( ( B e. V /\ A C_ B ) -> |^| { y | ( A C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } C_ |^| { y | ( B C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } )
7 ssexg 
 |-  ( ( A C_ B /\ B e. V ) -> A e. _V )
8 7 ancoms 
 |-  ( ( B e. V /\ A C_ B ) -> A e. _V )
9 dffi2 
 |-  ( A e. _V -> ( fi ` A ) = |^| { y | ( A C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } )
10 8 9 syl 
 |-  ( ( B e. V /\ A C_ B ) -> ( fi ` A ) = |^| { y | ( A C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } )
11 dffi2 
 |-  ( B e. V -> ( fi ` B ) = |^| { y | ( B C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } )
12 11 adantr 
 |-  ( ( B e. V /\ A C_ B ) -> ( fi ` B ) = |^| { y | ( B C_ y /\ A. x e. y A. z e. y ( x i^i z ) e. y ) } )
13 6 10 12 3sstr4d 
 |-  ( ( B e. V /\ A C_ B ) -> ( fi ` A ) C_ ( fi ` B ) )