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 syl6bir
 |-  ( 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 syl5bi
 |-  ( ( 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 syl6ibr
 |-  ( 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 ) ) )