MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dfac2 Unicode version

Theorem dfac2 7759
Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 8090). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 7313 and preleq 7320 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 7758.) TODO: Fix label in comment, and put label changes into list at top of set.mm. (Contributed by NM, 5-Apr-2004.) (Revised by Mario Carneiro, 26-Jun-2015.)
Assertion
Ref Expression
dfac2  |-  (CHOICE  <->  A. x E. y A. z  e.  x  ( z  =/=  (/)  ->  E! w  e.  z  E. v  e.  y  ( z  e.  v  /\  w  e.  v ) ) )
Distinct variable group:    x, y, z, w, v

Proof of Theorem dfac2
Dummy variables  u  f  g are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfac3 7750 . . 3  |-  (CHOICE  <->  A. x E. f A. z  e.  x  ( z  =/=  (/)  ->  ( f `  z )  e.  z ) )
2 nfra1 2595 . . . . . . 7  |-  F/ z A. z  e.  x  ( z  =/=  (/)  ->  (
f `  z )  e.  z )
3 rsp 2605 . . . . . . . . . . . . 13  |-  ( A. z  e.  x  (
z  =/=  (/)  ->  (
f `  z )  e.  z )  ->  (
z  e.  x  -> 
( z  =/=  (/)  ->  (
f `  z )  e.  z ) ) )
4 eqid 2285 . . . . . . . . . . . . . . . . . . 19  |-  z  =  z
5 neeq1 2456 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  (
u  =/=  (/)  <->  z  =/=  (/) ) )
6 eqeq1 2291 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  (
u  =  z  <->  z  =  z ) )
75, 6anbi12d 691 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  z  ->  (
( u  =/=  (/)  /\  u  =  z )  <->  ( z  =/=  (/)  /\  z  =  z ) ) )
87rspcev 2886 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  x  /\  ( z  =/=  (/)  /\  z  =  z ) )  ->  E. u  e.  x  ( u  =/=  (/)  /\  u  =  z ) )
94, 8mpanr2 665 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  e.  x  /\  z  =/=  (/) )  ->  E. u  e.  x  ( u  =/=  (/)  /\  u  =  z ) )
10 fveq2 5527 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  z  ->  (
f `  u )  =  ( f `  z ) )
1110preq1d 3714 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  { ( f `  u ) ,  u }  =  { ( f `  z ) ,  u } )
12 preq2 3709 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  { ( f `  z ) ,  u }  =  { ( f `  z ) ,  z } )
1311, 12eqtr2d 2318 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  z  ->  { ( f `  z ) ,  z }  =  { ( f `  u ) ,  u } )
1413anim2i 552 . . . . . . . . . . . . . . . . . . 19  |-  ( ( u  =/=  (/)  /\  u  =  z )  -> 
( u  =/=  (/)  /\  {
( f `  z
) ,  z }  =  { ( f `
 u ) ,  u } ) )
1514reximi 2652 . . . . . . . . . . . . . . . . . 18  |-  ( E. u  e.  x  ( u  =/=  (/)  /\  u  =  z )  ->  E. u  e.  x  ( u  =/=  (/)  /\  {
( f `  z
) ,  z }  =  { ( f `
 u ) ,  u } ) )
169, 15syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( z  e.  x  /\  z  =/=  (/) )  ->  E. u  e.  x  ( u  =/=  (/)  /\  { ( f `  z ) ,  z }  =  { ( f `  u ) ,  u } ) )
17 prex 4219 . . . . . . . . . . . . . . . . . 18  |-  { ( f `  z ) ,  z }  e.  _V
18 eqeq1 2291 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  { ( f `
 z ) ,  z }  ->  (
g  =  { ( f `  u ) ,  u }  <->  { (
f `  z ) ,  z }  =  { ( f `  u ) ,  u } ) )
1918anbi2d 684 . . . . . . . . . . . . . . . . . . 19  |-  ( g  =  { ( f `
 z ) ,  z }  ->  (
( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  <->  ( u  =/=  (/)  /\  { ( f `  z ) ,  z }  =  { ( f `  u ) ,  u } ) ) )
2019rexbidv 2566 . . . . . . . . . . . . . . . . . 18  |-  ( g  =  { ( f `
 z ) ,  z }  ->  ( E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  <->  E. u  e.  x  ( u  =/=  (/)  /\  { ( f `  z ) ,  z }  =  { ( f `  u ) ,  u } ) ) )
2117, 20elab 2916 . . . . . . . . . . . . . . . . 17  |-  ( { ( 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 } ) )
2216, 21sylibr 203 . . . . . . . . . . . . . . . 16  |-  ( ( z  e.  x  /\  z  =/=  (/) )  ->  { ( f `  z ) ,  z }  e.  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } ) } )
23 vex 2793 . . . . . . . . . . . . . . . . . 18  |-  z  e. 
_V
2423prid2 3737 . . . . . . . . . . . . . . . . 17  |-  z  e. 
{ ( f `  z ) ,  z }
25 fvex 5541 . . . . . . . . . . . . . . . . . 18  |-  ( f `
 z )  e. 
_V
2625prid1 3736 . . . . . . . . . . . . . . . . 17  |-  ( f `
 z )  e. 
{ ( f `  z ) ,  z }
2724, 26pm3.2i 441 . . . . . . . . . . . . . . . 16  |-  ( z  e.  { ( f `
 z ) ,  z }  /\  (
f `  z )  e.  { ( f `  z ) ,  z } )
28 eleq2 2346 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  { ( f `
 z ) ,  z }  ->  (
z  e.  v  <->  z  e.  { ( f `  z
) ,  z } ) )
29 eleq2 2346 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  { ( f `
 z ) ,  z }  ->  (
( f `  z
)  e.  v  <->  ( f `  z )  e.  {
( f `  z
) ,  z } ) )
3028, 29anbi12d 691 . . . . . . . . . . . . . . . . 17  |-  ( v  =  { ( f `
 z ) ,  z }  ->  (
( z  e.  v  /\  ( f `  z )  e.  v )  <->  ( z  e. 
{ ( f `  z ) ,  z }  /\  ( f `
 z )  e. 
{ ( f `  z ) ,  z } ) ) )
3130rspcev 2886 . . . . . . . . . . . . . . . 16  |-  ( ( { ( 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 ) )
3222, 27, 31sylancl 643 . . . . . . . . . . . . . . 15  |-  ( ( 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 2345 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( f `  z )  ->  (
w  e.  z  <->  ( f `  z )  e.  z ) )
34 eleq1 2345 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  ( f `  z )  ->  (
w  e.  v  <->  ( f `  z )  e.  v ) )
3534anbi2d 684 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  ( f `  z )  ->  (
( z  e.  v  /\  w  e.  v )  <->  ( z  e.  v  /\  ( f `
 z )  e.  v ) ) )
3635rexbidv 2566 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) )
3733, 36anbi12d 691 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) ) )
3825, 37spcev 2877 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 )
) )
3932, 38sylan2 460 . . . . . . . . . . . . . 14  |-  ( ( ( 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 )
) )
4039ex 423 . . . . . . . . . . . . 13  |-  ( ( 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 )
) ) )
413, 40syl8 65 . . . . . . . . . . . 12  |-  ( 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 )
) ) ) ) )
4241imp3a 420 . . . . . . . . . . 11  |-  ( 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 )
) ) ) )
4342pm2.43d 44 . . . . . . . . . 10  |-  ( 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 2551 . . . . . . . . . . . . . 14  |-  ( 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 2793 . . . . . . . . . . . . . . . . . . . 20  |-  v  e. 
_V
46 eqeq1 2291 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  =  v  ->  (
g  =  { ( f `  u ) ,  u }  <->  v  =  { ( f `  u ) ,  u } ) )
4746anbi2d 684 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  v  ->  (
( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  <->  ( u  =/=  (/)  /\  v  =  { ( f `  u ) ,  u } ) ) )
4847rexbidv 2566 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  v  ->  ( E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  <->  E. u  e.  x  ( u  =/=  (/)  /\  v  =  { ( f `  u ) ,  u } ) ) )
4945, 48elab 2916 . . . . . . . . . . . . . . . . . . 19  |-  ( v  e.  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } ) }  <->  E. u  e.  x  ( u  =/=  (/)  /\  v  =  { ( f `  u ) ,  u } ) )
50 neeq1 2456 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  u  ->  (
z  =/=  (/)  <->  u  =/=  (/) ) )
51 fveq2 5527 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  u  ->  (
f `  z )  =  ( f `  u ) )
5251eleq1d 2351 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  u  ->  (
( f `  z
)  e.  z  <->  ( f `  u )  e.  z ) )
53 eleq2 2346 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  u  ->  (
( f `  u
)  e.  z  <->  ( f `  u )  e.  u
) )
5452, 53bitrd 244 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  u  ->  (
( f `  z
)  e.  z  <->  ( f `  u )  e.  u
) )
5550, 54imbi12d 311 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  u  ->  (
( z  =/=  (/)  ->  (
f `  z )  e.  z )  <->  ( u  =/=  (/)  ->  ( f `  u )  e.  u
) ) )
5655rspccv 2883 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. z  e.  x  (
z  =/=  (/)  ->  (
f `  z )  e.  z )  ->  (
u  e.  x  -> 
( u  =/=  (/)  ->  (
f `  u )  e.  u ) ) )
57 elirrv 7313 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  -.  w  e.  w
58 eleq2 2346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w  =  z  ->  (
w  e.  w  <->  w  e.  z ) )
5957, 58mtbii 293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  =  z  ->  -.  w  e.  z )
6059con2i 112 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  e.  z  ->  -.  w  =  z )
61 vex 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  w  e. 
_V
62 fvex 5541 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f `
 u )  e. 
_V
63 vex 2793 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  u  e. 
_V
6461, 23, 62, 63prel12 3791 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( -.  w  =  z  -> 
( { w ,  z }  =  {
( f `  u
) ,  u }  <->  ( w  e.  { ( f `  u ) ,  u }  /\  z  e.  { (
f `  u ) ,  u } ) ) )
65 ancom 437 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( w  e.  v  /\  z  e.  v )  <->  ( z  e.  v  /\  w  e.  v )
)
66 eleq2 2346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
w  e.  v  <->  w  e.  { ( f `  u
) ,  u }
) )
67 eleq2 2346 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
z  e.  v  <->  z  e.  { ( f `  u
) ,  u }
) )
6866, 67anbi12d 691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
( w  e.  v  /\  z  e.  v )  <->  ( w  e. 
{ ( f `  u ) ,  u }  /\  z  e.  {
( f `  u
) ,  u }
) ) )
6965, 68syl5rbbr 251 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
( w  e.  {
( f `  u
) ,  u }  /\  z  e.  { ( f `  u ) ,  u } )  <-> 
( z  e.  v  /\  w  e.  v ) ) )
7064, 69sylan9bbr 681 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( v  =  { ( f `  u ) ,  u }  /\  -.  w  =  z
)  ->  ( {
w ,  z }  =  { ( f `
 u ) ,  u }  <->  ( z  e.  v  /\  w  e.  v ) ) )
7160, 70sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( v  =  { ( f `  u ) ,  u }  /\  w  e.  z )  ->  ( { w ,  z }  =  {
( f `  u
) ,  u }  <->  ( z  e.  v  /\  w  e.  v )
) )
7271adantrr 697 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( v  =  { ( f `  u ) ,  u }  /\  ( w  e.  z  /\  ( f `  u
)  e.  u ) )  ->  ( {
w ,  z }  =  { ( f `
 u ) ,  u }  <->  ( z  e.  v  /\  w  e.  v ) ) )
7372pm5.32da 622 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( 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 ) ) ) )
7461, 23, 62, 63preleq 7320 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( w  e.  z  /\  ( f `  u )  e.  u
)  /\  { w ,  z }  =  { ( f `  u ) ,  u } )  ->  (
w  =  ( f `
 u )  /\  z  =  u )
)
7573, 74syl6bir 220 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
( ( w  e.  z  /\  ( f `
 u )  e.  u )  /\  (
z  e.  v  /\  w  e.  v )
)  ->  ( w  =  ( f `  u )  /\  z  =  u ) ) )
7651eqeq2d 2296 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  u  ->  (
w  =  ( f `
 z )  <->  w  =  ( f `  u
) ) )
7776biimparc 473 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( w  =  ( f `
 u )  /\  z  =  u )  ->  w  =  ( f `
 z ) )
7875, 77syl6 29 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
( ( w  e.  z  /\  ( f `
 u )  e.  u )  /\  (
z  e.  v  /\  w  e.  v )
)  ->  w  =  ( f `  z
) ) )
7978exp4c 591 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
w  e.  z  -> 
( ( f `  u )  e.  u  ->  ( ( z  e.  v  /\  w  e.  v )  ->  w  =  ( f `  z ) ) ) ) )
8079com13 74 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f `  u )  e.  u  ->  (
w  e.  z  -> 
( v  =  {
( f `  u
) ,  u }  ->  ( ( z  e.  v  /\  w  e.  v )  ->  w  =  ( f `  z ) ) ) ) )
8156, 80syl8 65 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 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 ) ) ) ) ) ) )
8281com4r 80 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 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
) ) ) ) ) ) )
8382imp 418 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( 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
) ) ) ) ) )
8483imp4a 572 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( 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 ) ) ) ) )
8584com3l 75 . . . . . . . . . . . . . . . . . . . 20  |-  ( 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
) ) ) ) )
8685rexlimiv 2663 . . . . . . . . . . . . . . . . . . 19  |-  ( 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
) ) ) )
8749, 86sylbi 187 . . . . . . . . . . . . . . . . . 18  |-  ( 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
) ) ) )
8887exp3a 425 . . . . . . . . . . . . . . . . 17  |-  ( 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 ) ) ) ) )
8988com13 74 . . . . . . . . . . . . . . . 16  |-  ( 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
) ) ) ) )
9089imp4b 573 . . . . . . . . . . . . . . 15  |-  ( ( 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 ) ) )
9190exlimdv 1666 . . . . . . . . . . . . . 14  |-  ( ( 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 ) ) )
9244, 91syl5bi 208 . . . . . . . . . . . . 13  |-  ( ( 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 ) ) )
9392expimpd 586 . . . . . . . . . . . 12  |-  ( 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
) ) )
9493alrimiv 1619 . . . . . . . . . . 11  |-  ( 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
) ) )
95 mo2icl 2946 . . . . . . . . . . 11  |-  ( 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 )
) )
9694, 95syl 15 . . . . . . . . . 10  |-  ( 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 )
) )
9743, 96jctird 528 . . . . . . . . 9  |-  ( 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 )
) ) ) )
98 df-reu 2552 . . . . . . . . . 10  |-  ( 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 )
) )
99 eu5 2183 . . . . . . . . . 10  |-  ( 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 )
) ) )
10098, 99bitri 240 . . . . . . . . 9  |-  ( 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 )
) ) )
10197, 100syl6ibr 218 . . . . . . . 8  |-  ( 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 ) ) )
102101exp3a 425 . . . . . . 7  |-  ( 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 )
) ) )
1032, 102ralrimi 2626 . . . . . 6  |-  ( 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 )
) )
104 vex 2793 . . . . . . . . . . . 12  |-  f  e. 
_V
105104rnex 4944 . . . . . . . . . . 11  |-  ran  f  e.  _V
106 p0ex 4199 . . . . . . . . . . 11  |-  { (/) }  e.  _V
107105, 106unex 4520 . . . . . . . . . 10  |-  ( ran  f  u.  { (/) } )  e.  _V
108 vex 2793 . . . . . . . . . 10  |-  x  e. 
_V
109107, 108unex 4520 . . . . . . . . 9  |-  ( ( ran  f  u.  { (/)
} )  u.  x
)  e.  _V
110109pwex 4195 . . . . . . . 8  |-  ~P (
( ran  f  u.  {
(/) } )  u.  x
)  e.  _V
111 ssun1 3340 . . . . . . . . . . . . . . 15  |-  ( ran  f  u.  { (/) } )  C_  ( ( ran  f  u.  { (/) } )  u.  x )
112 fvrn0 5552 . . . . . . . . . . . . . . 15  |-  ( f `
 u )  e.  ( ran  f  u. 
{ (/) } )
113111, 112sselii 3179 . . . . . . . . . . . . . 14  |-  ( f `
 u )  e.  ( ( ran  f  u.  { (/) } )  u.  x )
114 elun2 3345 . . . . . . . . . . . . . 14  |-  ( u  e.  x  ->  u  e.  ( ( ran  f  u.  { (/) } )  u.  x ) )
115 prssi 3773 . . . . . . . . . . . . . 14  |-  ( ( ( f `  u
)  e.  ( ( ran  f  u.  { (/)
} )  u.  x
)  /\  u  e.  ( ( ran  f  u.  { (/) } )  u.  x ) )  ->  { ( f `  u ) ,  u }  C_  ( ( ran  f  u.  { (/) } )  u.  x ) )
116113, 114, 115sylancr 644 . . . . . . . . . . . . 13  |-  ( u  e.  x  ->  { ( f `  u ) ,  u }  C_  ( ( ran  f  u.  { (/) } )  u.  x ) )
117 prex 4219 . . . . . . . . . . . . . 14  |-  { ( f `  u ) ,  u }  e.  _V
118117elpw 3633 . . . . . . . . . . . . 13  |-  ( { ( f `  u
) ,  u }  e.  ~P ( ( ran  f  u.  { (/) } )  u.  x )  <->  { ( f `  u ) ,  u }  C_  ( ( ran  f  u.  { (/) } )  u.  x ) )
119116, 118sylibr 203 . . . . . . . . . . . 12  |-  ( u  e.  x  ->  { ( f `  u ) ,  u }  e.  ~P ( ( ran  f  u.  { (/) } )  u.  x ) )
120 eleq1 2345 . . . . . . . . . . . 12  |-  ( g  =  { ( f `
 u ) ,  u }  ->  (
g  e.  ~P (
( ran  f  u.  {
(/) } )  u.  x
)  <->  { ( f `  u ) ,  u }  e.  ~P (
( ran  f  u.  {
(/) } )  u.  x
) ) )
121119, 120syl5ibrcom 213 . . . . . . . . . . 11  |-  ( u  e.  x  ->  (
g  =  { ( f `  u ) ,  u }  ->  g  e.  ~P ( ( ran  f  u.  { (/)
} )  u.  x
) ) )
122121adantld 453 . . . . . . . . . 10  |-  ( u  e.  x  ->  (
( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  ->  g  e.  ~P ( ( ran  f  u.  { (/) } )  u.  x ) ) )
123122rexlimiv 2663 . . . . . . . . 9  |-  ( E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  ->  g  e.  ~P ( ( ran  f  u.  { (/) } )  u.  x ) )
124123abssi 3250 . . . . . . . 8  |-  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  {
( f `  u
) ,  u }
) }  C_  ~P ( ( ran  f  u.  { (/) } )  u.  x )
125110, 124ssexi 4161 . . . . . . 7  |-  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  {
( f `  u
) ,  u }
) }  e.  _V
126 rexeq 2739 . . . . . . . . . 10  |-  ( 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 )
) )
127126reubidv 2726 . . . . . . . . 9  |-  ( 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 )
) )
128127imbi2d 307 . . . . . . . 8  |-  ( 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 )
) ) )
129128ralbidv 2565 . . . . . . 7  |-  ( 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 )
) ) )
130125, 129spcev 2877 . . . . . 6  |-  ( 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 )
) )
131103, 130syl 15 . . . . 5  |-  ( 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 )
) )
132131exlimiv 1668 . . . 4  |-  ( 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 )
) )
133132alimi 1548 . . 3  |-  ( 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 ) ) )
1341, 133sylbi 187 . 2  |-  (CHOICE  ->  A. x E. y A. z  e.  x  ( z  =/=  (/)  ->  E! w  e.  z  E. v  e.  y  ( z  e.  v  /\  w  e.  v ) ) )
135 dfac2a 7758 . 2  |-  ( A. x E. y A. z  e.  x  ( z  =/=  (/)  ->  E! w  e.  z  E. v  e.  y  ( z  e.  v  /\  w  e.  v ) )  -> CHOICE )
136134, 135impbii 180 1  |-  (CHOICE  <->  A. x E. y A. z  e.  x  ( z  =/=  (/)  ->  E! w  e.  z  E. v  e.  y  ( z  e.  v  /\  w  e.  v ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 176    /\ wa 358   A.wal 1529   E.wex 1530    = wceq 1625    e. wcel 1686   E!weu 2145   E*wmo 2146   {cab 2271    =/= wne 2448   A.wral 2545   E.wrex 2546   E!wreu 2547    u. cun 3152    C_ wss 3154   (/)c0 3457   ~Pcpw 3627   {csn 3642   {cpr 3643   ran crn 4692   ` cfv 5257  CHOICEwac 7744
This theorem is referenced by:  dfac7  7760
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1535  ax-5 1546  ax-17 1605  ax-9 1637  ax-8 1645  ax-13 1688  ax-14 1690  ax-6 1705  ax-7 1710  ax-11 1717  ax-12 1868  ax-ext 2266  ax-sep 4143  ax-nul 4151  ax-pow 4190  ax-pr 4216  ax-un 4514  ax-reg 7308
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1531  df-nf 1534  df-sb 1632  df-eu 2149  df-mo 2150  df-clab 2272  df-cleq 2278  df-clel 2281  df-nfc 2410  df-ne 2450  df-ral 2550  df-rex 2551  df-reu 2552  df-rab 2554  df-v 2792  df-sbc 2994  df-dif 3157  df-un 3159  df-in 3161  df-ss 3168  df-nul 3458  df-if 3568  df-pw 3629  df-sn 3648  df-pr 3649  df-op 3651  df-uni 3830  df-br 4026  df-opab 4080  df-mpt 4081  df-eprel 4307  df-id 4311  df-fr 4354  df-xp 4697  df-rel 4698  df-cnv 4699  df-co 4700  df-dm 4701  df-rn 4702  df-res 4703  df-ima 4704  df-iota 5221  df-fun 5259  df-fn 5260  df-f 5261  df-fv 5265  df-riota 6306  df-ac 7745
  Copyright terms: Public domain W3C validator