This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem axdc3

Description: Dependent Choice. Axiom DC1 of Schechter p. 149, with the addition of an initial value C . This theorem is weaker than the Axiom of Choice but is stronger than Countable Choice. It shows the existence of a sequence whose values can only be shown to exist (but cannot be constructed explicitly) and also depend on earlier values in the sequence. (Contributed by Mario Carneiro, 27-Jan-2013)

Ref Expression
Hypothesis axdc3.1 
|- A e. _V
Assertion axdc3 
|- ( ( C e. A /\ F : A --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 axdc3.1 
 |-  A e. _V
2 feq1 
 |-  ( t = s -> ( t : suc n --> A <-> s : suc n --> A ) )
3 fveq1 
 |-  ( t = s -> ( t ` (/) ) = ( s ` (/) ) )
4 3 eqeq1d 
 |-  ( t = s -> ( ( t ` (/) ) = C <-> ( s ` (/) ) = C ) )
5 fveq1 
 |-  ( t = s -> ( t ` suc j ) = ( s ` suc j ) )
6 fveq1 
 |-  ( t = s -> ( t ` j ) = ( s ` j ) )
7 6 fveq2d 
 |-  ( t = s -> ( F ` ( t ` j ) ) = ( F ` ( s ` j ) ) )
8 5 7 eleq12d 
 |-  ( t = s -> ( ( t ` suc j ) e. ( F ` ( t ` j ) ) <-> ( s ` suc j ) e. ( F ` ( s ` j ) ) ) )
9 8 ralbidv 
 |-  ( t = s -> ( A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) <-> A. j e. n ( s ` suc j ) e. ( F ` ( s ` j ) ) ) )
10 suceq 
 |-  ( j = k -> suc j = suc k )
11 10 fveq2d 
 |-  ( j = k -> ( s ` suc j ) = ( s ` suc k ) )
12 2fveq3 
 |-  ( j = k -> ( F ` ( s ` j ) ) = ( F ` ( s ` k ) ) )
13 11 12 eleq12d 
 |-  ( j = k -> ( ( s ` suc j ) e. ( F ` ( s ` j ) ) <-> ( s ` suc k ) e. ( F ` ( s ` k ) ) ) )
14 13 cbvralvw 
 |-  ( A. j e. n ( s ` suc j ) e. ( F ` ( s ` j ) ) <-> A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) )
15 9 14 bitrdi 
 |-  ( t = s -> ( A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) <-> A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) )
16 2 4 15 3anbi123d 
 |-  ( t = s -> ( ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) <-> ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
17 16 rexbidv 
 |-  ( t = s -> ( E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) <-> E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) ) )
18 17 cbvabv 
 |-  { t | E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) } = { s | E. n e. _om ( s : suc n --> A /\ ( s ` (/) ) = C /\ A. k e. n ( s ` suc k ) e. ( F ` ( s ` k ) ) ) }
19 eqid 
 |-  ( x e. { t | E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) } |-> { y e. { t | E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) } | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } ) = ( x e. { t | E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) } |-> { y e. { t | E. n e. _om ( t : suc n --> A /\ ( t ` (/) ) = C /\ A. j e. n ( t ` suc j ) e. ( F ` ( t ` j ) ) ) } | ( dom y = suc dom x /\ ( y |` dom x ) = x ) } )
20 1 18 19 axdc3lem4 
 |-  ( ( C e. A /\ F : A --> ( ~P A \ { (/) } ) ) -> E. g ( g : _om --> A /\ ( g ` (/) ) = C /\ A. k e. _om ( g ` suc k ) e. ( F ` ( g ` k ) ) ) )