Metamath Proof Explorer

Theorem axdclem2

Description: Lemma for axdc . Using the full Axiom of Choice, we can construct a choice function g on ~P dom x . From this, we can build a sequence F starting at any value s e. dom x by repeatedly applying g to the set ( Fx ) (where x is the value from the previous iteration). (Contributed by Mario Carneiro, 25-Jan-2013)

Ref Expression
Hypothesis axdclem2.1 
|- F = ( rec ( ( y e. _V |-> ( g ` { z | y x z } ) ) , s ) |` _om )
Assertion axdclem2 
|- ( E. z s x z -> ( ran x C_ dom x -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) ) )

Proof

Step Hyp Ref Expression
1 axdclem2.1 
 |-  F = ( rec ( ( y e. _V |-> ( g ` { z | y x z } ) ) , s ) |` _om )
2 frfnom 
 |-  ( rec ( ( y e. _V |-> ( g ` { z | y x z } ) ) , s ) |` _om ) Fn _om
3 1 fneq1i 
 |-  ( F Fn _om <-> ( rec ( ( y e. _V |-> ( g ` { z | y x z } ) ) , s ) |` _om ) Fn _om )
4 2 3 mpbir 
 |-  F Fn _om
5 4 a1i 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ E. z s x z /\ ran x C_ dom x ) -> F Fn _om )
6 omex 
 |-  _om e. _V
7 6 a1i 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ E. z s x z /\ ran x C_ dom x ) -> _om e. _V )
8 5 7 fnexd 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ E. z s x z /\ ran x C_ dom x ) -> F e. _V )
9 fveq2 
 |-  ( n = (/) -> ( F ` n ) = ( F ` (/) ) )
10 suceq 
 |-  ( n = (/) -> suc n = suc (/) )
11 10 fveq2d 
 |-  ( n = (/) -> ( F ` suc n ) = ( F ` suc (/) ) )
12 9 11 breq12d 
 |-  ( n = (/) -> ( ( F ` n ) x ( F ` suc n ) <-> ( F ` (/) ) x ( F ` suc (/) ) ) )
13 fveq2 
 |-  ( n = k -> ( F ` n ) = ( F ` k ) )
14 suceq 
 |-  ( n = k -> suc n = suc k )
15 14 fveq2d 
 |-  ( n = k -> ( F ` suc n ) = ( F ` suc k ) )
16 13 15 breq12d 
 |-  ( n = k -> ( ( F ` n ) x ( F ` suc n ) <-> ( F ` k ) x ( F ` suc k ) ) )
17 fveq2 
 |-  ( n = suc k -> ( F ` n ) = ( F ` suc k ) )
18 suceq 
 |-  ( n = suc k -> suc n = suc suc k )
19 18 fveq2d 
 |-  ( n = suc k -> ( F ` suc n ) = ( F ` suc suc k ) )
20 17 19 breq12d 
 |-  ( n = suc k -> ( ( F ` n ) x ( F ` suc n ) <-> ( F ` suc k ) x ( F ` suc suc k ) ) )
21 1 fveq1i 
 |-  ( F ` (/) ) = ( ( rec ( ( y e. _V |-> ( g ` { z | y x z } ) ) , s ) |` _om ) ` (/) )
22 fr0g 
 |-  ( s e. _V -> ( ( rec ( ( y e. _V |-> ( g ` { z | y x z } ) ) , s ) |` _om ) ` (/) ) = s )
23 22 elv 
 |-  ( ( rec ( ( y e. _V |-> ( g ` { z | y x z } ) ) , s ) |` _om ) ` (/) ) = s
24 21 23 eqtri 
 |-  ( F ` (/) ) = s
25 24 breq1i 
 |-  ( ( F ` (/) ) x z <-> s x z )
26 25 biimpri 
 |-  ( s x z -> ( F ` (/) ) x z )
27 26 eximi 
 |-  ( E. z s x z -> E. z ( F ` (/) ) x z )
28 peano1 
 |-  (/) e. _om
29 1 axdclem 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x /\ E. z ( F ` (/) ) x z ) -> ( (/) e. _om -> ( F ` (/) ) x ( F ` suc (/) ) ) )
30 28 29 mpi 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x /\ E. z ( F ` (/) ) x z ) -> ( F ` (/) ) x ( F ` suc (/) ) )
31 27 30 syl3an3 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x /\ E. z s x z ) -> ( F ` (/) ) x ( F ` suc (/) ) )
32 31 3com23 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ E. z s x z /\ ran x C_ dom x ) -> ( F ` (/) ) x ( F ` suc (/) ) )
33 fvex 
 |-  ( F ` k ) e. _V
34 fvex 
 |-  ( F ` suc k ) e. _V
35 33 34 brelrn 
 |-  ( ( F ` k ) x ( F ` suc k ) -> ( F ` suc k ) e. ran x )
36 ssel 
 |-  ( ran x C_ dom x -> ( ( F ` suc k ) e. ran x -> ( F ` suc k ) e. dom x ) )
37 35 36 syl5 
 |-  ( ran x C_ dom x -> ( ( F ` k ) x ( F ` suc k ) -> ( F ` suc k ) e. dom x ) )
38 34 eldm 
 |-  ( ( F ` suc k ) e. dom x <-> E. z ( F ` suc k ) x z )
39 37 38 syl6ib 
 |-  ( ran x C_ dom x -> ( ( F ` k ) x ( F ` suc k ) -> E. z ( F ` suc k ) x z ) )
40 39 ad2antll 
 |-  ( ( k e. _om /\ ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x ) ) -> ( ( F ` k ) x ( F ` suc k ) -> E. z ( F ` suc k ) x z ) )
41 peano2 
 |-  ( k e. _om -> suc k e. _om )
42 1 axdclem 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x /\ E. z ( F ` suc k ) x z ) -> ( suc k e. _om -> ( F ` suc k ) x ( F ` suc suc k ) ) )
43 41 42 syl5 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x /\ E. z ( F ` suc k ) x z ) -> ( k e. _om -> ( F ` suc k ) x ( F ` suc suc k ) ) )
44 43 3expia 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x ) -> ( E. z ( F ` suc k ) x z -> ( k e. _om -> ( F ` suc k ) x ( F ` suc suc k ) ) ) )
45 44 com3r 
 |-  ( k e. _om -> ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x ) -> ( E. z ( F ` suc k ) x z -> ( F ` suc k ) x ( F ` suc suc k ) ) ) )
46 45 imp 
 |-  ( ( k e. _om /\ ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x ) ) -> ( E. z ( F ` suc k ) x z -> ( F ` suc k ) x ( F ` suc suc k ) ) )
47 40 46 syld 
 |-  ( ( k e. _om /\ ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ ran x C_ dom x ) ) -> ( ( F ` k ) x ( F ` suc k ) -> ( F ` suc k ) x ( F ` suc suc k ) ) )
48 47 3adantr2 
 |-  ( ( k e. _om /\ ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ E. z s x z /\ ran x C_ dom x ) ) -> ( ( F ` k ) x ( F ` suc k ) -> ( F ` suc k ) x ( F ` suc suc k ) ) )
49 48 ex 
 |-  ( k e. _om -> ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ E. z s x z /\ ran x C_ dom x ) -> ( ( F ` k ) x ( F ` suc k ) -> ( F ` suc k ) x ( F ` suc suc k ) ) ) )
50 12 16 20 32 49 finds2 
 |-  ( n e. _om -> ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ E. z s x z /\ ran x C_ dom x ) -> ( F ` n ) x ( F ` suc n ) ) )
51 50 com12 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ E. z s x z /\ ran x C_ dom x ) -> ( n e. _om -> ( F ` n ) x ( F ` suc n ) ) )
52 51 ralrimiv 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ E. z s x z /\ ran x C_ dom x ) -> A. n e. _om ( F ` n ) x ( F ` suc n ) )
53 fveq1 
 |-  ( f = F -> ( f ` n ) = ( F ` n ) )
54 fveq1 
 |-  ( f = F -> ( f ` suc n ) = ( F ` suc n ) )
55 53 54 breq12d 
 |-  ( f = F -> ( ( f ` n ) x ( f ` suc n ) <-> ( F ` n ) x ( F ` suc n ) ) )
56 55 ralbidv 
 |-  ( f = F -> ( A. n e. _om ( f ` n ) x ( f ` suc n ) <-> A. n e. _om ( F ` n ) x ( F ` suc n ) ) )
57 8 52 56 spcedv 
 |-  ( ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) /\ E. z s x z /\ ran x C_ dom x ) -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) )
58 57 3exp 
 |-  ( A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y ) -> ( E. z s x z -> ( ran x C_ dom x -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) ) ) )
59 vex 
 |-  x e. _V
60 59 dmex 
 |-  dom x e. _V
61 60 pwex 
 |-  ~P dom x e. _V
62 61 ac4c 
 |-  E. g A. y e. ~P dom x ( y =/= (/) -> ( g ` y ) e. y )
63 58 62 exlimiiv 
 |-  ( E. z s x z -> ( ran x C_ dom x -> E. f A. n e. _om ( f ` n ) x ( f ` suc n ) ) )