Metamath Proof Explorer

Theorem tz7.49c

Description: Corollary of Proposition 7.49 of TakeutiZaring p. 51. (Contributed by NM, 10-Feb-1997) (Revised by Mario Carneiro, 19-Jan-2013)

Ref Expression
Hypothesis tz7.49c.1 
|- F Fn On
Assertion tz7.49c 
|- ( ( A e. B /\ A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) -> E. x e. On ( F |` x ) : x -1-1-onto-> A )

Proof

Step Hyp Ref Expression
1 tz7.49c.1 
 |-  F Fn On
2 biid 
 |-  ( A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) <-> A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) )
3 1 2 tz7.49 
 |-  ( ( A e. B /\ A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) -> E. x e. On ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) )
4 3simpc 
 |-  ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) -> ( ( F " x ) = A /\ Fun `' ( F |` x ) ) )
5 onss 
 |-  ( x e. On -> x C_ On )
6 fnssres 
 |-  ( ( F Fn On /\ x C_ On ) -> ( F |` x ) Fn x )
7 1 5 6 sylancr 
 |-  ( x e. On -> ( F |` x ) Fn x )
8 df-ima 
 |-  ( F " x ) = ran ( F |` x )
9 8 eqeq1i 
 |-  ( ( F " x ) = A <-> ran ( F |` x ) = A )
10 9 biimpi 
 |-  ( ( F " x ) = A -> ran ( F |` x ) = A )
11 7 10 anim12i 
 |-  ( ( x e. On /\ ( F " x ) = A ) -> ( ( F |` x ) Fn x /\ ran ( F |` x ) = A ) )
12 11 anim1i 
 |-  ( ( ( x e. On /\ ( F " x ) = A ) /\ Fun `' ( F |` x ) ) -> ( ( ( F |` x ) Fn x /\ ran ( F |` x ) = A ) /\ Fun `' ( F |` x ) ) )
13 dff1o2 
 |-  ( ( F |` x ) : x -1-1-onto-> A <-> ( ( F |` x ) Fn x /\ Fun `' ( F |` x ) /\ ran ( F |` x ) = A ) )
14 3anan32 
 |-  ( ( ( F |` x ) Fn x /\ Fun `' ( F |` x ) /\ ran ( F |` x ) = A ) <-> ( ( ( F |` x ) Fn x /\ ran ( F |` x ) = A ) /\ Fun `' ( F |` x ) ) )
15 13 14 bitri 
 |-  ( ( F |` x ) : x -1-1-onto-> A <-> ( ( ( F |` x ) Fn x /\ ran ( F |` x ) = A ) /\ Fun `' ( F |` x ) ) )
16 12 15 sylibr 
 |-  ( ( ( x e. On /\ ( F " x ) = A ) /\ Fun `' ( F |` x ) ) -> ( F |` x ) : x -1-1-onto-> A )
17 16 expl 
 |-  ( x e. On -> ( ( ( F " x ) = A /\ Fun `' ( F |` x ) ) -> ( F |` x ) : x -1-1-onto-> A ) )
18 4 17 syl5 
 |-  ( x e. On -> ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) -> ( F |` x ) : x -1-1-onto-> A ) )
19 18 reximia 
 |-  ( E. x e. On ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) -> E. x e. On ( F |` x ) : x -1-1-onto-> A )
20 3 19 syl 
 |-  ( ( A e. B /\ A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) -> E. x e. On ( F |` x ) : x -1-1-onto-> A )