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

Metamath Proof Explorer

Theorem fint

Description: Function into an intersection. (Contributed by NM, 14-Oct-1999) (Proof shortened by Andrew Salmon, 17-Sep-2011)

Ref Expression
Hypothesis fint.1 
|- B =/= (/)
Assertion fint 
|- ( F : A --> |^| B <-> A. x e. B F : A --> x )

Proof

Step Hyp Ref Expression
1 fint.1 
 |-  B =/= (/)
2 ssint 
 |-  ( ran F C_ |^| B <-> A. x e. B ran F C_ x )
3 2 anbi2i 
 |-  ( ( F Fn A /\ ran F C_ |^| B ) <-> ( F Fn A /\ A. x e. B ran F C_ x ) )
4 r19.28zv 
 |-  ( B =/= (/) -> ( A. x e. B ( F Fn A /\ ran F C_ x ) <-> ( F Fn A /\ A. x e. B ran F C_ x ) ) )
5 1 4 ax-mp 
 |-  ( A. x e. B ( F Fn A /\ ran F C_ x ) <-> ( F Fn A /\ A. x e. B ran F C_ x ) )
6 3 5 bitr4i 
 |-  ( ( F Fn A /\ ran F C_ |^| B ) <-> A. x e. B ( F Fn A /\ ran F C_ x ) )
7 df-f 
 |-  ( F : A --> |^| B <-> ( F Fn A /\ ran F C_ |^| B ) )
8 df-f 
 |-  ( F : A --> x <-> ( F Fn A /\ ran F C_ x ) )
9 8 ralbii 
 |-  ( A. x e. B F : A --> x <-> A. x e. B ( F Fn A /\ ran F C_ x ) )
10 6 7 9 3bitr4i 
 |-  ( F : A --> |^| B <-> A. x e. B F : A --> x )