Metamath Proof Explorer

Theorem tz7.49

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

Ref Expression
Hypotheses tz7.49.1 
|- F Fn On
tz7.49.2 
|- ( ph <-> A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) )
Assertion tz7.49 
|- ( ( A e. B /\ ph ) -> E. x e. On ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) )

Proof

Step Hyp Ref Expression
1 tz7.49.1 
 |-  F Fn On
2 tz7.49.2 
 |-  ( ph <-> A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) )
3 df-ne 
 |-  ( ( A \ ( F " x ) ) =/= (/) <-> -. ( A \ ( F " x ) ) = (/) )
4 3 ralbii 
 |-  ( A. x e. On ( A \ ( F " x ) ) =/= (/) <-> A. x e. On -. ( A \ ( F " x ) ) = (/) )
5 ralim 
 |-  ( A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) -> ( A. x e. On ( A \ ( F " x ) ) =/= (/) -> A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) ) )
6 2 5 sylbi 
 |-  ( ph -> ( A. x e. On ( A \ ( F " x ) ) =/= (/) -> A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) ) )
7 4 6 syl5bir 
 |-  ( ph -> ( A. x e. On -. ( A \ ( F " x ) ) = (/) -> A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) ) )
8 1 tz7.48-3 
 |-  ( A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) -> -. A e. _V )
9 elex 
 |-  ( A e. B -> A e. _V )
10 8 9 nsyl3 
 |-  ( A e. B -> -. A. x e. On ( F ` x ) e. ( A \ ( F " x ) ) )
11 7 10 nsyli 
 |-  ( ph -> ( A e. B -> -. A. x e. On -. ( A \ ( F " x ) ) = (/) ) )
12 dfrex2 
 |-  ( E. x e. On ( A \ ( F " x ) ) = (/) <-> -. A. x e. On -. ( A \ ( F " x ) ) = (/) )
13 11 12 syl6ibr 
 |-  ( ph -> ( A e. B -> E. x e. On ( A \ ( F " x ) ) = (/) ) )
14 imaeq2 
 |-  ( x = y -> ( F " x ) = ( F " y ) )
15 14 difeq2d 
 |-  ( x = y -> ( A \ ( F " x ) ) = ( A \ ( F " y ) ) )
16 15 eqeq1d 
 |-  ( x = y -> ( ( A \ ( F " x ) ) = (/) <-> ( A \ ( F " y ) ) = (/) ) )
17 16 onminex 
 |-  ( E. x e. On ( A \ ( F " x ) ) = (/) -> E. x e. On ( ( A \ ( F " x ) ) = (/) /\ A. y e. x -. ( A \ ( F " y ) ) = (/) ) )
18 13 17 syl6 
 |-  ( ph -> ( A e. B -> E. x e. On ( ( A \ ( F " x ) ) = (/) /\ A. y e. x -. ( A \ ( F " y ) ) = (/) ) ) )
19 df-ne 
 |-  ( ( A \ ( F " y ) ) =/= (/) <-> -. ( A \ ( F " y ) ) = (/) )
20 19 ralbii 
 |-  ( A. y e. x ( A \ ( F " y ) ) =/= (/) <-> A. y e. x -. ( A \ ( F " y ) ) = (/) )
21 20 anbi2i 
 |-  ( ( ( A \ ( F " x ) ) = (/) /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) <-> ( ( A \ ( F " x ) ) = (/) /\ A. y e. x -. ( A \ ( F " y ) ) = (/) ) )
22 21 rexbii 
 |-  ( E. x e. On ( ( A \ ( F " x ) ) = (/) /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) <-> E. x e. On ( ( A \ ( F " x ) ) = (/) /\ A. y e. x -. ( A \ ( F " y ) ) = (/) ) )
23 18 22 syl6ibr 
 |-  ( ph -> ( A e. B -> E. x e. On ( ( A \ ( F " x ) ) = (/) /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) ) )
24 nfra1 
 |-  F/ x A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) )
25 2 24 nfxfr 
 |-  F/ x ph
26 simpllr 
 |-  ( ( ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) /\ x e. On ) /\ ( A \ ( F " x ) ) = (/) ) -> A. y e. x ( A \ ( F " y ) ) =/= (/) )
27 fnfun 
 |-  ( F Fn On -> Fun F )
28 1 27 ax-mp 
 |-  Fun F
29 fvelima 
 |-  ( ( Fun F /\ z e. ( F " x ) ) -> E. y e. x ( F ` y ) = z )
30 28 29 mpan 
 |-  ( z e. ( F " x ) -> E. y e. x ( F ` y ) = z )
31 nfv 
 |-  F/ y ph
32 nfra1 
 |-  F/ y A. y e. x ( A \ ( F " y ) ) =/= (/)
33 31 32 nfan 
 |-  F/ y ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) )
34 nfv 
 |-  F/ y ( x e. On -> z e. A )
35 rsp 
 |-  ( A. y e. x ( A \ ( F " y ) ) =/= (/) -> ( y e. x -> ( A \ ( F " y ) ) =/= (/) ) )
36 35 adantld 
 |-  ( A. y e. x ( A \ ( F " y ) ) =/= (/) -> ( ( x e. On /\ y e. x ) -> ( A \ ( F " y ) ) =/= (/) ) )
37 onelon 
 |-  ( ( x e. On /\ y e. x ) -> y e. On )
38 15 neeq1d 
 |-  ( x = y -> ( ( A \ ( F " x ) ) =/= (/) <-> ( A \ ( F " y ) ) =/= (/) ) )
39 fveq2 
 |-  ( x = y -> ( F ` x ) = ( F ` y ) )
40 39 15 eleq12d 
 |-  ( x = y -> ( ( F ` x ) e. ( A \ ( F " x ) ) <-> ( F ` y ) e. ( A \ ( F " y ) ) ) )
41 38 40 imbi12d 
 |-  ( x = y -> ( ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) <-> ( ( A \ ( F " y ) ) =/= (/) -> ( F ` y ) e. ( A \ ( F " y ) ) ) ) )
42 41 rspcv 
 |-  ( y e. On -> ( A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) -> ( ( A \ ( F " y ) ) =/= (/) -> ( F ` y ) e. ( A \ ( F " y ) ) ) ) )
43 2 42 syl5bi 
 |-  ( y e. On -> ( ph -> ( ( A \ ( F " y ) ) =/= (/) -> ( F ` y ) e. ( A \ ( F " y ) ) ) ) )
44 43 com23 
 |-  ( y e. On -> ( ( A \ ( F " y ) ) =/= (/) -> ( ph -> ( F ` y ) e. ( A \ ( F " y ) ) ) ) )
45 37 44 syl 
 |-  ( ( x e. On /\ y e. x ) -> ( ( A \ ( F " y ) ) =/= (/) -> ( ph -> ( F ` y ) e. ( A \ ( F " y ) ) ) ) )
46 36 45 sylcom 
 |-  ( A. y e. x ( A \ ( F " y ) ) =/= (/) -> ( ( x e. On /\ y e. x ) -> ( ph -> ( F ` y ) e. ( A \ ( F " y ) ) ) ) )
47 46 com3r 
 |-  ( ph -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) -> ( ( x e. On /\ y e. x ) -> ( F ` y ) e. ( A \ ( F " y ) ) ) ) )
48 47 imp 
 |-  ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) -> ( ( x e. On /\ y e. x ) -> ( F ` y ) e. ( A \ ( F " y ) ) ) )
49 48 expcomd 
 |-  ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) -> ( y e. x -> ( x e. On -> ( F ` y ) e. ( A \ ( F " y ) ) ) ) )
50 eldifi 
 |-  ( ( F ` y ) e. ( A \ ( F " y ) ) -> ( F ` y ) e. A )
51 eleq1 
 |-  ( ( F ` y ) = z -> ( ( F ` y ) e. A <-> z e. A ) )
52 50 51 syl5ibcom 
 |-  ( ( F ` y ) e. ( A \ ( F " y ) ) -> ( ( F ` y ) = z -> z e. A ) )
53 49 52 syl8 
 |-  ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) -> ( y e. x -> ( x e. On -> ( ( F ` y ) = z -> z e. A ) ) ) )
54 53 com34 
 |-  ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) -> ( y e. x -> ( ( F ` y ) = z -> ( x e. On -> z e. A ) ) ) )
55 33 34 54 rexlimd 
 |-  ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) -> ( E. y e. x ( F ` y ) = z -> ( x e. On -> z e. A ) ) )
56 30 55 syl5 
 |-  ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) -> ( z e. ( F " x ) -> ( x e. On -> z e. A ) ) )
57 56 com23 
 |-  ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) -> ( x e. On -> ( z e. ( F " x ) -> z e. A ) ) )
58 57 imp 
 |-  ( ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) /\ x e. On ) -> ( z e. ( F " x ) -> z e. A ) )
59 58 ssrdv 
 |-  ( ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) /\ x e. On ) -> ( F " x ) C_ A )
60 ssdif0 
 |-  ( A C_ ( F " x ) <-> ( A \ ( F " x ) ) = (/) )
61 60 biimpri 
 |-  ( ( A \ ( F " x ) ) = (/) -> A C_ ( F " x ) )
62 59 61 anim12i 
 |-  ( ( ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) /\ x e. On ) /\ ( A \ ( F " x ) ) = (/) ) -> ( ( F " x ) C_ A /\ A C_ ( F " x ) ) )
63 eqss 
 |-  ( ( F " x ) = A <-> ( ( F " x ) C_ A /\ A C_ ( F " x ) ) )
64 62 63 sylibr 
 |-  ( ( ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) /\ x e. On ) /\ ( A \ ( F " x ) ) = (/) ) -> ( F " x ) = A )
65 onss 
 |-  ( x e. On -> x C_ On )
66 32 31 nfan 
 |-  F/ y ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph )
67 nfv 
 |-  F/ y x C_ On
68 66 67 nfan 
 |-  F/ y ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) /\ x C_ On )
69 nfv 
 |-  F/ z ( ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) /\ x C_ On ) /\ y e. x )
70 ssel 
 |-  ( x C_ On -> ( y e. x -> y e. On ) )
71 onss 
 |-  ( y e. On -> y C_ On )
72 1 fndmi 
 |-  dom F = On
73 71 72 sseqtrrdi 
 |-  ( y e. On -> y C_ dom F )
74 funfvima2 
 |-  ( ( Fun F /\ y C_ dom F ) -> ( z e. y -> ( F ` z ) e. ( F " y ) ) )
75 28 73 74 sylancr 
 |-  ( y e. On -> ( z e. y -> ( F ` z ) e. ( F " y ) ) )
76 70 75 syl6 
 |-  ( x C_ On -> ( y e. x -> ( z e. y -> ( F ` z ) e. ( F " y ) ) ) )
77 35 com12 
 |-  ( y e. x -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) -> ( A \ ( F " y ) ) =/= (/) ) )
78 77 a1i 
 |-  ( x C_ On -> ( y e. x -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) -> ( A \ ( F " y ) ) =/= (/) ) ) )
79 70 78 44 syl10 
 |-  ( x C_ On -> ( y e. x -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) -> ( ph -> ( F ` y ) e. ( A \ ( F " y ) ) ) ) ) )
80 79 imp4a 
 |-  ( x C_ On -> ( y e. x -> ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) -> ( F ` y ) e. ( A \ ( F " y ) ) ) ) )
81 eldifn 
 |-  ( ( F ` y ) e. ( A \ ( F " y ) ) -> -. ( F ` y ) e. ( F " y ) )
82 eleq1a 
 |-  ( ( F ` z ) e. ( F " y ) -> ( ( F ` y ) = ( F ` z ) -> ( F ` y ) e. ( F " y ) ) )
83 82 con3d 
 |-  ( ( F ` z ) e. ( F " y ) -> ( -. ( F ` y ) e. ( F " y ) -> -. ( F ` y ) = ( F ` z ) ) )
84 81 83 syl5com 
 |-  ( ( F ` y ) e. ( A \ ( F " y ) ) -> ( ( F ` z ) e. ( F " y ) -> -. ( F ` y ) = ( F ` z ) ) )
85 80 84 syl8 
 |-  ( x C_ On -> ( y e. x -> ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) -> ( ( F ` z ) e. ( F " y ) -> -. ( F ` y ) = ( F ` z ) ) ) ) )
86 85 com34 
 |-  ( x C_ On -> ( y e. x -> ( ( F ` z ) e. ( F " y ) -> ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) -> -. ( F ` y ) = ( F ` z ) ) ) ) )
87 76 86 syldd 
 |-  ( x C_ On -> ( y e. x -> ( z e. y -> ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) -> -. ( F ` y ) = ( F ` z ) ) ) ) )
88 87 com4r 
 |-  ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) -> ( x C_ On -> ( y e. x -> ( z e. y -> -. ( F ` y ) = ( F ` z ) ) ) ) )
89 88 imp31 
 |-  ( ( ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) /\ x C_ On ) /\ y e. x ) -> ( z e. y -> -. ( F ` y ) = ( F ` z ) ) )
90 69 89 ralrimi 
 |-  ( ( ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) /\ x C_ On ) /\ y e. x ) -> A. z e. y -. ( F ` y ) = ( F ` z ) )
91 90 ex 
 |-  ( ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) /\ x C_ On ) -> ( y e. x -> A. z e. y -. ( F ` y ) = ( F ` z ) ) )
92 68 91 ralrimi 
 |-  ( ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) /\ x C_ On ) -> A. y e. x A. z e. y -. ( F ` y ) = ( F ` z ) )
93 92 ex 
 |-  ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) -> ( x C_ On -> A. y e. x A. z e. y -. ( F ` y ) = ( F ` z ) ) )
94 93 ancld 
 |-  ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) -> ( x C_ On -> ( x C_ On /\ A. y e. x A. z e. y -. ( F ` y ) = ( F ` z ) ) ) )
95 1 tz7.48lem 
 |-  ( ( x C_ On /\ A. y e. x A. z e. y -. ( F ` y ) = ( F ` z ) ) -> Fun `' ( F |` x ) )
96 65 94 95 syl56 
 |-  ( ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ph ) -> ( x e. On -> Fun `' ( F |` x ) ) )
97 96 ancoms 
 |-  ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) -> ( x e. On -> Fun `' ( F |` x ) ) )
98 97 imp 
 |-  ( ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) /\ x e. On ) -> Fun `' ( F |` x ) )
99 98 adantr 
 |-  ( ( ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) /\ x e. On ) /\ ( A \ ( F " x ) ) = (/) ) -> Fun `' ( F |` x ) )
100 26 64 99 3jca 
 |-  ( ( ( ( ph /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) /\ x e. On ) /\ ( A \ ( F " x ) ) = (/) ) -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) )
101 100 exp41 
 |-  ( ph -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) -> ( x e. On -> ( ( A \ ( F " x ) ) = (/) -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) ) ) ) )
102 101 com23 
 |-  ( ph -> ( x e. On -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) -> ( ( A \ ( F " x ) ) = (/) -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) ) ) ) )
103 102 com34 
 |-  ( ph -> ( x e. On -> ( ( A \ ( F " x ) ) = (/) -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) ) ) ) )
104 103 imp4a 
 |-  ( ph -> ( x e. On -> ( ( ( A \ ( F " x ) ) = (/) /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) -> ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) ) ) )
105 25 104 reximdai 
 |-  ( ph -> ( E. x e. On ( ( A \ ( F " x ) ) = (/) /\ A. y e. x ( A \ ( F " y ) ) =/= (/) ) -> E. x e. On ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) ) )
106 23 105 syld 
 |-  ( ph -> ( A e. B -> E. x e. On ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) ) )
107 106 impcom 
 |-  ( ( A e. B /\ ph ) -> E. x e. On ( A. y e. x ( A \ ( F " y ) ) =/= (/) /\ ( F " x ) = A /\ Fun `' ( F |` x ) ) )