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

Theorem dfac2 7844
Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 8175). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 7398 and preleq 7405 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 7843.) 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 7835 . . 3  |-  (CHOICE  <->  A. x E. f A. z  e.  x  ( z  =/=  (/)  ->  ( f `  z )  e.  z ) )
2 nfra1 2669 . . . . . . 7  |-  F/ z A. z  e.  x  ( z  =/=  (/)  ->  (
f `  z )  e.  z )
3 rsp 2679 . . . . . . . . . . . . 13  |-  ( A. z  e.  x  (
z  =/=  (/)  ->  (
f `  z )  e.  z )  ->  (
z  e.  x  -> 
( z  =/=  (/)  ->  (
f `  z )  e.  z ) ) )
4 eqid 2358 . . . . . . . . . . . . . . . . . . 19  |-  z  =  z
5 neeq1 2529 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  (
u  =/=  (/)  <->  z  =/=  (/) ) )
6 eqeq1 2364 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  (
u  =  z  <->  z  =  z ) )
75, 6anbi12d 691 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  z  ->  (
( u  =/=  (/)  /\  u  =  z )  <->  ( z  =/=  (/)  /\  z  =  z ) ) )
87rspcev 2960 . . . . . . . . . . . . . . . . . . 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 5605 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  z  ->  (
f `  u )  =  ( f `  z ) )
1110preq1d 3788 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  { ( f `  u ) ,  u }  =  { ( f `  z ) ,  u } )
12 preq2 3783 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  { ( f `  z ) ,  u }  =  { ( f `  z ) ,  z } )
1311, 12eqtr2d 2391 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  z  ->  { ( f `  z ) ,  z }  =  { ( f `  u ) ,  u } )
1413anim2i 552 . . . . . . . . . . . . . . . . . . 19  |-  ( ( u  =/=  (/)  /\  u  =  z )  -> 
( u  =/=  (/)  /\  {
( f `  z
) ,  z }  =  { ( f `
 u ) ,  u } ) )
1514reximi 2726 . . . . . . . . . . . . . . . . . 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 4296 . . . . . . . . . . . . . . . . . 18  |-  { ( f `  z ) ,  z }  e.  _V
18 eqeq1 2364 . . . . . . . . . . . . . . . . . . . 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 2640 . . . . . . . . . . . . . . . . . 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 2990 . . . . . . . . . . . . . . . . 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 2867 . . . . . . . . . . . . . . . . . 18  |-  z  e. 
_V
2423prid2 3811 . . . . . . . . . . . . . . . . 17  |-  z  e. 
{ ( f `  z ) ,  z }
25 fvex 5619 . . . . . . . . . . . . . . . . . 18  |-  ( f `
 z )  e. 
_V
2625prid1 3810 . . . . . . . . . . . . . . . . 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 2419 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  { ( f `
 z ) ,  z }  ->  (
z  e.  v  <->  z  e.  { ( f `  z
) ,  z } ) )
29 eleq2 2419 . . . . . . . . . . . . . . . . . 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 2960 . . . . . . . . . . . . . . . 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 2418 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( f `  z )  ->  (
w  e.  z  <->  ( f `  z )  e.  z ) )
34 eleq1 2418 . . . . . . . . . . . . . . . . . . 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 2640 . . . . . . . . . . . . . . . . 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 2951 . . . . . . . . . . . . . . 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 2625 . . . . . . . . . . . . . 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 2867 . . . . . . . . . . . . . . . . . . . 20  |-  v  e. 
_V
46 eqeq1 2364 . . . . . . . . . . . . . . . . . . . . . 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 2640 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  v  ->  ( E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  <->  E. u  e.  x  ( u  =/=  (/)  /\  v  =  { ( f `  u ) ,  u } ) ) )
4945, 48elab 2990 . . . . . . . . . . . . . . . . . . 19  |-  ( v  e.  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } ) }  <->  E. u  e.  x  ( u  =/=  (/)  /\  v  =  { ( f `  u ) ,  u } ) )
50 neeq1 2529 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  u  ->  (
z  =/=  (/)  <->  u  =/=  (/) ) )
51 fveq2 5605 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  u  ->  (
f `  z )  =  ( f `  u ) )
5251eleq1d 2424 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  u  ->  (
( f `  z
)  e.  z  <->  ( f `  u )  e.  z ) )
53 eleq2 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2957 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. z  e.  x  (
z  =/=  (/)  ->  (
f `  z )  e.  z )  ->  (
u  e.  x  -> 
( u  =/=  (/)  ->  (
f `  u )  e.  u ) ) )
57 elirrv 7398 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  -.  w  e.  w
58 eleq2 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  w  e. 
_V
62 fvex 5619 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f `
 u )  e. 
_V
63 vex 2867 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  u  e. 
_V
6461, 23, 62, 63prel12 3868 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
w  e.  v  <->  w  e.  { ( f `  u
) ,  u }
) )
67 eleq2 2419 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7405 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2369 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2737 . . . . . . . . . . . . . . . . . . 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 1636 . . . . . . . . . . . . . 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 1631 . . . . . . . . . . 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 3020 . . . . . . . . . . 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 2626 . . . . . . . . . 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 2247 . . . . . . . . . 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 2700 . . . . . 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 2867 . . . . . . . . . . . 12  |-  f  e. 
_V
105104rnex 5021 . . . . . . . . . . 11  |-  ran  f  e.  _V
106 p0ex 4276 . . . . . . . . . . 11  |-  { (/) }  e.  _V
107105, 106unex 4597 . . . . . . . . . 10  |-  ( ran  f  u.  { (/) } )  e.  _V
108 vex 2867 . . . . . . . . . 10  |-  x  e. 
_V
109107, 108unex 4597 . . . . . . . . 9  |-  ( ( ran  f  u.  { (/)
} )  u.  x
)  e.  _V
110109pwex 4272 . . . . . . . 8  |-  ~P (
( ran  f  u.  {
(/) } )  u.  x
)  e.  _V
111 ssun1 3414 . . . . . . . . . . . . . . 15  |-  ( ran  f  u.  { (/) } )  C_  ( ( ran  f  u.  { (/) } )  u.  x )
112 fvrn0 5630 . . . . . . . . . . . . . . 15  |-  ( f `
 u )  e.  ( ran  f  u. 
{ (/) } )
113111, 112sselii 3253 . . . . . . . . . . . . . 14  |-  ( f `
 u )  e.  ( ( ran  f  u.  { (/) } )  u.  x )
114 elun2 3419 . . . . . . . . . . . . . 14  |-  ( u  e.  x  ->  u  e.  ( ( ran  f  u.  { (/) } )  u.  x ) )
115 prssi 3850 . . . . . . . . . . . . . 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 4296 . . . . . . . . . . . . . 14  |-  { ( f `  u ) ,  u }  e.  _V
118117elpw 3707 . . . . . . . . . . . . 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 2418 . . . . . . . . . . . 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 2737 . . . . . . . . 9  |-  ( E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  ->  g  e.  ~P ( ( ran  f  u.  { (/) } )  u.  x ) )
124123abssi 3324 . . . . . . . 8  |-  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  {
( f `  u
) ,  u }
) }  C_  ~P ( ( ran  f  u.  { (/) } )  u.  x )
125110, 124ssexi 4238 . . . . . . 7  |-  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  {
( f `  u
) ,  u }
) }  e.  _V
126 rexeq 2813 . . . . . . . . . 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 2800 . . . . . . . . 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 2639 . . . . . . 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 2951 . . . . . 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 1634 . . . 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 1559 . . 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 7843 . 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 1540   E.wex 1541    = wceq 1642    e. wcel 1710   E!weu 2209   E*wmo 2210   {cab 2344    =/= wne 2521   A.wral 2619   E.wrex 2620   E!wreu 2621    u. cun 3226    C_ wss 3228   (/)c0 3531   ~Pcpw 3701   {csn 3716   {cpr 3717   ran crn 4769   ` cfv 5334  CHOICEwac 7829
This theorem is referenced by:  dfac7  7845
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4220  ax-nul 4228  ax-pow 4267  ax-pr 4293  ax-un 4591  ax-reg 7393
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-op 3725  df-uni 3907  df-br 4103  df-opab 4157  df-mpt 4158  df-eprel 4384  df-id 4388  df-fr 4431  df-xp 4774  df-rel 4775  df-cnv 4776  df-co 4777  df-dm 4778  df-rn 4779  df-res 4780  df-ima 4781  df-iota 5298  df-fun 5336  df-fn 5337  df-f 5338  df-fv 5342  df-riota 6388  df-ac 7830
  Copyright terms: Public domain W3C validator