Metamath Proof Explorer

Theorem tz7.48-1

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

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

Proof

Step Hyp Ref Expression
1 tz7.48.1 
 |-  F Fn On
2 vex 
 |-  y e. _V
3 2 elrn2 
 |-  ( y e. ran F <-> E. x <. x , y >. e. F )
4 vex 
 |-  x e. _V
5 4 2 opeldm 
 |-  ( <. x , y >. e. F -> x e. dom F )
6 1 fndmi 
 |-  dom F = On
7 5 6 eleqtrdi 
 |-  ( <. x , y >. e. F -> x e. On )
8 7 ancri 
 |-  ( <. x , y >. e. F -> ( x e. On /\ <. x , y >. e. F ) )
9 fnopfvb 
 |-  ( ( F Fn On /\ x e. On ) -> ( ( F ` x ) = y <-> <. x , y >. e. F ) )
10 1 9 mpan 
 |-  ( x e. On -> ( ( F ` x ) = y <-> <. x , y >. e. F ) )
11 10 pm5.32i 
 |-  ( ( x e. On /\ ( F ` x ) = y ) <-> ( x e. On /\ <. x , y >. e. F ) )
12 8 11 sylibr 
 |-  ( <. x , y >. e. F -> ( x e. On /\ ( F ` x ) = y ) )
13 12 eximi 
 |-  ( E. x <. x , y >. e. F -> E. x ( x e. On /\ ( F ` x ) = y ) )
14 3 13 sylbi 
 |-  ( y e. ran F -> E. x ( x e. On /\ ( F ` x ) = y ) )
15 nfra1 
 |-  F/ x A. x e. On ( F ` x ) e. ( A \ ( F " x ) )
16 nfv 
 |-  F/ x y e. A
17 rsp 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> ( x e. On -> ( F ` x ) e. ( A \ ( F " x ) ) ) )
18 eldifi 
 |-  ( ( F ` x ) e. ( A \ ( F " x ) ) -> ( F ` x ) e. A )
19 eleq1 
 |-  ( ( F ` x ) = y -> ( ( F ` x ) e. A <-> y e. A ) )
20 18 19 syl5ibcom 
 |-  ( ( F ` x ) e. ( A \ ( F " x ) ) -> ( ( F ` x ) = y -> y e. A ) )
21 20 imim2i 
 |-  ( ( x e. On -> ( F ` x ) e. ( A \ ( F " x ) ) ) -> ( x e. On -> ( ( F ` x ) = y -> y e. A ) ) )
22 21 impd 
 |-  ( ( x e. On -> ( F ` x ) e. ( A \ ( F " x ) ) ) -> ( ( x e. On /\ ( F ` x ) = y ) -> y e. A ) )
23 17 22 syl 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> ( ( x e. On /\ ( F ` x ) = y ) -> y e. A ) )
24 15 16 23 exlimd 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> ( E. x ( x e. On /\ ( F ` x ) = y ) -> y e. A ) )
25 14 24 syl5 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> ( y e. ran F -> y e. A ) )
26 25 ssrdv 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> ran F C_ A )