Metamath Proof Explorer

Theorem tz7.48-2

Description: Proposition 7.48(2) of TakeutiZaring p. 51. (Contributed by NM, 9-Feb-1997) (Revised by David Abernethy, 5-May-2013)

Ref Expression
Hypothesis tz7.48.1 
|- F Fn On
Assertion tz7.48-2 
|- ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> Fun `' F )

Proof

Step Hyp Ref Expression
1 tz7.48.1 
 |-  F Fn On
2 ssid 
 |-  On C_ On
3 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
4 3 ancoms 
 |-  ( ( y e. x /\ x e. On ) -> y e. On )
5 1 fndmi 
 |-  dom F = On
6 5 eleq2i 
 |-  ( y e. dom F <-> y e. On )
7 fnfun 
 |-  ( F Fn On -> Fun F )
8 1 7 ax-mp 
 |-  Fun F
9 funfvima 
 |-  ( ( Fun F /\ y e. dom F ) -> ( y e. x -> ( F ` y ) e. ( F " x ) ) )
10 8 9 mpan 
 |-  ( y e. dom F -> ( y e. x -> ( F ` y ) e. ( F " x ) ) )
11 10 impcom 
 |-  ( ( y e. x /\ y e. dom F ) -> ( F ` y ) e. ( F " x ) )
12 eleq1a 
 |-  ( ( F ` y ) e. ( F " x ) -> ( ( F ` x ) = ( F ` y ) -> ( F ` x ) e. ( F " x ) ) )
13 eldifn 
 |-  ( ( F ` x ) e. ( A \ ( F " x ) ) -> -. ( F ` x ) e. ( F " x ) )
14 12 13 nsyli 
 |-  ( ( F ` y ) e. ( F " x ) -> ( ( F ` x ) e. ( A \ ( F " x ) ) -> -. ( F ` x ) = ( F ` y ) ) )
15 11 14 syl 
 |-  ( ( y e. x /\ y e. dom F ) -> ( ( F ` x ) e. ( A \ ( F " x ) ) -> -. ( F ` x ) = ( F ` y ) ) )
16 6 15 sylan2br 
 |-  ( ( y e. x /\ y e. On ) -> ( ( F ` x ) e. ( A \ ( F " x ) ) -> -. ( F ` x ) = ( F ` y ) ) )
17 4 16 syldan 
 |-  ( ( y e. x /\ x e. On ) -> ( ( F ` x ) e. ( A \ ( F " x ) ) -> -. ( F ` x ) = ( F ` y ) ) )
18 17 expimpd 
 |-  ( y e. x -> ( ( x e. On /\ ( F ` x ) e. ( A \ ( F " x ) ) ) -> -. ( F ` x ) = ( F ` y ) ) )
19 18 com12 
 |-  ( ( x e. On /\ ( F ` x ) e. ( A \ ( F " x ) ) ) -> ( y e. x -> -. ( F ` x ) = ( F ` y ) ) )
20 19 ralrimiv 
 |-  ( ( x e. On /\ ( F ` x ) e. ( A \ ( F " x ) ) ) -> A. y e. x -. ( F ` x ) = ( F ` y ) )
21 20 ralimiaa 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> A. x e. On A. y e. x -. ( F ` x ) = ( F ` y ) )
22 1 tz7.48lem 
 |-  ( ( On C_ On /\ A. x e. On A. y e. x -. ( F ` x ) = ( F ` y ) ) -> Fun `' ( F |` On ) )
23 2 21 22 sylancr 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> Fun `' ( F |` On ) )
24 fnrel 
 |-  ( F Fn On -> Rel F )
25 1 24 ax-mp 
 |-  Rel F
26 5 eqimssi 
 |-  dom F C_ On
27 relssres 
 |-  ( ( Rel F /\ dom F C_ On ) -> ( F |` On ) = F )
28 25 26 27 mp2an 
 |-  ( F |` On ) = F
29 28 cnveqi 
 |-  `' ( F |` On ) = `' F
30 29 funeqi 
 |-  ( Fun `' ( F |` On ) <-> Fun `' F )
31 23 30 sylib 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> Fun `' F )