Metamath Proof Explorer

Theorem dfac2b

Description: Axiom of Choice (first form) of Enderton p. 49 implies our Axiom of Choice (in the form of ac3 ). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elneq and preleq that are referenced in the proof each make use of Regularity for their derivations. (The reverse implication can be derived without using Regularity; see dfac2a .) (Contributed by NM, 5-Apr-2004) (Revised by Mario Carneiro, 26-Jun-2015) (Revised by AV, 16-Jun-2022)

Ref Expression
Assertion dfac2b 
|- ( CHOICE -> A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )

Proof

Step Hyp Ref Expression
1 dfac3 
 |-  ( CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) )
2 nfra1 
 |-  F/ z A. z e. x ( z =/= (/) -> ( f ` z ) e. z )
3 rsp 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( z e. x -> ( z =/= (/) -> ( f ` z ) e. z ) ) )
4 equid 
 |-  z = z
5 neeq1 
 |-  ( u = z -> ( u =/= (/) <-> z =/= (/) ) )
6 eqeq1 
 |-  ( u = z -> ( u = z <-> z = z ) )
7 5 6 anbi12d 
 |-  ( u = z -> ( ( u =/= (/) /\ u = z ) <-> ( z =/= (/) /\ z = z ) ) )
8 7 rspcev 
 |-  ( ( z e. x /\ ( z =/= (/) /\ z = z ) ) -> E. u e. x ( u =/= (/) /\ u = z ) )
9 4 8 mpanr2 
 |-  ( ( z e. x /\ z =/= (/) ) -> E. u e. x ( u =/= (/) /\ u = z ) )
10 fveq2 
 |-  ( u = z -> ( f ` u ) = ( f ` z ) )
11 10 preq1d 
 |-  ( u = z -> { ( f ` u ) , u } = { ( f ` z ) , u } )
12 preq2 
 |-  ( u = z -> { ( f ` z ) , u } = { ( f ` z ) , z } )
13 11 12 eqtr2d 
 |-  ( u = z -> { ( f ` z ) , z } = { ( f ` u ) , u } )
14 13 anim2i 
 |-  ( ( u =/= (/) /\ u = z ) -> ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) )
15 14 reximi 
 |-  ( E. u e. x ( u =/= (/) /\ u = z ) -> E. u e. x ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) )
16 9 15 syl 
 |-  ( ( z e. x /\ z =/= (/) ) -> E. u e. x ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) )
17 prex 
 |-  { ( f ` z ) , z } e. _V
18 eqeq1 
 |-  ( g = { ( f ` z ) , z } -> ( g = { ( f ` u ) , u } <-> { ( f ` z ) , z } = { ( f ` u ) , u } ) )
19 18 anbi2d 
 |-  ( g = { ( f ` z ) , z } -> ( ( u =/= (/) /\ g = { ( f ` u ) , u } ) <-> ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) ) )
20 19 rexbidv 
 |-  ( g = { ( f ` z ) , z } -> ( E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) <-> E. u e. x ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) ) )
21 17 20 elab 
 |-  ( { ( f ` z ) , z } e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } <-> E. u e. x ( u =/= (/) /\ { ( f ` z ) , z } = { ( f ` u ) , u } ) )
22 16 21 sylibr 
 |-  ( ( z e. x /\ z =/= (/) ) -> { ( f ` z ) , z } e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } )
23 vex 
 |-  z e. _V
24 23 prid2 
 |-  z e. { ( f ` z ) , z }
25 fvex 
 |-  ( f ` z ) e. _V
26 25 prid1 
 |-  ( f ` z ) e. { ( f ` z ) , z }
27 24 26 pm3.2i 
 |-  ( z e. { ( f ` z ) , z } /\ ( f ` z ) e. { ( f ` z ) , z } )
28 eleq2 
 |-  ( v = { ( f ` z ) , z } -> ( z e. v <-> z e. { ( f ` z ) , z } ) )
29 eleq2 
 |-  ( v = { ( f ` z ) , z } -> ( ( f ` z ) e. v <-> ( f ` z ) e. { ( f ` z ) , z } ) )
30 28 29 anbi12d 
 |-  ( v = { ( f ` z ) , z } -> ( ( z e. v /\ ( f ` z ) e. v ) <-> ( z e. { ( f ` z ) , z } /\ ( f ` z ) e. { ( f ` z ) , z } ) ) )
31 30 rspcev 
 |-  ( ( { ( f ` z ) , z } e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } /\ ( z e. { ( f ` z ) , z } /\ ( f ` z ) e. { ( f ` z ) , z } ) ) -> E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ ( f ` z ) e. v ) )
32 22 27 31 sylancl 
 |-  ( ( z e. x /\ z =/= (/) ) -> E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ ( f ` z ) e. v ) )
33 eleq1 
 |-  ( w = ( f ` z ) -> ( w e. z <-> ( f ` z ) e. z ) )
34 eleq1 
 |-  ( w = ( f ` z ) -> ( w e. v <-> ( f ` z ) e. v ) )
35 34 anbi2d 
 |-  ( w = ( f ` z ) -> ( ( z e. v /\ w e. v ) <-> ( z e. v /\ ( f ` z ) e. v ) ) )
36 35 rexbidv 
 |-  ( w = ( f ` z ) -> ( E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) <-> E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ ( f ` z ) e. v ) ) )
37 33 36 anbi12d 
 |-  ( w = ( f ` z ) -> ( ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) <-> ( ( f ` z ) e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ ( f ` z ) e. v ) ) ) )
38 25 37 spcev 
 |-  ( ( ( f ` z ) e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ ( f ` z ) e. v ) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
39 32 38 sylan2 
 |-  ( ( ( f ` z ) e. z /\ ( z e. x /\ z =/= (/) ) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
40 39 ex 
 |-  ( ( f ` z ) e. z -> ( ( z e. x /\ z =/= (/) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
41 3 40 syl8 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( z e. x -> ( z =/= (/) -> ( ( z e. x /\ z =/= (/) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) ) ) )
42 41 impd 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( z e. x /\ z =/= (/) ) -> ( ( z e. x /\ z =/= (/) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) ) )
43 42 pm2.43d 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( z e. x /\ z =/= (/) ) -> E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
44 df-rex 
 |-  ( E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) <-> E. v ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } /\ ( z e. v /\ w e. v ) ) )
45 vex 
 |-  v e. _V
46 eqeq1 
 |-  ( g = v -> ( g = { ( f ` u ) , u } <-> v = { ( f ` u ) , u } ) )
47 46 anbi2d 
 |-  ( g = v -> ( ( u =/= (/) /\ g = { ( f ` u ) , u } ) <-> ( u =/= (/) /\ v = { ( f ` u ) , u } ) ) )
48 47 rexbidv 
 |-  ( g = v -> ( E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) <-> E. u e. x ( u =/= (/) /\ v = { ( f ` u ) , u } ) ) )
49 45 48 elab 
 |-  ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } <-> E. u e. x ( u =/= (/) /\ v = { ( f ` u ) , u } ) )
50 neeq1 
 |-  ( z = u -> ( z =/= (/) <-> u =/= (/) ) )
51 fveq2 
 |-  ( z = u -> ( f ` z ) = ( f ` u ) )
52 51 eleq1d 
 |-  ( z = u -> ( ( f ` z ) e. z <-> ( f ` u ) e. z ) )
53 eleq2 
 |-  ( z = u -> ( ( f ` u ) e. z <-> ( f ` u ) e. u ) )
54 52 53 bitrd 
 |-  ( z = u -> ( ( f ` z ) e. z <-> ( f ` u ) e. u ) )
55 50 54 imbi12d 
 |-  ( z = u -> ( ( z =/= (/) -> ( f ` z ) e. z ) <-> ( u =/= (/) -> ( f ` u ) e. u ) ) )
56 55 rspccv 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( u e. x -> ( u =/= (/) -> ( f ` u ) e. u ) ) )
57 elneq 
 |-  ( w e. z -> w =/= z )
58 57 neneqd 
 |-  ( w e. z -> -. w = z )
59 vex 
 |-  w e. _V
60 neqne 
 |-  ( -. w = z -> w =/= z )
61 prel12g 
 |-  ( ( w e. _V /\ z e. _V /\ w =/= z ) -> ( { w , z } = { ( f ` u ) , u } <-> ( w e. { ( f ` u ) , u } /\ z e. { ( f ` u ) , u } ) ) )
62 59 23 60 61 mp3an12i 
 |-  ( -. w = z -> ( { w , z } = { ( f ` u ) , u } <-> ( w e. { ( f ` u ) , u } /\ z e. { ( f ` u ) , u } ) ) )
63 eleq2 
 |-  ( v = { ( f ` u ) , u } -> ( w e. v <-> w e. { ( f ` u ) , u } ) )
64 eleq2 
 |-  ( v = { ( f ` u ) , u } -> ( z e. v <-> z e. { ( f ` u ) , u } ) )
65 63 64 anbi12d 
 |-  ( v = { ( f ` u ) , u } -> ( ( w e. v /\ z e. v ) <-> ( w e. { ( f ` u ) , u } /\ z e. { ( f ` u ) , u } ) ) )
66 ancom 
 |-  ( ( w e. v /\ z e. v ) <-> ( z e. v /\ w e. v ) )
67 65 66 bitr3di 
 |-  ( v = { ( f ` u ) , u } -> ( ( w e. { ( f ` u ) , u } /\ z e. { ( f ` u ) , u } ) <-> ( z e. v /\ w e. v ) ) )
68 62 67 sylan9bbr 
 |-  ( ( v = { ( f ` u ) , u } /\ -. w = z ) -> ( { w , z } = { ( f ` u ) , u } <-> ( z e. v /\ w e. v ) ) )
69 58 68 sylan2 
 |-  ( ( v = { ( f ` u ) , u } /\ w e. z ) -> ( { w , z } = { ( f ` u ) , u } <-> ( z e. v /\ w e. v ) ) )
70 69 adantrr 
 |-  ( ( v = { ( f ` u ) , u } /\ ( w e. z /\ ( f ` u ) e. u ) ) -> ( { w , z } = { ( f ` u ) , u } <-> ( z e. v /\ w e. v ) ) )
71 70 pm5.32da 
 |-  ( v = { ( f ` u ) , u } -> ( ( ( w e. z /\ ( f ` u ) e. u ) /\ { w , z } = { ( f ` u ) , u } ) <-> ( ( w e. z /\ ( f ` u ) e. u ) /\ ( z e. v /\ w e. v ) ) ) )
72 23 preleq 
 |-  ( ( ( w e. z /\ ( f ` u ) e. u ) /\ { w , z } = { ( f ` u ) , u } ) -> ( w = ( f ` u ) /\ z = u ) )
73 71 72 biimtrrdi 
 |-  ( v = { ( f ` u ) , u } -> ( ( ( w e. z /\ ( f ` u ) e. u ) /\ ( z e. v /\ w e. v ) ) -> ( w = ( f ` u ) /\ z = u ) ) )
74 51 eqeq2d 
 |-  ( z = u -> ( w = ( f ` z ) <-> w = ( f ` u ) ) )
75 74 biimparc 
 |-  ( ( w = ( f ` u ) /\ z = u ) -> w = ( f ` z ) )
76 73 75 syl6 
 |-  ( v = { ( f ` u ) , u } -> ( ( ( w e. z /\ ( f ` u ) e. u ) /\ ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) )
77 76 exp4c 
 |-  ( v = { ( f ` u ) , u } -> ( w e. z -> ( ( f ` u ) e. u -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
78 77 com13 
 |-  ( ( f ` u ) e. u -> ( w e. z -> ( v = { ( f ` u ) , u } -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
79 56 78 syl8 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( u e. x -> ( u =/= (/) -> ( w e. z -> ( v = { ( f ` u ) , u } -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) ) ) )
80 79 com4r 
 |-  ( w e. z -> ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( u e. x -> ( u =/= (/) -> ( v = { ( f ` u ) , u } -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) ) ) )
81 80 imp 
 |-  ( ( w e. z /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( u e. x -> ( u =/= (/) -> ( v = { ( f ` u ) , u } -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) ) )
82 81 imp4a 
 |-  ( ( w e. z /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( u e. x -> ( ( u =/= (/) /\ v = { ( f ` u ) , u } ) -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
83 82 com3l 
 |-  ( u e. x -> ( ( u =/= (/) /\ v = { ( f ` u ) , u } ) -> ( ( w e. z /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
84 83 rexlimiv 
 |-  ( E. u e. x ( u =/= (/) /\ v = { ( f ` u ) , u } ) -> ( ( w e. z /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) )
85 49 84 sylbi 
 |-  ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( ( w e. z /\ A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) ) -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) )
86 85 expd 
 |-  ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( w e. z -> ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
87 86 com13 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( w e. z -> ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( ( z e. v /\ w e. v ) -> w = ( f ` z ) ) ) ) )
88 87 imp4b 
 |-  ( ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) /\ w e. z ) -> ( ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } /\ ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) )
89 88 exlimdv 
 |-  ( ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) /\ w e. z ) -> ( E. v ( v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } /\ ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) )
90 44 89 biimtrid 
 |-  ( ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) /\ w e. z ) -> ( E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) -> w = ( f ` z ) ) )
91 90 expimpd 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) )
92 91 alrimiv 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> A. w ( ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) )
93 mo2icl 
 |-  ( A. w ( ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) -> w = ( f ` z ) ) -> E* w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
94 92 93 syl 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E* w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
95 43 94 jctird 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( z e. x /\ z =/= (/) ) -> ( E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) /\ E* w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) ) )
96 df-reu 
 |-  ( E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) <-> E! w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
97 df-eu 
 |-  ( E! w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) <-> ( E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) /\ E* w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
98 96 97 bitri 
 |-  ( E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) <-> ( E. w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) /\ E* w ( w e. z /\ E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
99 95 98 imbitrrdi 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( ( z e. x /\ z =/= (/) ) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
100 99 expd 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> ( z e. x -> ( z =/= (/) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
101 2 100 ralrimi 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> A. z e. x ( z =/= (/) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
102 vex 
 |-  f e. _V
103 102 rnex 
 |-  ran f e. _V
104 p0ex 
 |-  { (/) } e. _V
105 103 104 unex 
 |-  ( ran f u. { (/) } ) e. _V
106 vex 
 |-  x e. _V
107 105 106 unex 
 |-  ( ( ran f u. { (/) } ) u. x ) e. _V
108 107 pwex 
 |-  ~P ( ( ran f u. { (/) } ) u. x ) e. _V
109 ssun1 
 |-  ( ran f u. { (/) } ) C_ ( ( ran f u. { (/) } ) u. x )
110 fvrn0 
 |-  ( f ` u ) e. ( ran f u. { (/) } )
111 109 110 sselii 
 |-  ( f ` u ) e. ( ( ran f u. { (/) } ) u. x )
112 elun2 
 |-  ( u e. x -> u e. ( ( ran f u. { (/) } ) u. x ) )
113 prssi 
 |-  ( ( ( f ` u ) e. ( ( ran f u. { (/) } ) u. x ) /\ u e. ( ( ran f u. { (/) } ) u. x ) ) -> { ( f ` u ) , u } C_ ( ( ran f u. { (/) } ) u. x ) )
114 111 112 113 sylancr 
 |-  ( u e. x -> { ( f ` u ) , u } C_ ( ( ran f u. { (/) } ) u. x ) )
115 prex 
 |-  { ( f ` u ) , u } e. _V
116 115 elpw 
 |-  ( { ( f ` u ) , u } e. ~P ( ( ran f u. { (/) } ) u. x ) <-> { ( f ` u ) , u } C_ ( ( ran f u. { (/) } ) u. x ) )
117 114 116 sylibr 
 |-  ( u e. x -> { ( f ` u ) , u } e. ~P ( ( ran f u. { (/) } ) u. x ) )
118 eleq1 
 |-  ( g = { ( f ` u ) , u } -> ( g e. ~P ( ( ran f u. { (/) } ) u. x ) <-> { ( f ` u ) , u } e. ~P ( ( ran f u. { (/) } ) u. x ) ) )
119 117 118 syl5ibrcom 
 |-  ( u e. x -> ( g = { ( f ` u ) , u } -> g e. ~P ( ( ran f u. { (/) } ) u. x ) ) )
120 119 adantld 
 |-  ( u e. x -> ( ( u =/= (/) /\ g = { ( f ` u ) , u } ) -> g e. ~P ( ( ran f u. { (/) } ) u. x ) ) )
121 120 rexlimiv 
 |-  ( E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) -> g e. ~P ( ( ran f u. { (/) } ) u. x ) )
122 121 abssi 
 |-  { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } C_ ~P ( ( ran f u. { (/) } ) u. x )
123 108 122 ssexi 
 |-  { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } e. _V
124 rexeq 
 |-  ( y = { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( E. v e. y ( z e. v /\ w e. v ) <-> E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
125 124 reubidv 
 |-  ( y = { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( E! w e. z E. v e. y ( z e. v /\ w e. v ) <-> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) )
126 125 imbi2d 
 |-  ( y = { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) <-> ( z =/= (/) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
127 126 ralbidv 
 |-  ( y = { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } -> ( A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) <-> A. z e. x ( z =/= (/) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) ) )
128 123 127 spcev 
 |-  ( A. z e. x ( z =/= (/) -> E! w e. z E. v e. { g | E. u e. x ( u =/= (/) /\ g = { ( f ` u ) , u } ) } ( z e. v /\ w e. v ) ) -> E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
129 101 128 syl 
 |-  ( A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
130 129 exlimiv 
 |-  ( E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
131 130 alimi 
 |-  ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. z ) -> A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )
132 1 131 sylbi 
 |-  ( CHOICE -> A. x E. y A. z e. x ( z =/= (/) -> E! w e. z E. v e. y ( z e. v /\ w e. v ) ) )