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

Theorem dfac2 8292
Description: Axiom of Choice (first form) of [Enderton] p. 49 implies of our Axiom of Choice (in the form of ac3 8623). The proof does not make use of AC. Note that the Axiom of Regularity is used by the proof. Specifically, elirrv 7804 and preleq 7815 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 8291.) 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 8283 . . 3  |-  (CHOICE  <->  A. x E. f A. z  e.  x  ( z  =/=  (/)  ->  ( f `  z )  e.  z ) )
2 nfra1 2760 . . . . . . 7  |-  F/ z A. z  e.  x  ( z  =/=  (/)  ->  (
f `  z )  e.  z )
3 rsp 2770 . . . . . . . . . . . . 13  |-  ( A. z  e.  x  (
z  =/=  (/)  ->  (
f `  z )  e.  z )  ->  (
z  e.  x  -> 
( z  =/=  (/)  ->  (
f `  z )  e.  z ) ) )
4 equid 1729 . . . . . . . . . . . . . . . . . . 19  |-  z  =  z
5 neeq1 2610 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  (
u  =/=  (/)  <->  z  =/=  (/) ) )
6 eqeq1 2443 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  (
u  =  z  <->  z  =  z ) )
75, 6anbi12d 710 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  z  ->  (
( u  =/=  (/)  /\  u  =  z )  <->  ( z  =/=  (/)  /\  z  =  z ) ) )
87rspcev 3066 . . . . . . . . . . . . . . . . . . 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 5684 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( u  =  z  ->  (
f `  u )  =  ( f `  z ) )
1110preq1d 3953 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  { ( f `  u ) ,  u }  =  { ( f `  z ) ,  u } )
12 preq2 3948 . . . . . . . . . . . . . . . . . . . . 21  |-  ( u  =  z  ->  { ( f `  z ) ,  u }  =  { ( f `  z ) ,  z } )
1311, 12eqtr2d 2470 . . . . . . . . . . . . . . . . . . . 20  |-  ( u  =  z  ->  { ( f `  z ) ,  z }  =  { ( f `  u ) ,  u } )
1413anim2i 569 . . . . . . . . . . . . . . . . . . 19  |-  ( ( u  =/=  (/)  /\  u  =  z )  -> 
( u  =/=  (/)  /\  {
( f `  z
) ,  z }  =  { ( f `
 u ) ,  u } ) )
1514reximi 2817 . . . . . . . . . . . . . . . . . 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 4527 . . . . . . . . . . . . . . . . . 18  |-  { ( f `  z ) ,  z }  e.  _V
18 eqeq1 2443 . . . . . . . . . . . . . . . . . . . 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 2730 . . . . . . . . . . . . . . . . . 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 3099 . . . . . . . . . . . . . . . . 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 2969 . . . . . . . . . . . . . . . . . 18  |-  z  e. 
_V
2423prid2 3977 . . . . . . . . . . . . . . . . 17  |-  z  e. 
{ ( f `  z ) ,  z }
25 fvex 5694 . . . . . . . . . . . . . . . . . 18  |-  ( f `
 z )  e. 
_V
2625prid1 3976 . . . . . . . . . . . . . . . . 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 2498 . . . . . . . . . . . . . . . . . 18  |-  ( v  =  { ( f `
 z ) ,  z }  ->  (
z  e.  v  <->  z  e.  { ( f `  z
) ,  z } ) )
29 eleq2 2498 . . . . . . . . . . . . . . . . . 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 3066 . . . . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . . . . . 17  |-  ( w  =  ( f `  z )  ->  (
w  e.  z  <->  ( f `  z )  e.  z ) )
34 eleq1 2497 . . . . . . . . . . . . . . . . . . 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 2730 . . . . . . . . . . . . . . . . 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 3057 . . . . . . . . . . . . . . 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 2715 . . . . . . . . . . . . . 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 2969 . . . . . . . . . . . . . . . . . . . 20  |-  v  e. 
_V
46 eqeq1 2443 . . . . . . . . . . . . . . . . . . . . . 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 2730 . . . . . . . . . . . . . . . . . . . 20  |-  ( g  =  v  ->  ( E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  <->  E. u  e.  x  ( u  =/=  (/)  /\  v  =  { ( f `  u ) ,  u } ) ) )
4945, 48elab 3099 . . . . . . . . . . . . . . . . . . 19  |-  ( v  e.  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } ) }  <->  E. u  e.  x  ( u  =/=  (/)  /\  v  =  { ( f `  u ) ,  u } ) )
50 neeq1 2610 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( z  =  u  ->  (
z  =/=  (/)  <->  u  =/=  (/) ) )
51 fveq2 5684 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( z  =  u  ->  (
f `  z )  =  ( f `  u ) )
5251eleq1d 2503 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  =  u  ->  (
( f `  z
)  e.  z  <->  ( f `  u )  e.  z ) )
53 eleq2 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3063 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A. z  e.  x  (
z  =/=  (/)  ->  (
f `  z )  e.  z )  ->  (
u  e.  x  -> 
( u  =/=  (/)  ->  (
f `  u )  e.  u ) ) )
57 elirrv 7804 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  -.  w  e.  w
58 eleq2 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  w  e. 
_V
62 fvex 5694 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( f `
 u )  e. 
_V
63 vex 2969 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  u  e. 
_V
6461, 23, 62, 63prel12 4042 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35  |-  ( v  =  { ( f `
 u ) ,  u }  ->  (
w  e.  v  <->  w  e.  { ( f `  u
) ,  u }
) )
67 eleq2 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 7815 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 2829 . . . . . . . . . . . . . . . . . . 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 1690 . . . . . . . . . . . . . 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 1685 . . . . . . . . . . 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 3131 . . . . . . . . . . 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 2716 . . . . . . . . . 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 2281 . . . . . . . . . 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 2791 . . . . . 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 2969 . . . . . . . . . . . 12  |-  f  e. 
_V
105104rnex 6507 . . . . . . . . . . 11  |-  ran  f  e.  _V
106 p0ex 4472 . . . . . . . . . . 11  |-  { (/) }  e.  _V
107105, 106unex 6373 . . . . . . . . . 10  |-  ( ran  f  u.  { (/) } )  e.  _V
108 vex 2969 . . . . . . . . . 10  |-  x  e. 
_V
109107, 108unex 6373 . . . . . . . . 9  |-  ( ( ran  f  u.  { (/)
} )  u.  x
)  e.  _V
110109pwex 4468 . . . . . . . 8  |-  ~P (
( ran  f  u.  {
(/) } )  u.  x
)  e.  _V
111 ssun1 3512 . . . . . . . . . . . . . . 15  |-  ( ran  f  u.  { (/) } )  C_  ( ( ran  f  u.  { (/) } )  u.  x )
112 fvrn0 5705 . . . . . . . . . . . . . . 15  |-  ( f `
 u )  e.  ( ran  f  u. 
{ (/) } )
113111, 112sselii 3346 . . . . . . . . . . . . . 14  |-  ( f `
 u )  e.  ( ( ran  f  u.  { (/) } )  u.  x )
114 elun2 3517 . . . . . . . . . . . . . 14  |-  ( u  e.  x  ->  u  e.  ( ( ran  f  u.  { (/) } )  u.  x ) )
115 prssi 4022 . . . . . . . . . . . . . 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 4527 . . . . . . . . . . . . . 14  |-  { ( f `  u ) ,  u }  e.  _V
118117elpw 3859 . . . . . . . . . . . . 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 2497 . . . . . . . . . . . 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 2829 . . . . . . . . 9  |-  ( E. u  e.  x  ( u  =/=  (/)  /\  g  =  { ( f `  u ) ,  u } )  ->  g  e.  ~P ( ( ran  f  u.  { (/) } )  u.  x ) )
124123abssi 3420 . . . . . . . 8  |-  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  {
( f `  u
) ,  u }
) }  C_  ~P ( ( ran  f  u.  { (/) } )  u.  x )
125110, 124ssexi 4430 . . . . . . 7  |-  { g  |  E. u  e.  x  ( u  =/=  (/)  /\  g  =  {
( f `  u
) ,  u }
) }  e.  _V
126 rexeq 2912 . . . . . . . . . 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 2899 . . . . . . . . 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 2729 . . . . . . 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 3057 . . . . . 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 1688 . . . 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 1604 . . 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 8291 . 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 1367    = wceq 1369   E.wex 1586    e. wcel 1756   E!weu 2252   E*wmo 2253   {cab 2423    =/= wne 2600   A.wral 2709   E.wrex 2710   E!wreu 2711    u. cun 3319    C_ wss 3321   (/)c0 3630   ~Pcpw 3853   {csn 3870   {cpr 3872   ran crn 4833   ` cfv 5411  CHOICEwac 8277
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367  ax-reg 7799
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 2968  df-sbc 3180  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-br 4286  df-opab 4344  df-mpt 4345  df-eprel 4624  df-id 4628  df-fr 4671  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-fv 5419  df-riota 6045  df-ac 8278
This theorem is referenced by:  dfac7  8293
  Copyright terms: Public domain W3C validator