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

Theorem dfac2 8514
Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 8845). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 8026 and preleq 8037 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 8513.) 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 8505 . . 3  |-  (CHOICE  <->  A. x E. f A. z  e.  x  ( z  =/=  (/)  ->  ( f `  z )  e.  z ) )
2 nfra1 2824 . . . . . . 7  |-  F/ z A. z  e.  x  ( z  =/=  (/)  ->  (
f `  z )  e.  z )
3 rsp 2809 . . . . . . . . . . . . 13  |-  ( A. z  e.  x  (
z  =/=  (/)  ->  (
f `  z )  e.  z )  ->  (
z  e.  x  -> 
( z  =/=  (/)  ->  (
f `  z )  e.  z ) ) )
4 equid 1777 . . . . . . . . . . . . . . . . . . 19  |-  z  =  z
5 neeq1 2724 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  (
u  =/=  (/)  <->  z  =/=  (/) ) )
6 eqeq1 2447 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  (
u  =  z  <->  z  =  z ) )
75, 6anbi12d 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  z  ->  (
( u  =/=  (/)  /\  u  =  z )  <->  ( z  =/=  (/)  /\  z  =  z ) ) )
87rspcev 3196 . . . . . . . . . . . . . . . . . . 19  |-  ( ( z  e.  x  /\  ( z  =/=  (/)  /\  z  =  z ) )  ->  E. u  e.  x  ( u  =/=  (/)  /\  u  =  z ) )
94, 8mpanr2 684 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  e.  x  /\  z  =/=  (/) )  ->  E. u  e.  x  ( u  =/=  (/)  /\  u  =  z ) )
10 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  z  ->  (
f `  u )  =  ( f `  z ) )
1110preq1d 4100 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  { ( f `  u ) ,  u }  =  { ( f `  z ) ,  u } )
12 preq2 4095 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  { ( f `  z ) ,  u }  =  { ( f `  z ) ,  z } )
1311, 12eqtr2d 2485 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  z  ->  { ( f `  z ) ,  z }  =  { ( f `  u ) ,  u } )
1413anim2i 569 . . . . . . . . . . . . . . . . . . 19  |-  ( ( u  =/=  (/)  /\  u  =  z )  -> 
( u  =/=  (/)  /\  {
( f `  z
) ,  z }  =  { ( f `
 u ) ,  u } ) )
1514reximi 2911 . . . . . . . . . . . . . . . . . 18  |-  ( E. u  e.  x  ( u  =/=  (/)  /\  u  =  z )  ->  E. u  e.  x  ( u  =/=  (/)  /\  {
( f `  z
) ,  z }  =  { ( f `
 u ) ,  u } ) )
169, 15syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( z  e.  x  /\  z  =/=  (/) )  ->  E. u  e.  x  ( u  =/=  (/)  /\  { ( f `  z ) ,  z }  =  { ( f `  u ) ,  u } ) )
17 prex 4679 . . . . . . . . . . . . . . . . . 18  |-  { ( f `  z ) ,  z }  e.  _V
18 eqeq1 2447 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  { ( f `
 z ) ,  z }  ->  (
g  =  { ( f `  u ) ,  u }  <->  { (
f `  z ) ,  z }  =  { ( f `  u ) ,  u } ) )
1918anbi2d 703 . . . . . . . . . . . . . . . . . . 19  |-  ( g  =  { ( f `
 z ) ,  z }  ->  (
( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  <->  ( u  =/=  (/)  /\  { ( f `  z ) ,  z }  =  { ( f `  u ) ,  u } ) ) )
2019rexbidv 2954 . . . . . . . . . . . . . . . . . 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 3232 . . . . . . . . . . . . . . . . 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 212 . . . . . . . . . . . . . . . 16  |-  ( ( z  e.  x  /\  z  =/=  (/) )  ->  { ( f `  z ) ,  z }  e.  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } ) } )
23 vex 3098 . . . . . . . . . . . . . . . . . 18  |-  z  e. 
_V
2423prid2 4124 . . . . . . . . . . . . . . . . 17  |-  z  e. 
{ ( f `  z ) ,  z }
25 fvex 5866 . . . . . . . . . . . . . . . . . 18  |-  ( f `
 z )  e. 
_V
2625prid1 4123 . . . . . . . . . . . . . . . . 17  |-  ( f `
 z )  e. 
{ ( f `  z ) ,  z }
2724, 26pm3.2i 455 . . . . . . . . . . . . . . . 16  |-  ( z  e.  { ( f `
 z ) ,  z }  /\  (
f `  z )  e.  { ( f `  z ) ,  z } )
28 eleq2 2516 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  { ( f `
 z ) ,  z }  ->  (
z  e.  v  <->  z  e.  { ( f `  z
) ,  z } ) )
29 eleq2 2516 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  { ( f `
 z ) ,  z }  ->  (
( f `  z
)  e.  v  <->  ( f `  z )  e.  {
( f `  z
) ,  z } ) )
3028, 29anbi12d 710 . . . . . . . . . . . . . . . . 17  |-  ( v  =  { ( f `
 z ) ,  z }  ->  (
( z  e.  v  /\  ( f `  z )  e.  v )  <->  ( z  e. 
{ ( f `  z ) ,  z }  /\  ( f `
 z )  e. 
{ ( f `  z ) ,  z } ) ) )
3130rspcev 3196 . . . . . . . . . . . . . . . 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 662 . . . . . . . . . . . . . . 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 2515 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( f `  z )  ->  (
w  e.  z  <->  ( f `  z )  e.  z ) )
34 eleq1 2515 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  ( f `  z )  ->  (
w  e.  v  <->  ( f `  z )  e.  v ) )
3534anbi2d 703 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  ( f `  z )  ->  (
( z  e.  v  /\  w  e.  v )  <->  ( z  e.  v  /\  ( f `
 z )  e.  v ) ) )
3635rexbidv 2954 . . . . . . . . . . . . . . . . 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 710 . . . . . . . . . . . . . . . 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 3187 . . . . . . . . . . . . . . 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 474 . . . . . . . . . . . . . 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 434 . . . . . . . . . . . . 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 70 . . . . . . . . . . . 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 )
) ) ) ) )
4241impd 431 . . . . . . . . . . 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 48 . . . . . . . . . 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 2799 . . . . . . . . . . . . . 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 3098 . . . . . . . . . . . . . . . . . . . 20  |-  v  e. 
_V
46 eqeq1 2447 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( g  =  v  ->  (
g  =  { ( f `  u ) ,  u }  <->  v  =  { ( f `  u ) ,  u } ) )
4746anbi2d 703 . . . . . . . . . . . . . . . . . . . . 21  |-  ( g  =  v  ->  (
( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  <->  ( u  =/=  (/)  /\  v  =  { ( f `  u ) ,  u } ) ) )
4847rexbidv 2954 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  v  ->  ( E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  <->  E. u  e.  x  ( u  =/=  (/)  /\  v  =  { ( f `  u ) ,  u } ) ) )
4945, 48elab 3232 . . . . . . . . . . . . . . . . . . 19  |-  ( v  e.  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } ) }  <->  E. u  e.  x  ( u  =/=  (/)  /\  v  =  { ( f `  u ) ,  u } ) )
50 neeq1 2724 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  u  ->  (
z  =/=  (/)  <->  u  =/=  (/) ) )
51 fveq2 5856 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  u  ->  (
f `  z )  =  ( f `  u ) )
5251eleq1d 2512 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  u  ->  (
( f `  z
)  e.  z  <->  ( f `  u )  e.  z ) )
53 eleq2 2516 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  u  ->  (
( f `  u
)  e.  z  <->  ( f `  u )  e.  u
) )
5452, 53bitrd 253 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  u  ->  (
( f `  z
)  e.  z  <->  ( f `  u )  e.  u
) )
5550, 54imbi12d 320 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z  =  u  ->  (
( z  =/=  (/)  ->  (
f `  z )  e.  z )  <->  ( u  =/=  (/)  ->  ( f `  u )  e.  u
) ) )
5655rspccv 3193 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. z  e.  x  (
z  =/=  (/)  ->  (
f `  z )  e.  z )  ->  (
u  e.  x  -> 
( u  =/=  (/)  ->  (
f `  u )  e.  u ) ) )
57 elirrv 8026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  -.  w  e.  w
58 eleq2 2516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( w  =  z  ->  (
w  e.  w  <->  w  e.  z ) )
5957, 58mtbii 302 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( w  =  z  ->  -.  w  e.  z )
6059con2i 120 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( w  e.  z  ->  -.  w  =  z )
61 vex 3098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  w  e. 
_V
62 fvex 5866 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f `
 u )  e. 
_V
63 vex 3098 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  u  e. 
_V
6461, 23, 62, 63prel12 4192 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( -.  w  =  z  -> 
( { w ,  z }  =  {
( f `  u
) ,  u }  <->  ( w  e.  { ( f `  u ) ,  u }  /\  z  e.  { (
f `  u ) ,  u } ) ) )
65 ancom 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( w  e.  v  /\  z  e.  v )  <->  ( z  e.  v  /\  w  e.  v )
)
66 eleq2 2516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
w  e.  v  <->  w  e.  { ( f `  u
) ,  u }
) )
67 eleq2 2516 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
z  e.  v  <->  z  e.  { ( f `  u
) ,  u }
) )
6866, 67anbi12d 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
( w  e.  v  /\  z  e.  v )  <->  ( w  e. 
{ ( f `  u ) ,  u }  /\  z  e.  {
( f `  u
) ,  u }
) ) )
6965, 68syl5rbbr 260 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
( w  e.  {
( f `  u
) ,  u }  /\  z  e.  { ( f `  u ) ,  u } )  <-> 
( z  e.  v  /\  w  e.  v ) ) )
7064, 69sylan9bbr 700 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( v  =  { ( f `  u ) ,  u }  /\  -.  w  =  z
)  ->  ( {
w ,  z }  =  { ( f `
 u ) ,  u }  <->  ( z  e.  v  /\  w  e.  v ) ) )
7160, 70sylan2 474 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( v  =  { ( f `  u ) ,  u }  /\  w  e.  z )  ->  ( { w ,  z }  =  {
( f `  u
) ,  u }  <->  ( z  e.  v  /\  w  e.  v )
) )
7271adantrr 716 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 641 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 8037 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( w  e.  z  /\  ( f `  u )  e.  u
)  /\  { w ,  z }  =  { ( f `  u ) ,  u } )  ->  (
w  =  ( f `
 u )  /\  z  =  u )
)
7573, 74syl6bir 229 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
( ( w  e.  z  /\  ( f `
 u )  e.  u )  /\  (
z  e.  v  /\  w  e.  v )
)  ->  ( w  =  ( f `  u )  /\  z  =  u ) ) )
7651eqeq2d 2457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  u  ->  (
w  =  ( f `
 z )  <->  w  =  ( f `  u
) ) )
7776biimparc 487 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( w  =  ( f `
 u )  /\  z  =  u )  ->  w  =  ( f `
 z ) )
7875, 77syl6 33 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
( ( w  e.  z  /\  ( f `
 u )  e.  u )  /\  (
z  e.  v  /\  w  e.  v )
)  ->  w  =  ( f `  z
) ) )
7978exp4c 608 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
w  e.  z  -> 
( ( f `  u )  e.  u  ->  ( ( z  e.  v  /\  w  e.  v )  ->  w  =  ( f `  z ) ) ) ) )
8079com13 80 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( f `  u )  e.  u  ->  (
w  e.  z  -> 
( v  =  {
( f `  u
) ,  u }  ->  ( ( z  e.  v  /\  w  e.  v )  ->  w  =  ( f `  z ) ) ) ) )
8156, 80syl8 70 . . . . . . . . . . . . . . . . . . . . . . . 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 86 . . . . . . . . . . . . . . . . . . . . . . 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 429 . . . . . . . . . . . . . . . . . . . . . 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 589 . . . . . . . . . . . . . . . . . . . . 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 81 . . . . . . . . . . . . . . . . . . . 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 2929 . . . . . . . . . . . . . . . . . . 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 195 . . . . . . . . . . . . . . . . . 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
) ) ) )
8887expd 436 . . . . . . . . . . . . . . . . 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 80 . . . . . . . . . . . . . . . 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 590 . . . . . . . . . . . . . . 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 1711 . . . . . . . . . . . . . 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 217 . . . . . . . . . . . . 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 603 . . . . . . . . . . . 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 1706 . . . . . . . . . . 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 3264 . . . . . . . . . . 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 16 . . . . . . . . . 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 544 . . . . . . . . 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 2800 . . . . . . . . . 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 2296 . . . . . . . . . 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 249 . . . . . . . . 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 227 . . . . . . . 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 ) ) )
102101expd 436 . . . . . . 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 2843 . . . . . 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 3098 . . . . . . . . . . . 12  |-  f  e. 
_V
105104rnex 6719 . . . . . . . . . . 11  |-  ran  f  e.  _V
106 p0ex 4624 . . . . . . . . . . 11  |-  { (/) }  e.  _V
107105, 106unex 6583 . . . . . . . . . 10  |-  ( ran  f  u.  { (/) } )  e.  _V
108 vex 3098 . . . . . . . . . 10  |-  x  e. 
_V
109107, 108unex 6583 . . . . . . . . 9  |-  ( ( ran  f  u.  { (/)
} )  u.  x
)  e.  _V
110109pwex 4620 . . . . . . . 8  |-  ~P (
( ran  f  u.  {
(/) } )  u.  x
)  e.  _V
111 ssun1 3652 . . . . . . . . . . . . . . 15  |-  ( ran  f  u.  { (/) } )  C_  ( ( ran  f  u.  { (/) } )  u.  x )
112 fvrn0 5878 . . . . . . . . . . . . . . 15  |-  ( f `
 u )  e.  ( ran  f  u. 
{ (/) } )
113111, 112sselii 3486 . . . . . . . . . . . . . 14  |-  ( f `
 u )  e.  ( ( ran  f  u.  { (/) } )  u.  x )
114 elun2 3657 . . . . . . . . . . . . . 14  |-  ( u  e.  x  ->  u  e.  ( ( ran  f  u.  { (/) } )  u.  x ) )
115 prssi 4171 . . . . . . . . . . . . . 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 663 . . . . . . . . . . . . 13  |-  ( u  e.  x  ->  { ( f `  u ) ,  u }  C_  ( ( ran  f  u.  { (/) } )  u.  x ) )
117 prex 4679 . . . . . . . . . . . . . 14  |-  { ( f `  u ) ,  u }  e.  _V
118117elpw 4003 . . . . . . . . . . . . 13  |-  ( { ( f `  u
) ,  u }  e.  ~P ( ( ran  f  u.  { (/) } )  u.  x )  <->  { ( f `  u ) ,  u }  C_  ( ( ran  f  u.  { (/) } )  u.  x ) )
119116, 118sylibr 212 . . . . . . . . . . . 12  |-  ( u  e.  x  ->  { ( f `  u ) ,  u }  e.  ~P ( ( ran  f  u.  { (/) } )  u.  x ) )
120 eleq1 2515 . . . . . . . . . . . 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 222 . . . . . . . . . . 11  |-  ( u  e.  x  ->  (
g  =  { ( f `  u ) ,  u }  ->  g  e.  ~P ( ( ran  f  u.  { (/)
} )  u.  x
) ) )
122121adantld 467 . . . . . . . . . 10  |-  ( u  e.  x  ->  (
( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  ->  g  e.  ~P ( ( ran  f  u.  { (/) } )  u.  x ) ) )
123122rexlimiv 2929 . . . . . . . . 9  |-  ( E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  ->  g  e.  ~P ( ( ran  f  u.  { (/) } )  u.  x ) )
124123abssi 3560 . . . . . . . 8  |-  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  {
( f `  u
) ,  u }
) }  C_  ~P ( ( ran  f  u.  { (/) } )  u.  x )
125110, 124ssexi 4582 . . . . . . 7  |-  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  {
( f `  u
) ,  u }
) }  e.  _V
126 rexeq 3041 . . . . . . . . . 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 3028 . . . . . . . . 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 316 . . . . . . . 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 2882 . . . . . . 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 3187 . . . . . 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 16 . . . . 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 1709 . . . 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 1620 . . 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 195 . 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 8513 . 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 188 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 setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369   A.wal 1381    = wceq 1383   E.wex 1599    e. wcel 1804   E!weu 2268   E*wmo 2269   {cab 2428    =/= wne 2638   A.wral 2793   E.wrex 2794   E!wreu 2795    u. cun 3459    C_ wss 3461   (/)c0 3770   ~Pcpw 3997   {csn 4014   {cpr 4016   ran crn 4990   ` cfv 5578  CHOICEwac 8499
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-reg 8021
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-op 4021  df-uni 4235  df-br 4438  df-opab 4496  df-mpt 4497  df-eprel 4781  df-id 4785  df-fr 4828  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-fv 5586  df-riota 6242  df-ac 8500
This theorem is referenced by:  dfac7  8515
  Copyright terms: Public domain W3C validator