Metamath Proof Explorer

Theorem dfac8

Description: A proof of the equivalency of the well-ordering theorem weth and the axiom of choice ac7 . (Contributed by Mario Carneiro, 5-Jan-2013)

Ref Expression
Assertion dfac8 
|- ( CHOICE <-> A. x E. r r We x )

Proof

Step Hyp Ref Expression
1 dfac3 
 |-  ( CHOICE <-> A. y E. f A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) )
2 vex 
 |-  x e. _V
3 vpwex 
 |-  ~P x e. _V
4 raleq 
 |-  ( y = ~P x -> ( A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) <-> A. z e. ~P x ( z =/= (/) -> ( f ` z ) e. z ) ) )
5 4 exbidv 
 |-  ( y = ~P x -> ( E. f A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) <-> E. f A. z e. ~P x ( z =/= (/) -> ( f ` z ) e. z ) ) )
6 3 5 spcv 
 |-  ( A. y E. f A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) -> E. f A. z e. ~P x ( z =/= (/) -> ( f ` z ) e. z ) )
7 dfac8a 
 |-  ( x e. _V -> ( E. f A. z e. ~P x ( z =/= (/) -> ( f ` z ) e. z ) -> x e. dom card ) )
8 2 6 7 mpsyl 
 |-  ( A. y E. f A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) -> x e. dom card )
9 dfac8b 
 |-  ( x e. dom card -> E. r r We x )
10 8 9 syl 
 |-  ( A. y E. f A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) -> E. r r We x )
11 10 alrimiv 
 |-  ( A. y E. f A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) -> A. x E. r r We x )
12 vex 
 |-  y e. _V
13 vuniex 
 |-  U. y e. _V
14 weeq2 
 |-  ( x = U. y -> ( r We x <-> r We U. y ) )
15 14 exbidv 
 |-  ( x = U. y -> ( E. r r We x <-> E. r r We U. y ) )
16 13 15 spcv 
 |-  ( A. x E. r r We x -> E. r r We U. y )
17 dfac8c 
 |-  ( y e. _V -> ( E. r r We U. y -> E. f A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) ) )
18 12 16 17 mpsyl 
 |-  ( A. x E. r r We x -> E. f A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) )
19 18 alrimiv 
 |-  ( A. x E. r r We x -> A. y E. f A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) )
20 11 19 impbii 
 |-  ( A. y E. f A. z e. y ( z =/= (/) -> ( f ` z ) e. z ) <-> A. x E. r r We x )
21 1 20 bitri 
 |-  ( CHOICE <-> A. x E. r r We x )