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 ) )