Metamath Proof Explorer

Theorem tz7.48-3

Description: Proposition 7.48(3) of TakeutiZaring p. 51. (Contributed by NM, 9-Feb-1997)

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

Proof

Step Hyp Ref Expression
1 tz7.48.1 
 |-  F Fn On
2 1 fndmi 
 |-  dom F = On
3 onprc 
 |-  -. On e. _V
4 2 3 eqneltri 
 |-  -. dom F e. _V
5 1 tz7.48-2 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> Fun `' F )
6 funrnex 
 |-  ( dom `' F e. _V -> ( Fun `' F -> ran `' F e. _V ) )
7 6 com12 
 |-  ( Fun `' F -> ( dom `' F e. _V -> ran `' F e. _V ) )
8 df-rn 
 |-  ran F = dom `' F
9 8 eleq1i 
 |-  ( ran F e. _V <-> dom `' F e. _V )
10 dfdm4 
 |-  dom F = ran `' F
11 10 eleq1i 
 |-  ( dom F e. _V <-> ran `' F e. _V )
12 7 9 11 3imtr4g 
 |-  ( Fun `' F -> ( ran F e. _V -> dom F e. _V ) )
13 5 12 syl 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> ( ran F e. _V -> dom F e. _V ) )
14 4 13 mtoi 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> -. ran F e. _V )
15 1 tz7.48-1 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> ran F C_ A )
16 ssexg 
 |-  ( ( ran F C_ A /\ A e. _V ) -> ran F e. _V )
17 16 ex 
 |-  ( ran F C_ A -> ( A e. _V -> ran F e. _V ) )
18 15 17 syl 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> ( A e. _V -> ran F e. _V ) )
19 14 18 mtod 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> -. A e. _V )