Metamath Proof Explorer

Theorem fdc1

Description: Variant of fdc with no specified base value. (Contributed by Jeff Madsen, 18-Jun-2010)

Ref Expression
Hypotheses fdc1.1 
|- A e. _V
fdc1.2 
|- M e. ZZ
fdc1.3 
|- Z = ( ZZ>= ` M )
fdc1.4 
|- N = ( M + 1 )
fdc1.5 
|- ( a = ( f ` M ) -> ( ze <-> si ) )
fdc1.6 
|- ( a = ( f ` ( k - 1 ) ) -> ( ph <-> ps ) )
fdc1.7 
|- ( b = ( f ` k ) -> ( ps <-> ch ) )
fdc1.8 
|- ( a = ( f ` n ) -> ( th <-> ta ) )
fdc1.9 
|- ( et -> E. a e. A ze )
fdc1.10 
|- ( et -> R Fr A )
fdc1.11 
|- ( ( et /\ a e. A ) -> ( th \/ E. b e. A ph ) )
fdc1.12 
|- ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> b R a )
Assertion fdc1 
|- ( et -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( si /\ ta ) /\ A. k e. ( N ... n ) ch ) )

Proof

Step Hyp Ref Expression
1 fdc1.1 
 |-  A e. _V
2 fdc1.2 
 |-  M e. ZZ
3 fdc1.3 
 |-  Z = ( ZZ>= ` M )
4 fdc1.4 
 |-  N = ( M + 1 )
5 fdc1.5 
 |-  ( a = ( f ` M ) -> ( ze <-> si ) )
6 fdc1.6 
 |-  ( a = ( f ` ( k - 1 ) ) -> ( ph <-> ps ) )
7 fdc1.7 
 |-  ( b = ( f ` k ) -> ( ps <-> ch ) )
8 fdc1.8 
 |-  ( a = ( f ` n ) -> ( th <-> ta ) )
9 fdc1.9 
 |-  ( et -> E. a e. A ze )
10 fdc1.10 
 |-  ( et -> R Fr A )
11 fdc1.11 
 |-  ( ( et /\ a e. A ) -> ( th \/ E. b e. A ph ) )
12 fdc1.12 
 |-  ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> b R a )
13 eleq1w 
 |-  ( c = a -> ( c e. A <-> a e. A ) )
14 13 anbi2d 
 |-  ( c = a -> ( ( et /\ c e. A ) <-> ( et /\ a e. A ) ) )
15 sbceq2a 
 |-  ( c = a -> ( [. c / a ]. ze <-> ze ) )
16 14 15 anbi12d 
 |-  ( c = a -> ( ( ( et /\ c e. A ) /\ [. c / a ]. ze ) <-> ( ( et /\ a e. A ) /\ ze ) ) )
17 16 imbi1d 
 |-  ( c = a -> ( ( ( ( et /\ c e. A ) /\ [. c / a ]. ze ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( si /\ ta ) /\ A. k e. ( N ... n ) ch ) ) <-> ( ( ( et /\ a e. A ) /\ ze ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( si /\ ta ) /\ A. k e. ( N ... n ) ch ) ) ) )
18 sbsbc 
 |-  ( [ d / a ] ph <-> [. d / a ]. ph )
19 nfv 
 |-  F/ a ps
20 19 6 sbhypf 
 |-  ( d = ( f ` ( k - 1 ) ) -> ( [ d / a ] ph <-> ps ) )
21 18 20 bitr3id 
 |-  ( d = ( f ` ( k - 1 ) ) -> ( [. d / a ]. ph <-> ps ) )
22 sbsbc 
 |-  ( [ d / a ] th <-> [. d / a ]. th )
23 nfv 
 |-  F/ a ta
24 23 8 sbhypf 
 |-  ( d = ( f ` n ) -> ( [ d / a ] th <-> ta ) )
25 22 24 bitr3id 
 |-  ( d = ( f ` n ) -> ( [. d / a ]. th <-> ta ) )
26 simprl 
 |-  ( ( et /\ ( c e. A /\ [. c / a ]. ze ) ) -> c e. A )
27 10 adantr 
 |-  ( ( et /\ ( c e. A /\ [. c / a ]. ze ) ) -> R Fr A )
28 nfv 
 |-  F/ a ( et /\ d e. A )
29 nfsbc1v 
 |-  F/ a [. d / a ]. th
30 nfcv 
 |-  F/_ a A
31 nfsbc1v 
 |-  F/ a [. d / a ]. ph
32 30 31 nfrex 
 |-  F/ a E. b e. A [. d / a ]. ph
33 29 32 nfor 
 |-  F/ a ( [. d / a ]. th \/ E. b e. A [. d / a ]. ph )
34 28 33 nfim 
 |-  F/ a ( ( et /\ d e. A ) -> ( [. d / a ]. th \/ E. b e. A [. d / a ]. ph ) )
35 eleq1w 
 |-  ( a = d -> ( a e. A <-> d e. A ) )
36 35 anbi2d 
 |-  ( a = d -> ( ( et /\ a e. A ) <-> ( et /\ d e. A ) ) )
37 sbceq1a 
 |-  ( a = d -> ( th <-> [. d / a ]. th ) )
38 sbceq1a 
 |-  ( a = d -> ( ph <-> [. d / a ]. ph ) )
39 38 rexbidv 
 |-  ( a = d -> ( E. b e. A ph <-> E. b e. A [. d / a ]. ph ) )
40 37 39 orbi12d 
 |-  ( a = d -> ( ( th \/ E. b e. A ph ) <-> ( [. d / a ]. th \/ E. b e. A [. d / a ]. ph ) ) )
41 36 40 imbi12d 
 |-  ( a = d -> ( ( ( et /\ a e. A ) -> ( th \/ E. b e. A ph ) ) <-> ( ( et /\ d e. A ) -> ( [. d / a ]. th \/ E. b e. A [. d / a ]. ph ) ) ) )
42 34 41 11 chvarfv 
 |-  ( ( et /\ d e. A ) -> ( [. d / a ]. th \/ E. b e. A [. d / a ]. ph ) )
43 42 adantlr 
 |-  ( ( ( et /\ ( c e. A /\ [. c / a ]. ze ) ) /\ d e. A ) -> ( [. d / a ]. th \/ E. b e. A [. d / a ]. ph ) )
44 nfv 
 |-  F/ a et
45 44 31 nfan 
 |-  F/ a ( et /\ [. d / a ]. ph )
46 nfv 
 |-  F/ a ( d e. A /\ b e. A )
47 45 46 nfan 
 |-  F/ a ( ( et /\ [. d / a ]. ph ) /\ ( d e. A /\ b e. A ) )
48 nfv 
 |-  F/ a b R d
49 47 48 nfim 
 |-  F/ a ( ( ( et /\ [. d / a ]. ph ) /\ ( d e. A /\ b e. A ) ) -> b R d )
50 38 anbi2d 
 |-  ( a = d -> ( ( et /\ ph ) <-> ( et /\ [. d / a ]. ph ) ) )
51 35 anbi1d 
 |-  ( a = d -> ( ( a e. A /\ b e. A ) <-> ( d e. A /\ b e. A ) ) )
52 50 51 anbi12d 
 |-  ( a = d -> ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) <-> ( ( et /\ [. d / a ]. ph ) /\ ( d e. A /\ b e. A ) ) ) )
53 breq2 
 |-  ( a = d -> ( b R a <-> b R d ) )
54 52 53 imbi12d 
 |-  ( a = d -> ( ( ( ( et /\ ph ) /\ ( a e. A /\ b e. A ) ) -> b R a ) <-> ( ( ( et /\ [. d / a ]. ph ) /\ ( d e. A /\ b e. A ) ) -> b R d ) ) )
55 49 54 12 chvarfv 
 |-  ( ( ( et /\ [. d / a ]. ph ) /\ ( d e. A /\ b e. A ) ) -> b R d )
56 55 adantllr 
 |-  ( ( ( ( et /\ ( c e. A /\ [. c / a ]. ze ) ) /\ [. d / a ]. ph ) /\ ( d e. A /\ b e. A ) ) -> b R d )
57 1 2 3 4 21 7 25 26 27 43 56 fdc 
 |-  ( ( et /\ ( c e. A /\ [. c / a ]. ze ) ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) )
58 57 anassrs 
 |-  ( ( ( et /\ c e. A ) /\ [. c / a ]. ze ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) )
59 idd 
 |-  ( ( ( et /\ c e. A ) /\ [. c / a ]. ze ) -> ( f : ( M ... n ) --> A -> f : ( M ... n ) --> A ) )
60 dfsbcq 
 |-  ( ( f ` M ) = c -> ( [. ( f ` M ) / a ]. ze <-> [. c / a ]. ze ) )
61 fvex 
 |-  ( f ` M ) e. _V
62 61 5 sbcie 
 |-  ( [. ( f ` M ) / a ]. ze <-> si )
63 60 62 bitr3di 
 |-  ( ( f ` M ) = c -> ( [. c / a ]. ze <-> si ) )
64 63 biimpcd 
 |-  ( [. c / a ]. ze -> ( ( f ` M ) = c -> si ) )
65 64 adantl 
 |-  ( ( ( et /\ c e. A ) /\ [. c / a ]. ze ) -> ( ( f ` M ) = c -> si ) )
66 65 anim1d 
 |-  ( ( ( et /\ c e. A ) /\ [. c / a ]. ze ) -> ( ( ( f ` M ) = c /\ ta ) -> ( si /\ ta ) ) )
67 idd 
 |-  ( ( ( et /\ c e. A ) /\ [. c / a ]. ze ) -> ( A. k e. ( N ... n ) ch -> A. k e. ( N ... n ) ch ) )
68 59 66 67 3anim123d 
 |-  ( ( ( et /\ c e. A ) /\ [. c / a ]. ze ) -> ( ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) -> ( f : ( M ... n ) --> A /\ ( si /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
69 68 eximdv 
 |-  ( ( ( et /\ c e. A ) /\ [. c / a ]. ze ) -> ( E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) -> E. f ( f : ( M ... n ) --> A /\ ( si /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
70 69 reximdv 
 |-  ( ( ( et /\ c e. A ) /\ [. c / a ]. ze ) -> ( E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( ( f ` M ) = c /\ ta ) /\ A. k e. ( N ... n ) ch ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( si /\ ta ) /\ A. k e. ( N ... n ) ch ) ) )
71 58 70 mpd 
 |-  ( ( ( et /\ c e. A ) /\ [. c / a ]. ze ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( si /\ ta ) /\ A. k e. ( N ... n ) ch ) )
72 17 71 chvarvv 
 |-  ( ( ( et /\ a e. A ) /\ ze ) -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( si /\ ta ) /\ A. k e. ( N ... n ) ch ) )
73 72 9 r19.29a 
 |-  ( et -> E. n e. Z E. f ( f : ( M ... n ) --> A /\ ( si /\ ta ) /\ A. k e. ( N ... n ) ch ) )