Metamath Proof Explorer

Theorem intrnfi

Description: Sufficient condition for the intersection of the range of a function to be in the set of finite intersections. (Contributed by Mario Carneiro, 30-Aug-2015)

Ref Expression
Assertion intrnfi 
|- ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> |^| ran F e. ( fi ` B ) )

Proof

Step Hyp Ref Expression
1 simpr1 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> F : A --> B )
2 1 frnd 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> ran F C_ B )
3 1 fdmd 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> dom F = A )
4 simpr2 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> A =/= (/) )
5 3 4 eqnetrd 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> dom F =/= (/) )
6 dm0rn0 
 |-  ( dom F = (/) <-> ran F = (/) )
7 6 necon3bii 
 |-  ( dom F =/= (/) <-> ran F =/= (/) )
8 5 7 sylib 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> ran F =/= (/) )
9 simpr3 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> A e. Fin )
10 1 ffnd 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> F Fn A )
11 dffn4 
 |-  ( F Fn A <-> F : A -onto-> ran F )
12 10 11 sylib 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> F : A -onto-> ran F )
13 fofi 
 |-  ( ( A e. Fin /\ F : A -onto-> ran F ) -> ran F e. Fin )
14 9 12 13 syl2anc 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> ran F e. Fin )
15 2 8 14 3jca 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> ( ran F C_ B /\ ran F =/= (/) /\ ran F e. Fin ) )
16 elfir 
 |-  ( ( B e. V /\ ( ran F C_ B /\ ran F =/= (/) /\ ran F e. Fin ) ) -> |^| ran F e. ( fi ` B ) )
17 15 16 syldan 
 |-  ( ( B e. V /\ ( F : A --> B /\ A =/= (/) /\ A e. Fin ) ) -> |^| ran F e. ( fi ` B ) )