Metamath Proof Explorer

Theorem dfac8alem

Description: Lemma for dfac8a . If the power set of a set has a choice function, then the set is numerable. (Contributed by NM, 10-Feb-1997) (Revised by Mario Carneiro, 5-Jan-2013)

Ref Expression
Hypotheses dfac8alem.2 
|- F = recs ( G )
dfac8alem.3 
|- G = ( f e. _V |-> ( g ` ( A \ ran f ) ) )
Assertion dfac8alem 
|- ( A e. C -> ( E. g A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> A e. dom card ) )

Proof

Step Hyp Ref Expression
1 dfac8alem.2 
 |-  F = recs ( G )
2 dfac8alem.3 
 |-  G = ( f e. _V |-> ( g ` ( A \ ran f ) ) )
3 elex 
 |-  ( A e. C -> A e. _V )
4 difss 
 |-  ( A \ ( F " x ) ) C_ A
5 elpw2g 
 |-  ( A e. _V -> ( ( A \ ( F " x ) ) e. ~P A <-> ( A \ ( F " x ) ) C_ A ) )
6 4 5 mpbiri 
 |-  ( A e. _V -> ( A \ ( F " x ) ) e. ~P A )
7 neeq1 
 |-  ( y = ( A \ ( F " x ) ) -> ( y =/= (/) <-> ( A \ ( F " x ) ) =/= (/) ) )
8 fveq2 
 |-  ( y = ( A \ ( F " x ) ) -> ( g ` y ) = ( g ` ( A \ ( F " x ) ) ) )
9 id 
 |-  ( y = ( A \ ( F " x ) ) -> y = ( A \ ( F " x ) ) )
10 8 9 eleq12d 
 |-  ( y = ( A \ ( F " x ) ) -> ( ( g ` y ) e. y <-> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) )
11 7 10 imbi12d 
 |-  ( y = ( A \ ( F " x ) ) -> ( ( y =/= (/) -> ( g ` y ) e. y ) <-> ( ( A \ ( F " x ) ) =/= (/) -> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) ) )
12 11 rspcv 
 |-  ( ( A \ ( F " x ) ) e. ~P A -> ( A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> ( ( A \ ( F " x ) ) =/= (/) -> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) ) )
13 6 12 syl 
 |-  ( A e. _V -> ( A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> ( ( A \ ( F " x ) ) =/= (/) -> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) ) )
14 13 3imp 
 |-  ( ( A e. _V /\ A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) /\ ( A \ ( F " x ) ) =/= (/) ) -> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) )
15 1 tfr2 
 |-  ( x e. On -> ( F ` x ) = ( G ` ( F |` x ) ) )
16 1 tfr1 
 |-  F Fn On
17 fnfun 
 |-  ( F Fn On -> Fun F )
18 16 17 ax-mp 
 |-  Fun F
19 vex 
 |-  x e. _V
20 resfunexg 
 |-  ( ( Fun F /\ x e. _V ) -> ( F |` x ) e. _V )
21 18 19 20 mp2an 
 |-  ( F |` x ) e. _V
22 rneq 
 |-  ( f = ( F |` x ) -> ran f = ran ( F |` x ) )
23 df-ima 
 |-  ( F " x ) = ran ( F |` x )
24 22 23 eqtr4di 
 |-  ( f = ( F |` x ) -> ran f = ( F " x ) )
25 24 difeq2d 
 |-  ( f = ( F |` x ) -> ( A \ ran f ) = ( A \ ( F " x ) ) )
26 25 fveq2d 
 |-  ( f = ( F |` x ) -> ( g ` ( A \ ran f ) ) = ( g ` ( A \ ( F " x ) ) ) )
27 fvex 
 |-  ( g ` ( A \ ( F " x ) ) ) e. _V
28 26 2 27 fvmpt 
 |-  ( ( F |` x ) e. _V -> ( G ` ( F |` x ) ) = ( g ` ( A \ ( F " x ) ) ) )
29 21 28 ax-mp 
 |-  ( G ` ( F |` x ) ) = ( g ` ( A \ ( F " x ) ) )
30 15 29 eqtrdi 
 |-  ( x e. On -> ( F ` x ) = ( g ` ( A \ ( F " x ) ) ) )
31 30 eleq1d 
 |-  ( x e. On -> ( ( F ` x ) e. ( A \ ( F " x ) ) <-> ( g ` ( A \ ( F " x ) ) ) e. ( A \ ( F " x ) ) ) )
32 14 31 syl5ibrcom 
 |-  ( ( A e. _V /\ A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) /\ ( A \ ( F " x ) ) =/= (/) ) -> ( x e. On -> ( F ` x ) e. ( A \ ( F " x ) ) ) )
33 32 3expia 
 |-  ( ( A e. _V /\ A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) ) -> ( ( A \ ( F " x ) ) =/= (/) -> ( x e. On -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) )
34 33 com23 
 |-  ( ( A e. _V /\ A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) ) -> ( x e. On -> ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) )
35 34 ralrimiv 
 |-  ( ( A e. _V /\ A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) ) -> A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) )
36 35 ex 
 |-  ( A e. _V -> ( A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) )
37 16 tz7.49c 
 |-  ( ( A e. _V /\ A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) ) -> E. x e. On ( F |` x ) : x -1-1-onto-> A )
38 37 ex 
 |-  ( A e. _V -> ( A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) -> E. x e. On ( F |` x ) : x -1-1-onto-> A ) )
39 19 f1oen 
 |-  ( ( F |` x ) : x -1-1-onto-> A -> x ~~ A )
40 isnumi 
 |-  ( ( x e. On /\ x ~~ A ) -> A e. dom card )
41 39 40 sylan2 
 |-  ( ( x e. On /\ ( F |` x ) : x -1-1-onto-> A ) -> A e. dom card )
42 41 rexlimiva 
 |-  ( E. x e. On ( F |` x ) : x -1-1-onto-> A -> A e. dom card )
43 38 42 syl6 
 |-  ( A e. _V -> ( A. x e. On ( ( A \ ( F " x ) ) =/= (/) -> ( F ` x ) e. ( A \ ( F " x ) ) ) -> A e. dom card ) )
44 36 43 syld 
 |-  ( A e. _V -> ( A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> A e. dom card ) )
45 3 44 syl 
 |-  ( A e. C -> ( A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> A e. dom card ) )
46 45 exlimdv 
 |-  ( A e. C -> ( E. g A. y e. ~P A ( y =/= (/) -> ( g ` y ) e. y ) -> A e. dom card ) )